Parts of the status were not re-initialized correctly during a reset.

Fixed (and bugs avoided).

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 840a6e22017147b6a8b92587f235915b6d80edf1..73905eef306be23960b89d239e2ff473f7ce4ff3 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -531,7 +531,7 @@ let record_index_obj =
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
- prerr_endline (string_of_int height);
+ (*prerr_endline (string_of_int height);*)
  let mk_item orig_ty spec =
    let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
    let keys = 
@@ -618,11 +618,11 @@ let index_eq_for_auto status uri =
    let newstatus = index_eq uri status in
      if newstatus == status then status 
      else
-       (prerr_endline ("recording " ^ (NUri.string_of_uri uri));
+       ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
        let dump = record_index_eq uri :: newstatus#dump 
        in newstatus#set_dump dump)
  else 
-   (prerr_endline "Not a fact";
+   ((*prerr_endline "Not a fact";*)
    status)
 ;; 
 

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 7946b4a1e211ec3a0b769ba49f81f1ca8594b591..47744f66e0332e962b2feace6b5f42cb0399a8df 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -162,7 +162,11 @@ let uri_list_diff l2 l1 =
   let diff = S.diff s2 s1 in
   S.fold (fun uri uris -> uri :: uris) diff []
 
-let time_travel ~present ~past =
+let initial_status lexicon_status baseuri =
+ (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus
+;;
+
+let time_travel  ~present ?(past=initial_status present present#baseuri) () =
   let objs_to_remove =
    uri_list_diff present#objects past#objects in
   List.iter LibrarySync.remove_obj objs_to_remove;
@@ -170,10 +174,6 @@ let time_travel ~present ~past =
   NCicLibrary.time_travel past
 ;;
 
-let initial_status lexicon_status baseuri =
- (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus
-;;
-
 let init lexicon_status =
   CoercDb.restore CoercDb.empty_coerc_db;
   LibraryObjects.reset_defaults ();

diff --git a/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli
index d15896dab89823a41c8f9d6ab2fad4d522fdb0e1..bac7eee9b874e130d7ca123e9626ce2cd9fb2cf3 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.mli
+++ b/helm/software/components/grafite_engine/grafiteSync.mli
@@ -39,7 +39,7 @@ val prefer_coercion:
   GrafiteTypes.status -> UriManager.uri -> GrafiteTypes.status 
 
 val time_travel: 
-  present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
+  present:GrafiteTypes.status -> ?past:GrafiteTypes.status -> unit -> unit
 
   (* also resets the imperative part of the status 
    * init: the baseuri of the current script *)

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 2186b75b5ff2d4c9914861031920487d86498197..44ead20baf1672260e88037394fcda180c10affd 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -699,9 +699,17 @@ class script  ~(source_view: GSourceView2.source_view)
               () =
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
-let initial_statuses baseuri =
+let initial_statuses current baseuri =
+ let empty_lstatus = new LexiconEngine.status in
+ (match current with
+     Some current ->
+      LexiconSync.time_travel ~present:current ~past:empty_lstatus;
+      GrafiteSync.time_travel ~present:current ();
+      (* CSC: there is a known bug in invalidation; temporary fix here *)
+      NCicEnvironment.invalidate ()
+   | None -> ());
  let lexicon_status =
-   CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
+   CicNotation2.load_notation ~include_paths:[] empty_lstatus
      BuildTimeConf.core_notation_script 
  in
  let grafite_status = GrafiteSync.init lexicon_status baseuri in
@@ -770,7 +778,7 @@ object (self)
 
   val mutable statements = []    (** executed statements *)
 
-  val mutable history = [ initial_statuses default_buri ]
+  val mutable history = [ initial_statuses None default_buri ]
     (** 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.
@@ -845,7 +853,7 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
+    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)
@@ -1010,12 +1018,12 @@ object (self)
     in
     (* FIXME: this is not correct since there is no undo for 
      * library_objects.set_default... *)
-    GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
+    GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status ();
     LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
 
   method private reset_buffer = 
     statements <- [];
-    history <- [ initial_statuses self#buri_of_current_file ];
+    history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
     userGoal <- None;
     self#notify;
     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index ba6840ee5e500d51aed42c02660f05e527561de4..52d18f42a3ea5d43caaf6856d02d5aabb8377900 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -143,7 +143,7 @@ let rec interactive_loop () =
            LexiconSync.time_travel
             ~present:cur_grafite_status ~past:grafite_status;
            GrafiteSync.time_travel
-            ~present:cur_grafite_status ~past:grafite_status;
+            ~present:cur_grafite_status ~past:grafite_status ();
            interactive_loop (Some n)
     | `Do command ->
         let str = Ulexing.from_utf8_string command in