Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 75773e3fe579f3b1ccf9cf12a55befbcf9618cc1..da2c5b2fa168a85080812a7e329004d38f2a2c4d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -427,7 +427,6 @@ let fresh_script_id =
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView.source_view)
-              ~(init: GrafiteTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -463,7 +462,7 @@ object (self)
       (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
 
   val mutable statements = [];    (** executed statements *)
-  val mutable history = [ init ];
+  val mutable history = [ MatitaSync.init () ];
     (** list of states before having executed statements. Head element of this
       * list is the current state, last element is the state at the beginning of
       * the script.
@@ -634,11 +633,20 @@ object (self)
       end
   
   method private goto_top =
+    let init = 
+      let rec last x = function 
+      | [] -> x
+      | hd::tl -> last hd tl
+      in
+      last self#status history
+    in
+    (* FIXME: this is not correct since there is no undo for 
+     * library_objects.set_default... *)
     MatitaSync.time_travel ~present:self#status ~past:init
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ init ];
+    history <- [ MatitaSync.init () ];
     userGoal <- ~-1;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -649,7 +657,7 @@ object (self)
     source_buffer#begin_not_undoable_action ();
     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
     source_buffer#end_not_undoable_action ();
-    buffer#set_modified false
+    buffer#set_modified false;
   
   method template () =
     let template = HExtlib.input_file BuildTimeConf.script_template in 
@@ -786,10 +794,10 @@ end
 
 let _script = ref None
 
-let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
   in
   _script := Some s;
   s