34841
|
1 |
/*
|
|
2 |
* Scala instance of Console plugin
|
|
3 |
*
|
|
4 |
* @author Makarius
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle.jedit
|
|
8 |
|
|
9 |
|
34844
|
10 |
import console.{Console, ConsolePane, Shell, Output}
|
34841
|
11 |
|
|
12 |
import org.gjt.sp.jedit.jEdit
|
|
13 |
import org.gjt.sp.jedit.MiscUtilities
|
|
14 |
|
|
15 |
import java.io.{Writer, PrintWriter}
|
|
16 |
|
|
17 |
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
|
|
18 |
|
|
19 |
|
|
20 |
class Scala_Console extends Shell("Scala")
|
|
21 |
{
|
|
22 |
private var interpreters = Map[Console, Interpreter]()
|
|
23 |
|
|
24 |
private var global_console: Console = null
|
|
25 |
private var global_out: Output = null
|
|
26 |
private var global_err: Output = null
|
|
27 |
|
34844
|
28 |
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
|
|
29 |
{
|
|
30 |
global_console = console
|
|
31 |
global_out = out
|
|
32 |
global_err = if (err == null) out else err
|
|
33 |
val res = Exn.capture { e }
|
|
34 |
global_console = null
|
|
35 |
global_out = null
|
|
36 |
global_err = null
|
|
37 |
Exn.release(res)
|
|
38 |
}
|
|
39 |
|
34841
|
40 |
private def report_error(str: String)
|
|
41 |
{
|
|
42 |
if (global_console == null || global_err == null) System.err.println(str)
|
|
43 |
else global_err.print(global_console.getErrorColor, str)
|
|
44 |
}
|
|
45 |
|
|
46 |
private class Console_Writer extends Writer
|
|
47 |
{
|
|
48 |
def close {}
|
|
49 |
def flush {}
|
|
50 |
|
|
51 |
def write(cbuf: Array[Char], off: Int, len: Int)
|
|
52 |
{
|
|
53 |
if (len > 0) write(new String(cbuf.subArray(off, off + len)))
|
|
54 |
}
|
|
55 |
|
|
56 |
override def write(str: String)
|
|
57 |
{
|
|
58 |
if (global_out == null) System.out.println(str)
|
|
59 |
else global_out.print(null, str)
|
|
60 |
}
|
|
61 |
}
|
|
62 |
|
|
63 |
override def openConsole(console: Console)
|
|
64 |
{
|
|
65 |
val settings = new GenericRunnerSettings(report_error)
|
|
66 |
val printer = new PrintWriter(new Console_Writer, true)
|
|
67 |
interpreters += (console -> new Interpreter(settings, printer))
|
|
68 |
}
|
|
69 |
|
|
70 |
override def closeConsole(console: Console)
|
|
71 |
{
|
|
72 |
interpreters -= console
|
|
73 |
}
|
|
74 |
|
|
75 |
override def printPrompt(console: Console, out: Output)
|
|
76 |
{
|
34844
|
77 |
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
|
|
78 |
out.writeAttrs(null," ")
|
34841
|
79 |
}
|
|
80 |
|
|
81 |
override def execute(console: Console, input: String, out: Output, err: Output, command: String)
|
|
82 |
{
|
34844
|
83 |
with_console(console, out, err) {
|
|
84 |
interpreters(console).interpret(command)
|
|
85 |
}
|
|
86 |
if (err != null) err.commandDone()
|
|
87 |
out.commandDone()
|
34841
|
88 |
}
|
|
89 |
}
|