X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=c5239ffb4819c4dbacf0b967d66d34ecdd8b8ecf;hb=5356519d50425dfca5b42ad5faeb2181d4240c78;hp=182f6e165d5ab08f68ac5f8902e0e644ff89764c;hpb=35a06fa8d6c2664301b59e77dcbff5bcfd4a5091;p=helm.git

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 182f6e165..c5239ffb4 100644
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -743,14 +743,14 @@ class script  ~(source_view: GSourceView.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses () =
+let initial_statuses baseuri =
  (* these include_paths are used only to load the initial notation *)
  let include_paths =
   Helm_registry.get_list Helm_registry.string "matita.includes" in
  let lexicon_status =
   CicNotation2.load_notation ~include_paths
    BuildTimeConf.core_notation_script in
- let grafite_status = GrafiteSync.init () in
+ let grafite_status = GrafiteSync.init baseuri in
   grafite_status,lexicon_status
 in
 object (self)
@@ -773,7 +773,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses () ]
+  val mutable history = [ initial_statuses "cic:/matita/test/" ]
     (** 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.
@@ -933,7 +933,8 @@ object (self)
     
   method assignFileName file =
     let root, buri, file = Librarian.baseuri_of_script ~include_paths file in
-    Helm_registry.set "matita.filename" file
+    Helm_registry.set "matita.filename" file;
+    self#reset_buffer
     
   method saveToFile () =
     let oc = open_out (Librarian.filename ()) in
@@ -967,8 +968,10 @@ object (self)
     LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
 
   method private reset_buffer = 
+    let file = Librarian.filename () in
+    let root, buri, file = Librarian.baseuri_of_script file in
     statements <- [];
-    history <- [ initial_statuses () ];
+    history <- [ initial_statuses buri ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;