--- a/src/Pure/ROOT.ML Mon May 25 19:10:38 2020 +0200
+++ b/src/Pure/ROOT.ML Mon May 25 20:43:19 2020 +0200
@@ -328,7 +328,7 @@
ML_file "System/message_channel.ML";
ML_file "System/isabelle_process.ML";
ML_file "System/scala.ML";
-ML_file "System/scala_check.ML";
+ML_file "System/scala_compiler.ML";
ML_file "Thy/bibtex.ML";
ML_file "PIDE/protocol.ML";
ML_file "General/output_primitives_virtual.ML";
--- a/src/Pure/System/scala.scala Mon May 25 19:10:38 2020 +0200
+++ b/src/Pure/System/scala.scala Mon May 25 20:43:19 2020 +0200
@@ -77,18 +77,14 @@
if (!ok && errors.isEmpty) List("Error") else errors
}
-
- def check(body: String): List[String] =
- {
- try { toplevel("package test\nobject Test { " + body + " }") }
- catch { case ERROR(msg) => List(msg) }
- }
}
}
- def check_yxml(body: String): String =
+ def toplevel_yxml(source: String): String =
{
- val errors = Compiler.default_context.check(body)
+ val errors =
+ try { Compiler.default_context.toplevel(source) }
+ catch { case ERROR(msg) => List(msg) }
locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
@@ -199,5 +195,5 @@
class Functions extends Isabelle_Scala_Functions(
Scala.Fun("echo", identity),
- Scala.Fun("scala_check", Scala.check_yxml),
+ Scala.Fun("scala_toplevel", Scala.toplevel_yxml),
Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
--- a/src/Pure/System/scala_check.ML Mon May 25 19:10:38 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-(* Title: Pure/System/scala_check.ML
- Author: Makarius
-
-Semantic check of Scala sources.
-*)
-
-signature SCALA_CHECK =
-sig
- val declaration: string -> unit
-end;
-
-structure Scala_Check: SCALA_CHECK =
-struct
-
-(* 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala_compiler.ML Mon May 25 20:43:19 2020 +0200
@@ -0,0 +1,85 @@
+(* Title: Pure/System/scala_compiler.ML
+ Author: Makarius
+
+Scala compiler operations.
+*)
+
+signature SCALA_COMPILER =
+sig
+ val toplevel: string -> unit
+ val declaration: string -> unit
+end;
+
+structure Scala_Compiler: SCALA_COMPILER =
+struct
+
+(* check declaration *)
+
+fun toplevel source =
+ let val errors =
+ \<^scala>\<open>scala_toplevel\<close> source
+ |> YXML.parse_body
+ |> let open XML.Decode in list string end
+ in if null errors then () else error (cat_lines errors) end;
+
+fun declaration source =
+ toplevel ("package test\nobject Test { " ^ source ^ " }");
+
+
+(* 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;