src/Tools/jEdit/jedit_main/scala_console.scala
changeset 75702 97e8f4c938bf
parent 75654 21164fd15e3d
equal deleted inserted replaced
75701:84990c95712d 75702:97e8f4c938bf
    88   /* jEdit console methods */
    88   /* jEdit console methods */
    89 
    89 
    90   override def openConsole(console: Console): Unit = {
    90   override def openConsole(console: Console): Unit = {
    91     val context =
    91     val context =
    92       Scala.Compiler.context(
    92       Scala.Compiler.context(
    93       jar_dirs = JEdit_Lib.directories,
    93       jar_files = JEdit_Lib.directories,
    94       class_loader = Some(new JARClassLoader))
    94       class_loader = Some(new JARClassLoader))
    95 
    95 
    96     val interpreter = new Scala_Console.Interpreter(context, console)
    96     val interpreter = new Scala_Console.Interpreter(context, console)
    97     interpreter.execute((context, state) =>
    97     interpreter.execute((context, state) =>
    98       context.compile(Scala_Console.init, state = state).state)
    98       context.compile(Scala_Console.init, state = state).state)