src/Tools/jEdit/src/scala_console.scala
changeset 48409 0d2114eb412a
parent 47992 7700f0e9618c
child 48412 dbd75cbb84ba
equal deleted inserted replaced
48374:623607c5a40f 48409:0d2114eb412a
    13 
    13 
    14 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    14 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    15 import org.gjt.sp.jedit.MiscUtilities
    15 import org.gjt.sp.jedit.MiscUtilities
    16 
    16 
    17 import java.lang.System
    17 import java.lang.System
    18 import java.io.{File, OutputStream, Writer, PrintWriter}
    18 import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
    19 
    19 
    20 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    20 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    21 import scala.tools.nsc.interpreter.IMain
    21 import scala.tools.nsc.interpreter.IMain
    22 import scala.collection.mutable
    22 import scala.collection.mutable
    23 
    23 
    28 
    28 
    29   private def reconstruct_classpath(): String =
    29   private def reconstruct_classpath(): String =
    30   {
    30   {
    31     def find_jars(start: String): List[String] =
    31     def find_jars(start: String): List[String] =
    32       if (start != null)
    32       if (start != null)
    33         Standard_System.find_files(new File(start),
    33         Standard_System.find_files(new JFile(start),
    34           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    34           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    35       else Nil
    35       else Nil
    36     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    36     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    37     path.mkString(File.pathSeparator)
    37     path.mkString(JFile.pathSeparator)
    38   }
    38   }
    39 
    39 
    40 
    40 
    41   /* global state -- owned by Swing thread */
    41   /* global state -- owned by Swing thread */
    42 
    42