author | wenzelm |
Sat, 09 Jan 2010 22:03:47 +0100 | |
changeset 34849 | 96bcb91b45ce |
parent 34846 | ca76b3978540 |
child 34850 | fdd560e80264 |
permissions | -rw-r--r-- |
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 |
|
34845 | 12 |
import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
34841 | 13 |
import org.gjt.sp.jedit.MiscUtilities |
14 |
||
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
15 |
import java.io.{File, Writer, PrintWriter} |
34841 | 16 |
|
17 |
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} |
|
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
18 |
import scala.collection.mutable |
34841 | 19 |
|
20 |
||
21 |
class Scala_Console extends Shell("Scala") |
|
22 |
{ |
|
34849 | 23 |
/* global state -- owned by Swing thread */ |
24 |
||
34841 | 25 |
private var interpreters = Map[Console, Interpreter]() |
26 |
||
27 |
private var global_console: Console = null |
|
28 |
private var global_out: Output = null |
|
29 |
private var global_err: Output = null |
|
30 |
||
34844 | 31 |
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = |
32 |
{ |
|
33 |
global_console = console |
|
34 |
global_out = out |
|
35 |
global_err = if (err == null) out else err |
|
36 |
val res = Exn.capture { e } |
|
37 |
global_console = null |
|
38 |
global_out = null |
|
39 |
global_err = null |
|
40 |
Exn.release(res) |
|
41 |
} |
|
42 |
||
34841 | 43 |
private def report_error(str: String) |
44 |
{ |
|
45 |
if (global_console == null || global_err == null) System.err.println(str) |
|
46 |
else global_err.print(global_console.getErrorColor, str) |
|
47 |
} |
|
48 |
||
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
49 |
private def construct_classpath(): String = |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
50 |
{ |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
51 |
def find_jars(start: String): List[String] = |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
52 |
if (start != null) |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
53 |
Standard_System.find_files(new File(start), |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
54 |
entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
55 |
else Nil |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
56 |
val path = |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
57 |
(jEdit.getJEditHome + File.separator + "jedit.jar") :: |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
58 |
(find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)) |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
59 |
path.mkString(File.pathSeparator) |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
60 |
} |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
61 |
|
34841 | 62 |
private class Console_Writer extends Writer |
63 |
{ |
|
64 |
def close {} |
|
65 |
def flush {} |
|
66 |
||
67 |
override def write(str: String) |
|
68 |
{ |
|
69 |
if (global_out == null) System.out.println(str) |
|
70 |
else global_out.print(null, str) |
|
71 |
} |
|
34849 | 72 |
|
73 |
def write(cbuf: Array[Char], off: Int, len: Int) |
|
74 |
{ |
|
75 |
if (len > 0) write(new String(cbuf.subArray(off, off + len))) |
|
76 |
} |
|
34841 | 77 |
} |
78 |
||
79 |
override def openConsole(console: Console) |
|
80 |
{ |
|
81 |
val settings = new GenericRunnerSettings(report_error) |
|
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
82 |
settings.classpath.value = construct_classpath() |
34841 | 83 |
val printer = new PrintWriter(new Console_Writer, true) |
34849 | 84 |
|
34845 | 85 |
val interp = new Interpreter(settings, printer) |
86 |
{ |
|
87 |
override def parentClassLoader = new JARClassLoader |
|
88 |
} |
|
89 |
interp.setContextClassLoader |
|
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
90 |
interp.bind("view", "org.gjt.sp.jedit.View", console.getView) |
34849 | 91 |
interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session) |
34845 | 92 |
interpreters += (console -> interp) |
34841 | 93 |
} |
94 |
||
95 |
override def closeConsole(console: Console) |
|
96 |
{ |
|
97 |
interpreters -= console |
|
98 |
} |
|
99 |
||
34849 | 100 |
override def printInfoMessage(out: Output) |
101 |
{ |
|
102 |
out.print(null, |
|
103 |
"This shell evaluates Isabelle/Scala expressions.\n\n" + |
|
104 |
"The following special toplevel bindings are provided:\n" + |
|
105 |
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + |
|
106 |
" session -- Isabelle session (e.g. session.isabelle_system)\n") |
|
107 |
} |
|
108 |
||
34841 | 109 |
override def printPrompt(console: Console, out: Output) |
110 |
{ |
|
34844 | 111 |
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") |
34845 | 112 |
out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") |
34841 | 113 |
} |
114 |
||
115 |
override def execute(console: Console, input: String, out: Output, err: Output, command: String) |
|
116 |
{ |
|
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
117 |
val interp = interpreters(console) |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
118 |
with_console(console, out, err) { interp.interpret(command) } |
34844 | 119 |
if (err != null) err.commandDone() |
120 |
out.commandDone() |
|
34841 | 121 |
} |
34849 | 122 |
|
123 |
override def stop(console: Console) |
|
124 |
{ |
|
125 |
closeConsole(console) |
|
126 |
console.clear |
|
127 |
openConsole(console) |
|
128 |
val out = console.getOutput |
|
129 |
out.commandDone |
|
130 |
printPrompt(console, out) |
|
131 |
} |
|
34841 | 132 |
} |