changeset 74789 | a5c23da73fca |
parent 74563 | 042041c0ebeb |
child 74790 | 3ce6fb9db485 |
--- a/src/Pure/System/scala_compiler.ML Sun Nov 14 21:52:13 2021 +0100 +++ b/src/Pure/System/scala_compiler.ML Mon Nov 15 11:38:14 2021 +0100 @@ -59,7 +59,7 @@ fun scala_name name = Latex.string (Latex.output_ascii_breakable "." name) - |> Latex.enclose_text "\\isatt{" "}"; + |> XML.enclose "\\isatt{" "}"; in