let i = ref 0 in
fun () -> incr i; !i
-class script ~(source_view: GSourceView.source_view)
+class script ~(source_view: GSourceView2.source_view)
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~ask_confirmation
() =
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
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.
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)
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;