X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=680dec8e612850447ca1f179bb1e9a48dd6c19d3;hb=6ab0b3e34eee7c4efa628e2994b461347d1bcebf;hp=91276e0ddf8945c1e9c24e7ff6c7107f0a24da08;hpb=0c69106b8cf67a0baad545a9d7b0816b2b7de8ac;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 91276e0dd..680dec8e6 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -914,6 +914,8 @@ class gui () =
         MatitaMisc.decrease_font_size;
       connect_menu_item main#normalFontSizeMenuItem
         MatitaMisc.reset_font_size;
+      ignore (main#scriptNotebook#connect#switch_page
+       (fun page -> (MatitaScript.at_page page)#activate));
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -975,7 +977,6 @@ class gui () =
     method newScript () = 
        let scrolledWindow = GBin.scrolled_window () in
        let tab_label = GMisc.label ~text:"foo" () in
-       ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce);
        let script =
         MatitaScript.script 
           ~urichooser:(fun source_view uris ->
@@ -993,6 +994,7 @@ class gui () =
                 ~parent:(MatitaMisc.get_gui ())#main#toplevel ())
           ~parent:scrolledWindow ~tab_label ()
        in
+        ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce);
         main#scriptNotebook#goto_page 0;
         sequents_viewer#reset;
         sequents_viewer#load_logo;
@@ -1003,15 +1005,11 @@ class gui () =
              `ProofMode ->
               sequents_viewer#nload_sequents grafite_status;
               (try
-                script#setGoal
-                 (Some (Continuationals.Stack.find_goal grafite_status#stack));
                 let goal =
-                 match script#goal with
-                    None -> assert false
-                  | Some n -> n
+                 Continuationals.Stack.find_goal grafite_status#stack
                 in
                  sequents_viewer#goto_sequent grafite_status goal
-              with Failure _ -> script#setGoal None);
+              with Failure _ -> ());
            | `CommandMode -> sequents_viewer#load_logo
         in
         script#addObserver sequents_observer;