# HG changeset patch
# User wenzelm
# Date 1590139806 -7200
# Node ID 1330fa4a2b85a17d5311790a77ff52b26f2be5a1
# Parent  6a51e64ba13df930acc4aae03bd01ade34931b9f
clarified signature;

diff -r 6a51e64ba13d -r 1330fa4a2b85 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu May 21 20:00:09 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 22 11:30:06 2020 +0200
@@ -25,6 +25,12 @@
 
 object JEdit_Lib
 {
+  /* jEdit directories */
+
+  def directories: List[JFile] =
+    (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
+
+
   /* location within multi-screen environment */
 
   final case class Screen_Location(point: Point, bounds: Rectangle)
diff -r 6a51e64ba13d -r 1330fa4a2b85 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Thu May 21 20:00:09 2020 +0000
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 22 11:30:06 2020 +0200
@@ -23,13 +23,6 @@
 
 class Scala_Console extends Shell("Scala")
 {
-  /* reconstructed jEdit/plugin classpath */
-
-  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 */
 
   @volatile private var interpreters = Map.empty[Console, Interpreter]
@@ -113,7 +106,8 @@
     private val running = Synchronized[Option[Thread]](None)
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
-    private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs)
+    private val settings =
+      Scala.compiler_settings(error = report_error, jar_dirs = JEdit_Lib.directories)
 
     private val interp = new IMain(settings, new PrintWriter(console_writer, true))
     {