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:CicNotationPp.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
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
None status ctx menv subst (parsed_text,parsed_text_length,
- CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
| thms ->
String.concat ", "
(HExtlib.filter_map (function
- | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | NotationPt.NRef r -> Some (NCicPp.r2s true r)
| _ -> None)
thms)
in
[s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
-let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
- let module CTC = CicTypeChecker in
- (* no idea why ocaml wants this *)
- let parsed_text_length = String.length parsed_text in
- let dbd = LibraryDb.instance () in
- match mac with
- (* REAL macro *)
- | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false
- | TA.Eval (_, kind, term) -> assert false (* MATITA 1.0
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context =
- match user_goal with
- None -> []
- | Some n -> GrafiteTypes.get_proof_context grafite_status n in
- let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let term =
- match kind with
- | `Normalize ->
- CicReduction.normalize ~delta:true ~subst:[] context term
- | `Simpl ->
- ProofEngineReduction.simpl context term
- | `Unfold None ->
- ProofEngineReduction.unfold ?what:None context term
- | `Unfold (Some lazy_term) ->
- let what, _, _ =
- lazy_term context metasenv CicUniv.empty_ugraph in
- ProofEngineReduction.unfold ~what context term
- | `Whd ->
- CicReduction.whd ~delta:true ~subst:[] context term
- in
- let t_and_ty = Cic.Cast (term,ty) in
- guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [(grafite_status#set_proof_status No_proof), parsed_text ],"",
- parsed_text_length *)
- | TA.Inline (_, suri, params) ->
- let str = "\n\n" ^
- ApplyTransformation.txt_of_inline_macro
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- params suri
- in
- [], str, String.length parsed_text
-
-and eval_executable include_paths (buffer : GText.buffer) guistuff
+let rec eval_executable include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
script ex loc
=
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
- | GrafiteEngine.Macro (_loc,lazy_macro) ->
- let context = [] in
- let grafite_status,macro = lazy_macro context in
- eval_macro include_paths buffer guistuff grafite_status
- user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
| GrafiteEngine.NMacro (_loc,macro) ->
eval_nmacro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
(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)