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