clarified signature: proper eval/print via interpret;
authorwenzelm
Fri, 25 Sep 2020 13:28:28 +0200
changeset 72294 25c6423ec538
parent 72293 584aea0b29bb
child 72295 aafec95bc30e
clarified signature: proper eval/print via interpret;
src/Pure/System/scala.scala
src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala.scala	Fri Sep 25 11:24:28 2020 +0200
+++ b/src/Pure/System/scala.scala	Fri Sep 25 13:28:28 2020 +0200
@@ -10,7 +10,7 @@
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
-import scala.tools.nsc.interpreter.IMain
+import scala.tools.nsc.interpreter.{IMain, Results}
 
 
 object Scala
@@ -100,12 +100,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 rep = new interp.ReadEvalPrint
-        val ok = interp.withLabel("\u0001") { rep.compile(source) }
+        val ok =
+          interp.withLabel("\u0001") {
+            if (interpret) interp.interpret(source) == Results.Success
+            else (new interp.ReadEvalPrint).compile(source)
+          }
         out.close
 
         val Error = """(?s)^\S* error: (.*)$""".r
@@ -120,10 +123,16 @@
 
   object Toplevel extends Fun("scala_toplevel")
   {
-    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	Fri Sep 25 11:24:28 2020 +0200
+++ b/src/Pure/System/scala_compiler.ML	Fri Sep 25 13:28:28 2020 +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);