src/Pure/System/scala_compiler.ML
changeset 74790 3ce6fb9db485
parent 74789 a5c23da73fca
child 75417 2c861b196d52
--- a/src/Pure/System/scala_compiler.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/System/scala_compiler.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -58,8 +58,7 @@
 val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
 
 fun scala_name name =
-  Latex.string (Latex.output_ascii_breakable "." name)
-  |> XML.enclose "\\isatt{" "}";
+  Latex.macro "isatt" (Latex.string (Latex.output_ascii_breakable "." name));
 
 in