--- 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;