From c301e17392ad24f9d6009be092506dc2313c4427 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Feb 2010 16:56:57 +0000 Subject: [PATCH] Parts of the status were not re-initialized correctly during a reset. Fixed (and bugs avoided). --- .../grafite_engine/grafiteEngine.ml | 6 +++--- .../components/grafite_engine/grafiteSync.ml | 10 +++++----- .../components/grafite_engine/grafiteSync.mli | 2 +- helm/software/matita/matitaScript.ml | 20 +++++++++++++------ helm/software/matita/matitaWiki.ml | 2 +- 5 files changed, 24 insertions(+), 16 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 840a6e220..73905eef3 100644 --- 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 7946b4a1e..47744f66e 100644 --- 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 d15896dab..bac7eee9b 100644 --- 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 2186b75b5..44ead20ba 100644 --- 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 ba6840ee5..52d18f42a 100644 --- 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 -- 2.39.2