From 65a0f081b506782b436bcac976343261b8011eba Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 21 Dec 2010 15:14:47 +0000
Subject: [PATCH] When switching to a new script, the other parts of the
 interface are now notified.

---
 matita/matita/matitaGui.ml       |  4 +++-
 matita/matita/matitaMathView.mli |  2 +-
 matita/matita/matitaScript.ml    | 10 ++++++++--
 matita/matita/matitaScript.mli   |  2 ++
 4 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 91276e0dd..eb39e019d 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;
diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli
index 32f095a0a..8e323ddc4 100644
--- 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 f3f38ccac..8ed2fa910 100644
--- 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 5e8658d3f..28f415ab2 100644
--- 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
-- 
2.39.2