coercion command now requires an uri

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 75773e3fe579f3b1ccf9cf12a55befbcf9618cc1..c14bd77101628212a200e1066d31252c9c9792b5 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -83,6 +83,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | None -> []
         | Some devel -> [MatitamakeLib.root_for_development devel ]
   in
+  let include_ =
+    include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+  in
   let parsed_text_length = String.length parsed_text in
   let loc, ex = 
     match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
@@ -427,7 +430,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 +465,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 +636,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 +660,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 +797,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