# HG changeset patch
# User wenzelm
# Date 1650534593 -7200
# Node ID d6f2fbdc6322841f9fa9701da570abfab9d0a0b3
# Parent  d5041b68a2374a4a7965feb5b3794a68fa41e3b3
clarified signature;

diff -r d5041b68a237 -r d6f2fbdc6322 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Thu Apr 21 11:28:50 2022 +0200
+++ b/src/Pure/System/scala.scala	Thu Apr 21 11:49:53 2022 +0200
@@ -80,7 +80,11 @@
     } yield elem
 
   object Compiler {
+    def default_print_writer: PrintWriter =
+      new NewLinePrintWriter(new ConsoleWriter, true)
+
     def context(
+      print_writer: PrintWriter = default_print_writer,
       error: String => Unit = Exn.error,
       jar_dirs: List[JFile] = Nil,
       class_loader: Option[ClassLoader] = None
@@ -93,43 +97,40 @@
       settings.classpath.value =
         (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
-      new Context(settings, class_loader)
+      new Context(settings, print_writer, class_loader)
     }
 
-    def default_print_writer: PrintWriter =
-      new NewLinePrintWriter(new ConsoleWriter, true)
-
     class Context private [Compiler](
       val settings: GenericRunnerSettings,
+      val print_writer: PrintWriter,
       val class_loader: Option[ClassLoader]
     ) {
       override def toString: String = settings.toString
 
-      def interpreter(print_writer: PrintWriter = default_print_writer): IMain = {
+      val interp: IMain =
         new IMain(settings, new ReplReporterImpl(settings, print_writer)) {
           override def parentClassLoader: ClassLoader =
             class_loader getOrElse super.parentClassLoader
         }
-      }
+    }
 
-      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) {
-            if (interpret) interp.interpret(source) == Results.Success
-            else (new interp.ReadEvalPrint).compile(source)
-          }
-        out.close()
+    def toplevel(interpret: Boolean, source: String): List[String] = {
+      val out = new StringWriter
+      val interp = Compiler.context(print_writer = new PrintWriter(out)).interp
+      val marker = '\u000b'
+      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
-        val errors =
-          space_explode(marker, Library.strip_ansi_color(out.toString)).
-            collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
+      val Error = """(?s)^\S* error: (.*)$""".r
+      val errors =
+        space_explode(marker, Library.strip_ansi_color(out.toString)).
+          collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
-        if (!ok && errors.isEmpty) List("Error") else errors
-      }
+      if (!ok && errors.isEmpty) List("Error") else errors
     }
   }
 
@@ -143,7 +144,7 @@
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
-        try { Compiler.context().toplevel(interpret, source) }
+        try { Compiler.toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
diff -r d5041b68a237 -r d6f2fbdc6322 src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Thu Apr 21 11:28:50 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Thu Apr 21 11:49:53 2022 +0200
@@ -93,10 +93,10 @@
 
     private val interp =
       Scala.Compiler.context(
+          print_writer = new PrintWriter(console_writer, true),
           error = report_error,
           jar_dirs = JEdit_Lib.directories,
-          class_loader = Some(new JARClassLoader)).
-        interpreter(new PrintWriter(console_writer, true))
+          class_loader = Some(new JARClassLoader)).interp
 
     val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") {
       case Start(console) =>