Bug fixed: the newScript method must be called only after registering the

gui. I have moved the invocation of self#newScript from the initializer to the
instance() function to solve the issue (an ugly gtk error when Matita starts).

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 63d0f999b557b8a96472b2d31f219ade53f9e01f..99a93773ba3c7f79c44ce396a4d5044277c0af39 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -865,8 +865,7 @@ class gui () =
        (fun page ->
          let script = MatitaScript.at_page page in
           script#activate;
-          main#saveMenuItem#misc#set_sensitive script#has_name));
-      self#newScript ()
+          main#saveMenuItem#misc#set_sensitive script#has_name))
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -968,7 +967,7 @@ class gui () =
      let script = MatitaScript.at_page page in 
       self#closeScript page script
 
-    method private newScript () = 
+    method newScript () = 
        let scrolledWindow = GBin.scrolled_window () in
        let hbox = GPack.hbox () in
        let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in
@@ -1063,8 +1062,10 @@ class gui () =
 
 let gui () = 
   let g = new gui () in
-  MatitaMisc.set_gui g;
-  g
+  let rg = (g :> MatitaGuiTypes.gui) in
+  MatitaMisc.set_gui rg;
+  g#newScript ();
+  rg
   
 let instance = singleton gui