# HG changeset patch # User wenzelm # Date 1649404729 -7200 # Node ID 2c861b196d522314f2be17f9d93ca44b6f8f075f # Parent 39aa4d9e5559f8a7759d4bff993b061b0640fe06 removed unused flag (see 25c6423ec538); diff -r 39aa4d9e5559 -r 2c861b196d52 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Thu Apr 07 20:15:58 2022 +0200 +++ b/src/Pure/System/scala.scala Fri Apr 08 09:58:49 2022 +0200 @@ -112,15 +112,11 @@ } } - def toplevel(interpret: Boolean, source: String): List[String] = { + def toplevel(source: String): List[String] = { val out = new StringWriter val interp = interpreter(new PrintWriter(out)) val marker = '\u000b' - val ok = - interp.withLabel(marker.toString) { - if (interpret) interp.interpret(source) == Results.Success - else (new interp.ReadEvalPrint).compile(source) - } + val ok = interp.withLabel(marker.toString) { (new interp.ReadEvalPrint).compile(source) } out.close() val Error = """(?s)^\S* error: (.*)$""".r @@ -135,15 +131,9 @@ object Toplevel extends Fun_String("scala_toplevel") { val here = Scala_Project.here - 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) - } + def apply(source: String): String = { val errors = - try { Compiler.context().toplevel(interpret, source) } + try { Compiler.context().toplevel(source) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } diff -r 39aa4d9e5559 -r 2c861b196d52 src/Pure/System/scala_compiler.ML --- a/src/Pure/System/scala_compiler.ML Thu Apr 07 20:15:58 2022 +0200 +++ b/src/Pure/System/scala_compiler.ML Fri Apr 08 09:58:49 2022 +0200 @@ -6,7 +6,7 @@ signature SCALA_COMPILER = sig - val toplevel: bool -> string -> unit + val toplevel: string -> unit val static_check: string * Position.T -> unit end; @@ -15,18 +15,15 @@ (* check declaration *) -fun toplevel interpret source = +fun toplevel source = let val errors = - (interpret, source) - |> let open XML.Encode in pair bool string end - |> YXML.string_of_body - |> \<^scala>\scala_toplevel\ + \<^scala>\scala_toplevel\ source |> 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 false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }") + toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }") handle ERROR msg => error (msg ^ Position.here pos);