[], "", 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