# HG changeset patch
# User wenzelm
# Date 1590432199 -7200
# Node ID feb37a43ace6f303a05ea6628b4950966d08a921
# Parent  f7d15620dd8ea04d1e5f99387c0098755b7ebfea
clarified signature;

diff -r f7d15620dd8e -r feb37a43ace6 src/Pure/ROOT.ML
--- 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";
diff -r f7d15620dd8e -r feb37a43ace6 src/Pure/System/scala.scala
--- 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))
diff -r f7d15620dd8e -r feb37a43ace6 src/Pure/System/scala_check.ML
--- 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;
diff -r f7d15620dd8e -r feb37a43ace6 src/Pure/System/scala_compiler.ML
--- /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;