HLog.error "please create it.";
raise (Failure ("No root file for "^mafilename))
in
- let initial_lexicon_status =
- CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script
- in
- let b,x =
- try
- GrafiteSync.push ();
- LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
- let rc = MatitacLib.Make.make root [tgt] in
- GrafiteSync.pop ();
- CicNotation.reset ();
- ignore(CicNotation2.load_notation ~include_paths:[]
- BuildTimeConf.core_notation_script);
- let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
- initial_lexicon_status (List.rev
- x.LexiconEngine.lexicon_content_rev)
- in
- rc,x
- with
- | exn ->
- HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
- assert false
- in
+ let b = MatitacLib.Make.make root [tgt] in
if b then
try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
raise
[], "", parsed_text_length
| TA.WHint (loc, term) ->
let _subst = [] in
- let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in
+ let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
ProofEngineTypes.Fail _ as exn ->
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
- | TA.Inline (_,style,suri,prefix) ->
+ | TA.Inline (_,style,suri,prefix,flavour) ->
let str =
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- style suri prefix
+ style ?flavour prefix suri
in
[], str, String.length parsed_text