clarified signature;
authorwenzelm
Fri, 22 May 2020 11:30:06 +0200
changeset 71861 1330fa4a2b85
parent 71854 6a51e64ba13d
child 71862 8bbadb065ebe
clarified signature;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/scala_console.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)
--- 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))
     {