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@34841: import java.io.{Writer, PrintWriter}
wenzelm@34841: 
wenzelm@34841: import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
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@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@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@34845: 
wenzelm@34845:     val view = console.getView
wenzelm@34845:     val edit_pane = view.getEditPane
wenzelm@34845:     interp.bind("view", "org.gjt.sp.jedit.View", view)
wenzelm@34845:     interp.bind("editPane", "org.gjt.sp.jedit.EditPane", edit_pane)
wenzelm@34845:     interp.bind("buffer", "org.gjt.sp.jedit.Buffer", edit_pane.getBuffer)
wenzelm@34845:     interp.bind("textArea", "org.gjt.sp.jedit.textarea.JEditTextArea", edit_pane.getTextArea)
wenzelm@34845:     interp.bind("wm", "org.gjt.sp.jedit.gui.DockableWindowManager", view.getDockableWindowManager)
wenzelm@34845: 
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@34845:     with_console(console, out, err) { interpreters(console).interpret(command) }
wenzelm@34844:     if (err != null) err.commandDone()
wenzelm@34844: 		out.commandDone()
wenzelm@34841:   }
wenzelm@34841: }