# HG changeset patch
# User wenzelm
# Date 1590005261 -7200
# Node ID f640380aaf86fa4581ef897a4df9d15c12722c36
# Parent  265bbad3d6af8ea7e1c625721882c5f2ae5cd352
clarified signature;

diff -r 265bbad3d6af -r f640380aaf86 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Wed May 20 20:45:43 2020 +0200
+++ b/src/Pure/System/scala.scala	Wed May 20 22:07:41 2020 +0200
@@ -8,12 +8,39 @@
 
 
 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+import java.io.{File => JFile}
 
 import scala.util.matching.Regex
+import scala.tools.nsc.GenericRunnerSettings
 
 
 object Scala
 {
+  /* compiler classpath and settings */
+
+  def compiler_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 =
+      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+
+    (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+  }
+
+  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
+  }
+
+
+
   /** invoke JVM method via Isabelle/Scala **/
 
   /* method reflection */
diff -r 265bbad3d6af -r f640380aaf86 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Wed May 20 20:45:43 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Wed May 20 22:07:41 2020 +0200
@@ -25,23 +25,9 @@
 {
   /* reconstructed jEdit/plugin classpath */
 
-  private def reconstruct_classpath(): String =
-  {
-    def find_jars(start: String): List[String] =
-      if (start != null)
-        File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
-          map(File.absolute_name)
-      else Nil
-
-    val initial_class_path =
-      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
-
-    val path =
-      initial_class_path :::
-      find_jars(jEdit.getSettingsDirectory) :::
-      find_jars(jEdit.getJEditHome)
-    path.mkString(JFile.pathSeparator)
-  }
+  private def jar_dirs: List[JFile] =
+    (proper_string(jEdit.getSettingsDirectory).toList :::
+     proper_string(jEdit.getJEditHome).toList).map(new JFile(_))
 
 
   /* global state -- owned by GUI thread */
@@ -127,8 +113,7 @@
     private val running = Synchronized[Option[Thread]](None)
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
-    private val settings = new GenericRunnerSettings(report_error)
-    settings.classpath.value = reconstruct_classpath()
+    private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs)
 
     private val interp = new IMain(settings, new PrintWriter(console_writer, true))
     {