wenzelm@34841: /*
wenzelm@34841:  * Scala instance of Console plugin
wenzelm@34841:  *
wenzelm@34841:  * @author Makarius
wenzelm@34841:  */
wenzelm@34841: 
wenzelm@34841: package isabelle.jedit
wenzelm@34841: 
wenzelm@34841: 
wenzelm@34844: import console.{Console, ConsolePane, Shell, Output}
wenzelm@34841: 
wenzelm@34845: import org.gjt.sp.jedit.{jEdit, JARClassLoader}
wenzelm@34841: import org.gjt.sp.jedit.MiscUtilities
wenzelm@34841: 
wenzelm@34846: import java.io.{File, Writer, PrintWriter}
wenzelm@34841: 
wenzelm@34841: import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
wenzelm@34846: import scala.collection.mutable
wenzelm@34841: 
wenzelm@34841: 
wenzelm@34841: class Scala_Console extends Shell("Scala")
wenzelm@34841: {
wenzelm@34841:   private var interpreters = Map[Console, Interpreter]()
wenzelm@34841: 
wenzelm@34841:   private var global_console: Console = null
wenzelm@34841:   private var global_out: Output = null
wenzelm@34841:   private var global_err: Output = null
wenzelm@34841: 
wenzelm@34844:   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
wenzelm@34844:   {
wenzelm@34844:     global_console = console
wenzelm@34844:     global_out = out
wenzelm@34844:     global_err = if (err == null) out else err
wenzelm@34844:     val res = Exn.capture { e }
wenzelm@34844:     global_console = null
wenzelm@34844:     global_out = null
wenzelm@34844:     global_err = null
wenzelm@34844:     Exn.release(res)
wenzelm@34844:   }
wenzelm@34844: 
wenzelm@34841:   private def report_error(str: String)
wenzelm@34841:   {
wenzelm@34841:     if (global_console == null || global_err == null) System.err.println(str)
wenzelm@34841:     else global_err.print(global_console.getErrorColor, str)
wenzelm@34841:   }
wenzelm@34841: 
wenzelm@34846:   private def construct_classpath(): String =
wenzelm@34846:   {
wenzelm@34846:     def find_jars(start: String): List[String] =
wenzelm@34846:       if (start != null)
wenzelm@34846:         Standard_System.find_files(new File(start),
wenzelm@34846:           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
wenzelm@34846:       else Nil
wenzelm@34846:     val path =
wenzelm@34846:       (jEdit.getJEditHome + File.separator + "jedit.jar") ::
wenzelm@34846:         (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome))
wenzelm@34846:      path.mkString(File.pathSeparator)
wenzelm@34846:   }
wenzelm@34846: 
wenzelm@34841:   private class Console_Writer extends Writer
wenzelm@34841:   {
wenzelm@34841:     def close {}
wenzelm@34841:     def flush {}
wenzelm@34841: 
wenzelm@34841:     def write(cbuf: Array[Char], off: Int, len: Int)
wenzelm@34841:     {
wenzelm@34841:       if (len > 0) write(new String(cbuf.subArray(off, off + len)))
wenzelm@34841:     }
wenzelm@34841: 
wenzelm@34841:     override def write(str: String)
wenzelm@34841:     {
wenzelm@34841:       if (global_out == null) System.out.println(str)
wenzelm@34841:       else global_out.print(null, str)
wenzelm@34841:     }
wenzelm@34841:   }
wenzelm@34841: 
wenzelm@34841:   override def openConsole(console: Console)
wenzelm@34841:   {
wenzelm@34841:     val settings = new GenericRunnerSettings(report_error)
wenzelm@34846:     settings.classpath.value = construct_classpath()
wenzelm@34841:     val printer = new PrintWriter(new Console_Writer, true)
wenzelm@34845:     val interp = new Interpreter(settings, printer)
wenzelm@34845:     {
wenzelm@34845:       override def parentClassLoader = new JARClassLoader
wenzelm@34845:     }
wenzelm@34845:     interp.setContextClassLoader
wenzelm@34846:     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
wenzelm@34845:     interpreters += (console -> interp)
wenzelm@34841:   }
wenzelm@34841: 
wenzelm@34841:   override def closeConsole(console: Console)
wenzelm@34841:   {
wenzelm@34841:     interpreters -= console
wenzelm@34841:   }
wenzelm@34841: 
wenzelm@34841:   override def printPrompt(console: Console, out: Output)
wenzelm@34841: 	{
wenzelm@34844:     out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
wenzelm@34845: 		out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
wenzelm@34841: 	}
wenzelm@34841: 
wenzelm@34841:   override def execute(console: Console, input: String, out: Output, err: Output, command: String)
wenzelm@34841:   {
wenzelm@34846:     val interp = interpreters(console)
wenzelm@34846:     with_console(console, out, err) { interp.interpret(command) }
wenzelm@34844:     if (err != null) err.commandDone()
wenzelm@34844: 		out.commandDone()
wenzelm@34841:   }
wenzelm@34841: }