antiquotations for Scala entities;

--- a/etc/symbols	Sun May 24 19:57:13 2020 +0000
+++ b/etc/symbols	Mon May 25 19:10:38 2020 +0200
@@ -419,6 +419,9 @@
 \<^prop>                argument: cartouche
 \<^scala>               argument: cartouche
 \<^scala_function>      argument: cartouche
+\<^scala_method>        argument: cartouche
+\<^scala_object>        argument: cartouche
+\<^scala_type>          argument: cartouche
 \<^session>             argument: cartouche
 \<^simproc>             argument: cartouche
 \<^sort>                argument: cartouche

--- a/lib/texinputs/isabellesym.sty	Sun May 24 19:57:13 2020 +0000
+++ b/lib/texinputs/isabellesym.sty	Mon May 25 19:10:38 2020 +0200
@@ -404,6 +404,9 @@
 \newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
 \newcommand{\isactrlscala}{\isakeywordcontrol{scala}}
 \newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}}
+\newcommand{\isactrlscalaUNDERSCOREmethod}{\isakeywordcontrol{scala{\isacharunderscore}method}}
+\newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}}
+\newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}}
 \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
 \newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
 \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}

--- a/src/Pure/System/scala_check.ML	Sun May 24 19:57:13 2020 +0000
+++ b/src/Pure/System/scala_check.ML	Mon May 25 19:10:38 2020 +0200
@@ -6,17 +6,76 @@
 
 signature SCALA_CHECK =
 sig
-  val decl: string -> unit
+  val declaration: string -> unit
 end;
 
 structure Scala_Check: SCALA_CHECK =
 struct
 
-fun decl source =
+(* check declaration *)
+
+fun declaration source =
   let val errors =
     \<^scala>\<open>scala_check\<close> source
     |> YXML.parse_body
     |> let open XML.Decode in list string end
   in if null errors then () else error (cat_lines errors) end;
 
+
+(* antiquotations *)
+
+local
+
+fun make_list bg en = space_implode "," #> enclose bg en;
+
+fun print_args [] = ""
+  | print_args xs = make_list "(" ")" xs;
+
+fun print_types [] = ""
+  | print_types Ts = make_list "[" "]" Ts;
+
+fun print_class (c, Ts) = c ^ print_types Ts;
+
+val types =
+  Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [];
+
+val in_class =
+  Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types  --| Parse.$$$ ")");
+
+val arguments =
+  (Parse.nat >> (fn n => replicate n "_") ||
+    Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args
+  || Scan.succeed " _";
+
+val method_arguments = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
+
+in
+
+val _ =
+  Theory.setup
+    (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close>
+      (Scan.lift (Parse.embedded -- (types >> print_types)))
+      (fn _ => fn (t, type_args) =>
+        (declaration ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #>
+
+    Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close>
+      (Scan.lift Parse.embedded)
+      (fn _ => fn object => (declaration ("val _test_ = " ^ object); object)) #>
+
+    Thy_Output.antiquotation_verbatim_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
+          val class_types = (case class of SOME (_, Ts) => Ts | NONE => []);
+          val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types));
+          val def_context =
+            (case class of
+              NONE => def ^ " = "
+            | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_.");
+          val source = def_context ^ method ^ method_args;
+          val _ = declaration source;
+        in (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end));
+
 end;
+
+end;