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