From b9a7832bdd58be9ab5b9547af880bea152f2c3ce Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Dec 2010 21:27:29 +0000
Subject: [PATCH] code simplification

---
 matita/matita/matita.ml          | 1 -
 matita/matita/matitaGui.ml       | 3 ++-
 matita/matita/matitaGuiTypes.mli | 1 -
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index fa664e95b..72b82839d 100644
--- 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 f38a27859..236d32f68 100644
--- 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 5ced23d9e..fa2583d06 100644
--- 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
 
-- 
2.39.2