--- a/src/Pure/System/scala.scala Sat Apr 09 12:07:51 2022 +0200
+++ b/src/Pure/System/scala.scala Sat Apr 09 12:29:39 2022 +0200
@@ -112,11 +112,15 @@
}
}
- def toplevel(source: String): List[String] = {
+ def toplevel(interpret: Boolean, source: String): List[String] = {
val out = new StringWriter
val interp = interpreter(new PrintWriter(out))
val marker = '\u000b'
- val ok = interp.withLabel(marker.toString) { (new interp.ReadEvalPrint).compile(source) }
+ val ok =
+ interp.withLabel(marker.toString) {
+ if (interpret) interp.interpret(source) == Results.Success
+ else (new interp.ReadEvalPrint).compile(source)
+ }
out.close()
val Error = """(?s)^\S* error: (.*)$""".r
@@ -131,9 +135,15 @@
object Toplevel extends Fun_String("scala_toplevel") {
val here = Scala_Project.here
- def apply(source: String): String = {
+ def apply(arg: String): String = {
+ val (interpret, source) =
+ YXML.parse_body(arg) match {
+ case Nil => (false, "")
+ case List(XML.Text(source)) => (false, source)
+ case body => import XML.Decode._; pair(bool, string)(body)
+ }
val errors =
- try { Compiler.context().toplevel(source) }
+ try { Compiler.context().toplevel(interpret, source) }
catch { case ERROR(msg) => List(msg) }
locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
--- a/src/Pure/System/scala_compiler.ML Sat Apr 09 12:07:51 2022 +0200
+++ b/src/Pure/System/scala_compiler.ML Sat Apr 09 12:29:39 2022 +0200
@@ -6,7 +6,7 @@
signature SCALA_COMPILER =
sig
- val toplevel: string -> unit
+ val toplevel: bool -> string -> unit
val static_check: string * Position.T -> unit
end;
@@ -15,15 +15,18 @@
(* check declaration *)
-fun toplevel source =
+fun toplevel interpret source =
let val errors =
- \<^scala>\<open>scala_toplevel\<close> source
+ (interpret, source)
+ |> let open XML.Encode in pair bool string end
+ |> YXML.string_of_body
+ |> \<^scala>\<open>scala_toplevel\<close>
|> YXML.parse_body
|> let open XML.Decode in list string end
in if null errors then () else error (cat_lines errors) end;
fun static_check (source, pos) =
- toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
+ toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
handle ERROR msg => error (msg ^ Position.here pos);