code simplification

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index fa664e95b6a06ee2944557bd4688337bb214c09a..72b82839d95823175cb80a604ea21c3d76c97784 100644 (file)
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -112,7 +112,6 @@ let _ =
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
   let gui = MatitaGui.instance () in
   init_debugging_menu gui;
-  gui#newScript ();
   List.iter gui#loadScript (List.rev args);
   gui#main#mainWin#show ();
   try

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index f38a278597a51f1dd7fbeaf23d7a97751bbd4271..236d32f6887867e648677893493fb63fd70b9f69 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -874,6 +874,7 @@ class gui () =
          let script = MatitaScript.at_page page in
           script#activate;
           main#saveMenuItem#misc#set_sensitive script#has_name));
+      self#newScript ()
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -975,7 +976,7 @@ class gui () =
      let script = MatitaScript.at_page page in 
       self#closeScript page script
 
-    method newScript () = 
+    method private newScript () = 
        let scrolledWindow = GBin.scrolled_window () in
        let hbox = GPack.hbox () in
        let tab_label = GMisc.label ~text:"foo"

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index 5ced23d9edae6cef9cbe216785d1fa19eaf7ab05..fa2583d06d6b98299d374df8983c6390f8cfd08a 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -29,7 +29,6 @@ object
   method main: MatitaGeneratedGui.mainWin
 
     (** {2 Utility methods} *)
-  method newScript: unit -> unit
   method loadScript: string -> unit
 end