--- 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 */
--- 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))
{