author | wenzelm |
Thu, 23 Jul 2009 18:44:08 +0200 | |
changeset 32148 | 253f6808dabe |
parent 27999 | c26e0373c24f |
permissions | -rw-r--r-- |
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 java.util.Properties |
|
11 |
import java.lang.NumberFormatException |
|
12 |
||
13 |
import scala.collection.mutable.ListBuffer |
|
14 |
import scala.io.Source |
|
15 |
||
27998 | 16 |
import org.gjt.sp.util.Log |
17 |
import org.gjt.sp.jedit.{jEdit, EBPlugin, EBMessage} |
|
18 |
import org.gjt.sp.jedit.msg.DockableWindowUpdate |
|
19 |
||
20 |
import errorlist.DefaultErrorSource |
|
21 |
import errorlist.ErrorSource |
|
22 |
||
27987 | 23 |
|
27991 | 24 |
|
25 |
/** global state **/ |
|
27987 | 26 |
|
27 |
object IsabellePlugin { |
|
27991 | 28 |
|
27999 | 29 |
/* Isabelle symbols */ |
30 |
||
31 |
val symbols = new Symbol.Interpretation |
|
32 |
||
33 |
def result_content(result: IsabelleProcess.Result) = |
|
34 |
XML.content(YXML.parse_failsafe(symbols.decode(result.result))).mkString("") |
|
35 |
||
36 |
||
27991 | 37 |
/* Isabelle process */ |
38 |
||
39 |
var isabelle: IsabelleProcess = null |
|
40 |
||
41 |
||
42 |
/* unique ids */ |
|
43 |
||
44 |
private var id_count: BigInt = 0 |
|
27987 | 45 |
|
27988 | 46 |
def id() : String = synchronized { id_count += 1; "jedit:" + id_count } |
27987 | 47 |
|
27988 | 48 |
def id_properties(value: String) : Properties = { |
27987 | 49 |
val props = new Properties |
50 |
props.setProperty(Markup.ID, value) |
|
51 |
props |
|
52 |
} |
|
53 |
||
27988 | 54 |
def id_properties() : Properties = { id_properties(id()) } |
27987 | 55 |
|
56 |
||
27991 | 57 |
/* result consumers */ |
27987 | 58 |
|
27991 | 59 |
type Consumer = IsabelleProcess.Result => Boolean |
60 |
private var consumers = new ListBuffer[Consumer] |
|
27987 | 61 |
|
27991 | 62 |
def add_consumer(consumer: Consumer) = synchronized { consumers += consumer } |
27987 | 63 |
|
27988 | 64 |
def add_permanent_consumer(consumer: IsabelleProcess.Result => Unit) = { |
65 |
add_consumer(result => { consumer(result); false }) |
|
27987 | 66 |
} |
67 |
||
27991 | 68 |
def del_consumer(consumer: Consumer) = synchronized { consumers -= consumer } |
27987 | 69 |
|
27991 | 70 |
private def consume(result: IsabelleProcess.Result) = { |
27987 | 71 |
synchronized { consumers.elements.toList } foreach (consumer => |
72 |
{ |
|
27991 | 73 |
if (result != null && result.is_control) Log.log(Log.DEBUG, result, null) |
27987 | 74 |
val finished = |
75 |
try { consumer(result) } |
|
27991 | 76 |
catch { case e: Throwable => Log.log(Log.ERROR, result, e); true } |
77 |
if (finished || result == null) del_consumer(consumer) |
|
27987 | 78 |
}) |
79 |
} |
|
27991 | 80 |
|
81 |
class ConsumerThread extends Thread { |
|
82 |
override def run = { |
|
83 |
var finished = false |
|
84 |
while (!finished) { |
|
85 |
val result = |
|
86 |
try { IsabellePlugin.isabelle.get_result() } |
|
87 |
catch { case _: NullPointerException => null } |
|
88 |
||
89 |
if (result != null) { |
|
90 |
consume(result) |
|
91 |
if (result.kind == IsabelleProcess.Kind.EXIT) { |
|
92 |
consume(null) |
|
93 |
finished = true |
|
94 |
} |
|
95 |
} |
|
96 |
else finished = true |
|
97 |
} |
|
98 |
} |
|
99 |
} |
|
100 |
||
27987 | 101 |
} |
102 |
||
103 |
||
104 |
/* Main plugin setup */ |
|
105 |
||
27998 | 106 |
class IsabellePlugin extends EBPlugin { |
27991 | 107 |
|
108 |
import IsabellePlugin._ |
|
109 |
||
110 |
val errors = new DefaultErrorSource("isabelle") |
|
111 |
val consumer_thread = new ConsumerThread |
|
112 |
||
27987 | 113 |
|
114 |
override def start = { |
|
27991 | 115 |
|
116 |
/* error source */ |
|
27987 | 117 |
|
27991 | 118 |
ErrorSource.registerErrorSource(errors) |
119 |
||
120 |
add_permanent_consumer (result => |
|
121 |
if (result != null && |
|
27987 | 122 |
(result.kind == IsabelleProcess.Kind.WARNING || |
123 |
result.kind == IsabelleProcess.Kind.ERROR)) { |
|
124 |
(Position.line_of(result.props), Position.file_of(result.props)) match { |
|
125 |
case (Some(line), Some(file)) => |
|
27991 | 126 |
val typ = |
127 |
if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING |
|
128 |
else ErrorSource.ERROR |
|
129 |
val content = result_content(result) |
|
27987 | 130 |
if (content.length > 0) { |
131 |
val lines = Source.fromString(content).getLines |
|
27991 | 132 |
val err = new DefaultErrorSource.DefaultError(errors, |
27987 | 133 |
typ, file, line - 1, 0, 0, lines.next) |
134 |
for (msg <- lines) err.addExtraMessage(msg) |
|
27991 | 135 |
errors.addError(err) |
27987 | 136 |
} |
137 |
case _ => |
|
138 |
} |
|
139 |
}) |
|
140 |
||
141 |
||
27991 | 142 |
/* Isabelle process */ |
143 |
||
27995
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
144 |
val options = |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
145 |
(for (mode <- jEdit.getProperty("isabelle.print-modes").split("\\s+") if mode != "") |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
146 |
yield "-m" + mode) |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
147 |
val args = { |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
148 |
val logic = jEdit.getProperty("isabelle.logic") |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
149 |
if (logic != "") List(logic) else Nil |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
150 |
} |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
151 |
isabelle = new IsabelleProcess((options ++ args): _*) |
81cce44fa5d7
isabelle process: pick options/args from properties;
wenzelm
parents:
27991
diff
changeset
|
152 |
|
27991 | 153 |
consumer_thread.start |
154 |
||
27987 | 155 |
} |
156 |
||
27999 | 157 |
|
27991 | 158 |
override def stop = { |
159 |
isabelle.kill |
|
160 |
consumer_thread.join |
|
161 |
ErrorSource.unregisterErrorSource(errors) |
|
27987 | 162 |
} |
27991 | 163 |
|
27998 | 164 |
|
165 |
override def handleMessage(message: EBMessage) = message match { |
|
166 |
case _: DockableWindowUpdate => // FIXME check isabelle process |
|
167 |
case _ => |
|
168 |
} |
|
169 |
||
27987 | 170 |
} |