# HG changeset patch # User wenzelm # Date 1733838176 -3600 # Node ID e88cf59244ee8b77248321cd5257ef24d5600947 # Parent a1ad3d1761fe54d53189ae05cae184875174e80d tuned; diff -r a1ad3d1761fe -r e88cf59244ee src/Pure/General/latex.ML --- a/src/Pure/General/latex.ML Tue Dec 10 10:52:46 2024 +0100 +++ b/src/Pure/General/latex.ML Tue Dec 10 14:42:56 2024 +0100 @@ -243,15 +243,19 @@ local -val macro_markup = YXML.output_markup o Markup.latex_macro; -val command_markup = macro_markup "isacommand"; -val keyword_markup = macro_markup "isakeyword"; -val indent_markup = macro_markup "isaindent"; +val markup_macro = YXML.output_markup o Markup.latex_macro; +val markup_indent = markup_macro "isaindent"; +val markup_latex = + Symtab.make + [(Markup.commandN, markup_macro "isacommand"), + (Markup.keyword1N, markup_macro "isacommand"), + (Markup.keyword2N, markup_macro "isakeyword"), + (Markup.keyword3N, markup_macro"isacommand") + ]; -fun latex_markup (s, _: Properties.T) = - if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup - else if s = Markup.keyword2N then keyword_markup - else Markup.no_output; +fun latex_markup (a, props) = + (if Markup.has_syntax props then NONE else Symtab.lookup markup_latex a) + |> the_default Markup.no_output; fun latex_markup_output (bg, en) = (case try YXML.parse (bg ^ en) of @@ -259,7 +263,7 @@ | _ => Markup.no_output); fun latex_indent s (_: int) = - if s = "" then s else uncurry enclose indent_markup s; + if s = "" then s else uncurry enclose markup_indent s; in