# HG changeset patch
# User wenzelm
# Date 1590578537 -7200
# Node ID f08cf9d8f90b6bdb46e2153ccaa621127d23ac7f
# Parent  9a12eb655f67debbde6c097e8ff69ae86e56ff1f
breakable scala_name;

diff -r 9a12eb655f67 -r f08cf9d8f90b src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML	Tue May 26 22:45:05 2020 +0200
+++ b/src/Pure/System/scala_compiler.ML	Wed May 27 13:22:17 2020 +0200
@@ -53,6 +53,10 @@
 
 val method_arguments = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
 
+fun scala_name name =
+  let val latex = Latex.string (Latex.output_ascii_breakable "." name)
+  in Latex.enclose_block "\\isatt{" "}" [latex] end;
+
 in
 
 val _ =
@@ -60,16 +64,17 @@
     (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close>
       (Scan.lift Parse.embedded) (fn _ => tap static_check) #>
 
-    Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close>
+    Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_type\<close>
       (Scan.lift (Parse.embedded -- (types >> print_types)))
       (fn _ => fn (t, type_args) =>
-        (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #>
+        (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args);
+          scala_name (t ^ type_args))) #>
 
-    Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close>
+    Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_object\<close>
       (Scan.lift Parse.embedded)
-      (fn _ => fn object => (static_check ("val _test_ = " ^ object); object)) #>
+      (fn _ => fn object => (static_check ("val _test_ = " ^ object); scala_name object)) #>
 
-    Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_method\<close>
+    Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_method\<close>
       (Scan.lift (Scan.option in_class -- Parse.embedded -- types -- method_arguments))
       (fn _ => fn (((class, method), method_types), method_args) =>
         let
@@ -81,7 +86,7 @@
             | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_.");
           val source = def_context ^ method ^ method_args;
           val _ = static_check source;
-        in (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end));
+        in scala_name (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end));
 
 end;