27987
|
1 |
/* Title: lib/jedit/plugin/isabelle_plugin.scala
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Isabelle/jEdit plugin -- main setup.
|
|
6 |
*/
|
|
7 |
|
|
8 |
package isabelle.jedit
|
|
9 |
|
|
10 |
import org.gjt.sp.jedit.EditPlugin
|
|
11 |
import org.gjt.sp.util.Log
|
|
12 |
|
|
13 |
import errorlist.DefaultErrorSource
|
|
14 |
import errorlist.ErrorSource
|
|
15 |
|
|
16 |
import java.util.Properties
|
|
17 |
import java.lang.NumberFormatException
|
|
18 |
|
|
19 |
import scala.collection.mutable.ListBuffer
|
|
20 |
import scala.io.Source
|
|
21 |
|
|
22 |
|
|
23 |
/* Global state */
|
|
24 |
|
|
25 |
object IsabellePlugin {
|
|
26 |
// unique ids
|
27988
|
27 |
private var id_count = 0
|
27987
|
28 |
|
27988
|
29 |
def id() : String = synchronized { id_count += 1; "jedit:" + id_count }
|
27987
|
30 |
|
27988
|
31 |
def id_properties(value: String) : Properties = {
|
27987
|
32 |
val props = new Properties
|
|
33 |
props.setProperty(Markup.ID, value)
|
|
34 |
props
|
|
35 |
}
|
|
36 |
|
27988
|
37 |
def id_properties() : Properties = { id_properties(id()) }
|
27987
|
38 |
|
|
39 |
|
|
40 |
// the error source
|
|
41 |
var errors: DefaultErrorSource = null
|
|
42 |
|
|
43 |
// the Isabelle process
|
|
44 |
var isabelle: IsabelleProcess = null
|
|
45 |
|
|
46 |
|
|
47 |
// result content
|
|
48 |
def result_content(result: IsabelleProcess.Result) =
|
|
49 |
XML.content(isabelle.result_tree(result)).mkString("")
|
|
50 |
|
|
51 |
|
|
52 |
// result consumers
|
|
53 |
type consumer = IsabelleProcess.Result => Boolean
|
|
54 |
private var consumers = new ListBuffer[consumer]
|
|
55 |
|
27988
|
56 |
def add_consumer(consumer: consumer) = synchronized { consumers += consumer }
|
27987
|
57 |
|
27988
|
58 |
def add_permanent_consumer(consumer: IsabelleProcess.Result => Unit) = {
|
|
59 |
add_consumer(result => { consumer(result); false })
|
27987
|
60 |
}
|
|
61 |
|
27988
|
62 |
def del_consumer(consumer: consumer) = synchronized { consumers -= consumer }
|
27987
|
63 |
|
|
64 |
def consume(result: IsabelleProcess.Result) : Unit = {
|
|
65 |
synchronized { consumers.elements.toList } foreach (consumer =>
|
|
66 |
{
|
|
67 |
val finished =
|
|
68 |
try { consumer(result) }
|
|
69 |
catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
|
|
70 |
if (finished || result == null)
|
27988
|
71 |
del_consumer(consumer)
|
27987
|
72 |
})
|
|
73 |
}
|
|
74 |
}
|
|
75 |
|
|
76 |
|
|
77 |
/* Main plugin setup */
|
|
78 |
|
|
79 |
class IsabellePlugin extends EditPlugin {
|
|
80 |
private var thread: Thread = null
|
|
81 |
|
|
82 |
override def start = {
|
|
83 |
// error source
|
|
84 |
IsabellePlugin.errors = new DefaultErrorSource("isabelle")
|
|
85 |
ErrorSource.registerErrorSource(IsabellePlugin.errors)
|
|
86 |
|
27988
|
87 |
IsabellePlugin.add_permanent_consumer (result =>
|
27987
|
88 |
if (result != null && result.props != null &&
|
|
89 |
(result.kind == IsabelleProcess.Kind.WARNING ||
|
|
90 |
result.kind == IsabelleProcess.Kind.ERROR)) {
|
|
91 |
val typ =
|
|
92 |
if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
|
|
93 |
else ErrorSource.ERROR
|
|
94 |
(Position.line_of(result.props), Position.file_of(result.props)) match {
|
|
95 |
case (Some(line), Some(file)) =>
|
|
96 |
val content = IsabellePlugin.result_content(result)
|
|
97 |
if (content.length > 0) {
|
|
98 |
val lines = Source.fromString(content).getLines
|
|
99 |
val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
|
|
100 |
typ, file, line - 1, 0, 0, lines.next)
|
|
101 |
for (msg <- lines) err.addExtraMessage(msg)
|
|
102 |
IsabellePlugin.errors.addError(err)
|
|
103 |
}
|
|
104 |
case _ =>
|
|
105 |
}
|
|
106 |
})
|
|
107 |
|
|
108 |
|
|
109 |
// Isabelle process
|
|
110 |
IsabellePlugin.isabelle =
|
|
111 |
new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
|
|
112 |
thread = new Thread (new Runnable {
|
|
113 |
def run = {
|
|
114 |
var result: IsabelleProcess.Result = null
|
|
115 |
do {
|
|
116 |
try {
|
|
117 |
result = IsabellePlugin.isabelle.results.take
|
|
118 |
}
|
|
119 |
catch {
|
|
120 |
case _: NullPointerException => result = null
|
|
121 |
case _: InterruptedException => result = null
|
|
122 |
}
|
|
123 |
if (result != null) {
|
|
124 |
System.err.println(result) // FIXME
|
|
125 |
IsabellePlugin.consume(result)
|
|
126 |
}
|
|
127 |
if (result.kind == IsabelleProcess.Kind.EXIT) {
|
|
128 |
result = null
|
|
129 |
IsabellePlugin.consume(null)
|
|
130 |
}
|
|
131 |
} while (result != null)
|
|
132 |
}
|
|
133 |
})
|
|
134 |
thread.start
|
|
135 |
}
|
|
136 |
|
|
137 |
override def stop = {
|
|
138 |
IsabellePlugin.isabelle.kill
|
|
139 |
thread.interrupt; thread.join; thread = null
|
|
140 |
IsabellePlugin.isabelle = null
|
|
141 |
|
|
142 |
ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
|
|
143 |
IsabellePlugin.errors = null
|
|
144 |
}
|
|
145 |
}
|