From 591098895b69f9179c6156cac43abdf0d38a8708 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Jan 2011 22:02:11 +0000 Subject: [PATCH] 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). --- matita/matita/matitaGui.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 63d0f999b..99a93773b 100644 --- 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 -- 2.39.2