+
+ public void updateErrorMarksAll()
+ {
+ this.updateErrorMarks("ERR");
+ this.updateErrorMarks("WARN");
+ this.updateErrorMarks("DEPR");
+
+ }
+ void updateErrorMarks(string cat)
+ {
+ this.code_editor_tab.updateErrorMarks(cat);
+ switch(this.file.xtype) {
+ case "Roo":
+ this.window_rooview.updateErrorMarks(cat);// foce scroll.
+ return;
+ case "Gtk":
+ this.window_gladeview.updateErrorMarks(cat);
+ return;
+ default:
+ return;
+ }
+ }
+
+