- | [] -> grafite_status, lexicon_status
- | ((grafite,lexicon),None)::_ -> grafite, lexicon
- | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
-
- with MatitaEngine.EnrichedWithLexiconStatus
- (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
- match f (get_macro_context (Some grafite_status)) with
- | _, GrafiteAst.Inline (_, style, suri, prefix) ->
- let str =
- ApplyTransformation.txt_of_inline_macro style suri prefix
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex") in
+ | [] -> grafite_status
+ | (g,None)::_ -> g
+ | (g,Some _)::_ ->
+ raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
+ with MatitaEngine.EnrichedWithStatus
+ (GrafiteEngine.Macro (floc, f), grafite) as exn ->
+ match f (get_macro_context (Some grafite)) with
+ | _, GrafiteAst.Inline (_, _suri, _params) ->
+(*
+ let str =
+ ApplyTransformation.txt_of_inline_macro style prefix suri
+ ?flavour
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ in