author | wenzelm |
Sat, 09 Jul 2011 21:53:27 +0200 | |
changeset 43721 | fad8634cee62 |
parent 43661 | 39fdbd814c7f |
child 45580 | 136e3faf74da |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
37175
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/scala_console.scala |
36760 | 2 |
Author: Makarius |
3 |
||
4 |
Scala instance of Console plugin. |
|
5 |
*/ |
|
34841 | 6 |
|
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
36015 | 10 |
import isabelle._ |
11 |
||
34844 | 12 |
import console.{Console, ConsolePane, Shell, Output} |
34841 | 13 |
|
34845 | 14 |
import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
34841 | 15 |
import org.gjt.sp.jedit.MiscUtilities |
16 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43282
diff
changeset
|
17 |
import java.lang.System |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
18 |
import java.io.{File, OutputStream, Writer, PrintWriter} |
34841 | 19 |
|
20 |
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
|
21 |
import scala.collection.mutable |
34841 | 22 |
|
23 |
||
24 |
class Scala_Console extends Shell("Scala") |
|
25 |
{ |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
26 |
/* reconstructed jEdit/plugin classpath */ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
27 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
28 |
private def reconstruct_classpath(): String = |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
29 |
{ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
30 |
def find_jars(start: String): List[String] = |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
31 |
if (start != null) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
32 |
Standard_System.find_files(new File(start), |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
33 |
entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
34 |
else Nil |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
35 |
val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
36 |
path.mkString(File.pathSeparator) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
37 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
38 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
39 |
|
34849 | 40 |
/* global state -- owned by Swing thread */ |
41 |
||
34841 | 42 |
private var interpreters = Map[Console, Interpreter]() |
43 |
||
44 |
private var global_console: Console = null |
|
45 |
private var global_out: Output = null |
|
46 |
private var global_err: Output = null |
|
47 |
||
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
48 |
private val console_stream = new OutputStream |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
49 |
{ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
50 |
val buf = new StringBuilder |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
51 |
override def flush() |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
52 |
{ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
53 |
val str = Standard_System.decode_permissive_utf8(buf.toString) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
54 |
buf.clear |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
55 |
if (global_out == null) System.out.print(str) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
56 |
else Swing_Thread.now { global_out.writeAttrs(null, str) } |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
57 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
58 |
override def close() { flush () } |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
59 |
def write(byte: Int) { buf.append(byte.toChar) } |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
60 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
61 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
62 |
private val console_writer = new Writer |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
63 |
{ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
64 |
def flush() {} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
65 |
def close() {} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
66 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
67 |
def write(cbuf: Array[Char], off: Int, len: Int) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
68 |
{ |
36015 | 69 |
if (len > 0) write(new String(cbuf.slice(off, off + len))) |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
70 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
71 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
72 |
override def write(str: String) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
73 |
{ |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
74 |
if (global_out == null) System.out.println(str) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
75 |
else global_out.print(null, str) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
76 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
77 |
} |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
78 |
|
34844 | 79 |
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = |
80 |
{ |
|
81 |
global_console = console |
|
82 |
global_out = out |
|
83 |
global_err = if (err == null) out else err |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
84 |
val res = Exn.capture { scala.Console.withOut(console_stream)(e) } |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
85 |
console_stream.flush |
34844 | 86 |
global_console = null |
87 |
global_out = null |
|
88 |
global_err = null |
|
89 |
Exn.release(res) |
|
90 |
} |
|
91 |
||
34841 | 92 |
private def report_error(str: String) |
93 |
{ |
|
94 |
if (global_console == null || global_err == null) System.err.println(str) |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
95 |
else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } |
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
96 |
} |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
97 |
|
34841 | 98 |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
99 |
/* jEdit console methods */ |
34841 | 100 |
|
101 |
override def openConsole(console: Console) |
|
102 |
{ |
|
103 |
val settings = new GenericRunnerSettings(report_error) |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
104 |
settings.classpath.value = reconstruct_classpath() |
34849 | 105 |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
106 |
val interp = new Interpreter(settings, new PrintWriter(console_writer, true)) |
34845 | 107 |
{ |
108 |
override def parentClassLoader = new JARClassLoader |
|
109 |
} |
|
110 |
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
|
111 |
interp.bind("view", "org.gjt.sp.jedit.View", console.getView) |
34852 | 112 |
interp.bind("console", "console.Console", console) |
34851
304a86164dd2
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents:
34850
diff
changeset
|
113 |
interp.interpret("import isabelle.jedit.Isabelle") |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
114 |
|
34845 | 115 |
interpreters += (console -> interp) |
34841 | 116 |
} |
117 |
||
118 |
override def closeConsole(console: Console) |
|
119 |
{ |
|
120 |
interpreters -= console |
|
121 |
} |
|
122 |
||
34849 | 123 |
override def printInfoMessage(out: Output) |
124 |
{ |
|
125 |
out.print(null, |
|
126 |
"This shell evaluates Isabelle/Scala expressions.\n\n" + |
|
127 |
"The following special toplevel bindings are provided:\n" + |
|
34851
304a86164dd2
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents:
34850
diff
changeset
|
128 |
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + |
34852 | 129 |
" console -- jEdit Console plugin instance\n" + |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
130 |
" Isabelle -- Isabelle plugin instance (e.g. Isabelle.session)\n") |
34849 | 131 |
} |
132 |
||
34841 | 133 |
override def printPrompt(console: Console, out: Output) |
37175 | 134 |
{ |
34844 | 135 |
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") |
37175 | 136 |
out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") |
137 |
} |
|
34841 | 138 |
|
139 |
override def execute(console: Console, input: String, out: Output, err: Output, command: String) |
|
140 |
{ |
|
34846
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
141 |
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
|
142 |
with_console(console, out, err) { interp.interpret(command) } |
34844 | 143 |
if (err != null) err.commandDone() |
37175 | 144 |
out.commandDone() |
34841 | 145 |
} |
34849 | 146 |
|
147 |
override def stop(console: Console) |
|
148 |
{ |
|
149 |
closeConsole(console) |
|
150 |
console.clear |
|
151 |
openConsole(console) |
|
152 |
val out = console.getOutput |
|
153 |
out.commandDone |
|
154 |
printPrompt(console, out) |
|
155 |
} |
|
34841 | 156 |
} |