# HG changeset patch
# User wenzelm
# Date 1590155627 -7200
# Node ID bfc120aa737a562e54097b02a485c433ad8e6504
# Parent  e95ea6956df39d30eafdfd0c20d14f5680245b9c
clarified signature;
more operations;

diff -r e95ea6956df3 -r bfc120aa737a src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Fri May 22 13:53:19 2020 +0200
+++ b/src/Pure/System/scala.scala	Fri May 22 15:53:47 2020 +0200
@@ -7,40 +7,62 @@
 package isabelle
 
 
-import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.io.{File => JFile}
+import java.lang.reflect.{Modifier, InvocationTargetException}
+import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.util.matching.Regex
 import scala.tools.nsc.GenericRunnerSettings
+import scala.tools.nsc.interpreter.IMain
 
 
 object Scala
 {
-  /* compiler classpath and settings */
+  /* compiler */
 
-  def compiler_classpath(jar_dirs: List[JFile]): String =
+  object Compiler
   {
-    def find_jars(dir: JFile): List[String] =
-      File.find_files(dir, file => file.getName.endsWith(".jar")).
-        map(File.absolute_name)
+    def classpath(jar_dirs: List[JFile]): String =
+    {
+      def find_jars(dir: JFile): List[String] =
+        File.find_files(dir, file => file.getName.endsWith(".jar")).
+          map(File.absolute_name)
+
+      val class_path =
+        for {
+          prop <- List("scala.boot.class.path", "java.class.path")
+          path = System.getProperty(prop, "") if path != "\"\""
+          elem <- space_explode(JFile.pathSeparatorChar, path)
+        } yield elem
+
+      (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+    }
+
+    type Settings = scala.tools.nsc.Settings
 
-    val class_path =
-      for {
-        prop <- List("scala.boot.class.path", "java.class.path")
-        path = System.getProperty(prop, "") if path != "\"\""
-        elem <- space_explode(JFile.pathSeparatorChar, path)
-      } yield elem
+    def settings(
+      error: String => Unit = Exn.error,
+      jar_dirs: List[JFile] = Nil): Settings =
+    {
+      val settings = new GenericRunnerSettings(error)
+      settings.classpath.value = classpath(jar_dirs)
+      settings
+    }
 
-    (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
-  }
+    def toplevel(settings: Settings, source: String): List[String] =
+    {
+      val out = new StringWriter
+      val interp = new IMain(settings, new PrintWriter(out))
+      val rep = new interp.ReadEvalPrint
+      val ok = interp.withLabel("\u0001") { rep.compile(source) }
+      out.close
 
-  def compiler_settings(
-    error: String => Unit = Exn.error,
-    jar_dirs: List[JFile] = Nil): GenericRunnerSettings =
-  {
-    val settings = new GenericRunnerSettings(error)
-    settings.classpath.value = compiler_classpath(jar_dirs)
-    settings
+      val Error = """(?s)^\S* error: (.*)$""".r
+      val errors =
+        space_explode('\u0001', Library.strip_ansi_color(out.toString)).
+          collect({ case Error(msg) => Word.capitalize(Library.trim_line(msg)) })
+
+      if (!ok && errors.isEmpty) List("Error") else errors
+    }
   }
 
 
diff -r e95ea6956df3 -r bfc120aa737a src/Pure/library.scala
--- a/src/Pure/library.scala	Fri May 22 13:53:19 2020 +0200
+++ b/src/Pure/library.scala	Fri May 22 15:53:47 2020 +0200
@@ -144,6 +144,9 @@
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
+  def strip_ansi_color(s: String): String =
+    s.replaceAll("""\u001b\[\d+m""", "")
+
 
   /* quote */
 
diff -r e95ea6956df3 -r bfc120aa737a src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 22 13:53:19 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 22 15:53:47 2020 +0200
@@ -101,7 +101,7 @@
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
     private val settings =
-      Scala.compiler_settings(error = report_error, jar_dirs = JEdit_Lib.directories)
+      Scala.Compiler.settings(error = report_error, jar_dirs = JEdit_Lib.directories)
 
     private val interp = new IMain(settings, new PrintWriter(console_writer, true))
     {