When switching to a new script, the other parts of the interface are

now notified.

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 91276e0ddf8945c1e9c24e7ff6c7107f0a24da08..eb39e019ddfc54472aa457d0eedb648adc8dd42c 100644 (file)
--- 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;

diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli
index 32f095a0a693e9763eb079485933a654c4735ed7..8e323ddc42aa6a35f127d70b77eac0ec0564fc53 100644 (file)
--- a/matita/matita/matitaMathView.mli
+++ b/matita/matita/matitaMathView.mli
@@ -26,7 +26,7 @@
 (** {2 Instances} *)
 val cicBrowser: unit -> MatitaGuiTypes.cicBrowser
 
-(** {2 Singleton instances} *)
+(** {2 To be called just once} *)
 val sequentsViewer_instance:  GPack.notebook -> MatitaGuiTypes.sequentsViewer
 
 (** {2 Global changes} *)

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index f3f38ccac20ba3251892ccb6a37215d8f81f4ec4..8ed2fa910b9fa7cf482a2e1f8772ed429809b867 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -832,6 +832,9 @@ object (self)
     let grafite_status = self#grafite_status in
     List.iter (fun o -> o grafite_status) observers
 
+  method activate =
+    self#notify
+
   method loadFromString s =
     buffer#set_text s;
     self#reset_buffer;
@@ -1040,15 +1043,18 @@ let script ~urichooser ~ask_confirmation ~parent ~tab_label ()
   _script := s::!_script;
   s
 
-let current () =
+let at_page page =
  let notebook = (MatitaMisc.get_gui ())#main#scriptNotebook in
- let parent = notebook#get_nth_page notebook#current_page in
+ let parent = notebook#get_nth_page page in
   try
    List.find (fun s -> s#has_parent parent) !_script
   with
    Not_found -> assert false
 ;;
 
+let current () =
+ at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page)
+
 let iter_scripts f = List.iter f !_script;;
 
 let _ =

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index 5e8658d3fc184493f99af6cfc7b28942e00ffc9a..28f415ab2aa947fdc92008e013e916a3623e9cda 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -50,6 +50,7 @@ object
 
   (** {2 History} *)
 
+  method activate : unit
   method advance : ?statement:string -> unit -> unit
   method retract : unit -> unit
   method goto: [`Top | `Bottom | `Cursor] -> unit -> unit
@@ -117,4 +118,5 @@ val script:
     script
 
 val current: unit -> script
+val at_page: int -> script
 val iter_scripts: (script -> unit) -> unit