check Scala source snippets from ML;

--- a/src/Pure/System/scala.ML	Sat May 23 21:43:30 2020 +0200
+++ b/src/Pure/System/scala.ML	Sat May 23 21:58:44 2020 +0200
@@ -10,6 +10,7 @@
   val function: string -> string -> string
   val function_yxml: string -> XML.body -> XML.body
   exception Null
+  val check: string -> unit
 end;
 
 structure Scala: SCALA =
@@ -70,4 +71,15 @@
       fulfill id tag res
         handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
+
+
+(** check source snippet **)
+
+fun check source =
+  let val errors =
+    function "scala_check" source
+    |> YXML.parse_body
+    |> let open XML.Decode in list string end
+  in if null errors then () else error (cat_lines errors) end;
+
 end;

--- a/src/Pure/System/scala.scala	Sat May 23 21:43:30 2020 +0200
+++ b/src/Pure/System/scala.scala	Sat May 23 21:58:44 2020 +0200
@@ -79,9 +79,21 @@
 
         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 =
+  {
+    val errors = Compiler.default_context.check(body)
+    locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
+  }
+
 
 
   /** invoke Scala functions from ML **/
@@ -198,4 +210,5 @@
 class Functions extends Isabelle_Scala_Functions(
   Scala.Fun("echo", identity),
   Scala.Fun.yxml("echo_yxml", identity),
+  Scala.Fun("scala_check", Scala.check_yxml),
   Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))