type guistuff = {
mathviewer:MatitaTypes.mathViewer;
- urichooser: UriManager.uri list -> UriManager.uri list;
+ urichooser: NReference.reference list -> NReference.reference list;
ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
else raise (Failure ("Compiling: " ^ tgt))
;;
-let pp_eager_statement_ast =
- GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
- ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+let pp_eager_statement_ast = GrafiteAstPp.pp_statement
let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
let parsed_text_length = String.length parsed_text in
(match current with
Some current ->
LexiconSync.time_travel ~present:current ~past:empty_lstatus;
- GrafiteSync.time_travel ~present:current ();
+ NCicLibrary.time_travel
+ ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus);
(* CSC: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate ()
| None -> ());
CicNotation2.load_notation ~include_paths:[] empty_lstatus
BuildTimeConf.core_notation_script
in
- let grafite_status = GrafiteSync.init lexicon_status baseuri in
+ let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
grafite_status
in
let read_include_paths file =
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 ();
+ NCicLibrary.time_travel grafite_status;
statements <- new_statements;
history <- new_history;
self#moveMark (- offset)