tuned;
authorwenzelm
Tue, 10 Dec 2024 10:52:46 +0100
changeset 81567 a1ad3d1761fe
parent 81566 f207acb03ccb
child 81568 e88cf59244ee
tuned;
src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Sun Dec 08 20:13:40 2024 +0100
+++ b/src/Pure/General/latex.ML	Tue Dec 10 10:52:46 2024 +0100
@@ -243,9 +243,10 @@
 
 local
 
-val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
-val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
-val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
+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";
 
 fun latex_markup (s, _: Properties.T) =
   if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup