From f6e34efbe6ce54f87d62997a0b81ca541a12d3da Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Sep 2005 13:52:37 +0000
Subject: [PATCH] bugfixes: 1) ask for saving/mooing only when the user has
 choosen a file to load 2) opening a file doesn't call goto_top (removing all
 xml, even if the moo has    been generated). This fix should enforce the
 invariant that a moo exists only    if the corrsponding xml objects do. 3)
 the switch_page callback is inhibited before removing pages in   
 sequentViewers#reset

---
 helm/matita/matita.ml         |  9 +++------
 helm/matita/matitaGui.ml      | 22 +++++++++++-----------
 helm/matita/matitaMathView.ml | 14 +++++++-------
 helm/matita/matitaScript.ml   | 18 ++++++++++++------
 4 files changed, 33 insertions(+), 30 deletions(-)

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 6e5af0645..2a87554d8 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -91,12 +91,9 @@ let _ =
     | Incomplete_proof ((proof, goal) as status) ->
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
-    | Proof proof -> 
-        sequents_viewer#load_logo_with_qed
-    | No_proof -> 
-        sequents_viewer#load_logo
-    | Intermediate _ -> 
-        assert false (* only the engine may be in this state *)
+    | Proof proof -> sequents_viewer#load_logo_with_qed
+    | No_proof -> sequents_viewer#load_logo
+    | Intermediate _ -> assert false (* only the engine may be in this state *)
   in
   script#addObserver sequents_observer;
   script#addObserver browser_observer
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 153d474ab..1b46c03a4 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -606,19 +606,19 @@ class gui () =
         let script = s () in 
         let status = script#status in
         try 
-          if source_view#buffer#modified then
-            begin
-              match ask_unsaved main#toplevel with
-              | `YES -> saveScript ()
-              | `NO -> ()
-              | `CANCEL -> raise MatitaTypes.Cancel
-            end;
-          (match script_fname with
-          | None -> ()
-          | Some fname -> 
-              ask_and_save_moo_if_needed main#toplevel fname status);
           match self#chooseFile () with
           | Some f -> 
+                if source_view#buffer#modified then
+                  begin
+                    match ask_unsaved main#toplevel with
+                    | `YES -> saveScript ()
+                    | `NO -> ()
+                    | `CANCEL -> raise MatitaTypes.Cancel
+                  end;
+                (match script_fname with
+                | None -> ()
+                | Some fname -> 
+                    ask_and_save_moo_if_needed main#toplevel fname status);
                 script#reset (); 
                 script#assignFileName f;
                 source_view#source_buffer#begin_not_undoable_action ();
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 47f8c5a5c..532c3dd97 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -430,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           w#remove cicMathView#coerce;
           scrolledWin <- None
       | None -> ());
-      for i = 0 to pages do notebook#remove_page 0 done;
+      (match switch_page_callback with
+      | Some id ->
+          GtkSignal.disconnect notebook#as_widget id;
+          switch_page_callback <- None
+      | None -> ());
+      for i = 0 to pages do notebook#remove_page 0 done; 
       notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- [];
+      _metasenv <- []; 
       self#script#setGoal ~-1;
-      (match switch_page_callback with
-      | Some id ->
-          GtkSignal.disconnect notebook#as_widget id;
-          switch_page_callback <- None
-      | None -> ())
 
     method load_sequents (status: ProofEngineTypes.status) =
       let ((_, metasenv, _, _), goal) = status in
diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f181b53d2..8bd0d60d1 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -586,7 +586,7 @@ object (self)
 
   method loadFromFile f =
     buffer#set_text (MatitaMisc.input_file f);
-    self#goto_top;
+    self#reset_buffer;
     buffer#set_modified false
     
   method assignFileName file =
@@ -613,21 +613,23 @@ object (self)
       end
   
   method private goto_top =
-    MatitaSync.time_travel ~present:self#status ~past:init;
+    MatitaSync.time_travel ~present:self#status ~past:init
+
+  method private reset_buffer = 
     statements <- [];
     history <- [ init ];
     userGoal <- ~-1;
+    self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
 
   method reset () =
-    self#goto_top;
+    self#reset_buffer;
     source_buffer#begin_not_undoable_action ();
     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
     source_buffer#end_not_undoable_action ();
-    self#notify;
     buffer#set_modified false
-
+  
   method template () =
     let template = MatitaMisc.input_file BuildTimeConf.script_template in 
     buffer#insert ~iter:(buffer#get_iter `START) template;
@@ -645,7 +647,11 @@ object (self)
     let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in 
     let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
     match pos with
-    | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify
+    | `Top -> 
+        dispose_old_locked_mark (); 
+        self#goto_top; 
+        self#reset_buffer;
+        self#notify
     | `Bottom ->
         (try 
           let rec dowhile () =
-- 
2.39.2