1 /* Title: jedit/plugin/IsabellePlugin.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 |
|
27 @volatile |
|
28 private var idCount = 0 |
|
29 |
|
30 def id() : String = synchronized { idCount += 1; "jedit:" + idCount } |
|
31 |
|
32 def idProperties(value: String) : Properties = { |
|
33 val props = new Properties |
|
34 props.setProperty(Markup.ID, value) |
|
35 props |
|
36 } |
|
37 |
|
38 def idProperties() : Properties = { idProperties(id()) } |
|
39 |
|
40 |
|
41 // the error source |
|
42 @volatile |
|
43 var errors: DefaultErrorSource = null |
|
44 |
|
45 // the Isabelle process |
|
46 @volatile |
|
47 var isabelle: IsabelleProcess = null |
|
48 |
|
49 |
|
50 // result content |
|
51 def result_content(result: IsabelleProcess.Result) = |
|
52 XML.content(isabelle.result_tree(result)).mkString("") |
|
53 |
|
54 |
|
55 // result consumers |
|
56 type consumer = IsabelleProcess.Result => Boolean |
|
57 private var consumers = new ListBuffer[consumer] |
|
58 |
|
59 def addConsumer(consumer: consumer) = synchronized { consumers += consumer } |
|
60 |
|
61 def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = { |
|
62 addConsumer(result => { consumer(result); false }) |
|
63 } |
|
64 |
|
65 def delConsumer(consumer: consumer) = synchronized { consumers -= consumer } |
|
66 |
|
67 def consume(result: IsabelleProcess.Result) : Unit = { |
|
68 synchronized { consumers.elements.toList } foreach (consumer => |
|
69 { |
|
70 val finished = |
|
71 try { consumer(result) } |
|
72 catch { case e: Throwable => Log.log(Log.ERROR, this, e); true } |
|
73 if (finished || result == null) |
|
74 delConsumer(consumer) |
|
75 }) |
|
76 } |
|
77 } |
|
78 |
|
79 |
|
80 /* Main plugin setup */ |
|
81 |
|
82 class IsabellePlugin extends EditPlugin { |
|
83 private var thread: Thread = null |
|
84 |
|
85 override def start = { |
|
86 // error source |
|
87 IsabellePlugin.errors = new DefaultErrorSource("isabelle") |
|
88 ErrorSource.registerErrorSource(IsabellePlugin.errors) |
|
89 |
|
90 IsabellePlugin.addPermanentConsumer (result => |
|
91 if (result != null && result.props != null && |
|
92 (result.kind == IsabelleProcess.Kind.WARNING || |
|
93 result.kind == IsabelleProcess.Kind.ERROR)) { |
|
94 val typ = |
|
95 if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING |
|
96 else ErrorSource.ERROR |
|
97 (Position.line_of(result.props), Position.file_of(result.props)) match { |
|
98 case (Some(line), Some(file)) => |
|
99 val content = IsabellePlugin.result_content(result) |
|
100 if (content.length > 0) { |
|
101 val lines = Source.fromString(content).getLines |
|
102 val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors, |
|
103 typ, file, line - 1, 0, 0, lines.next) |
|
104 for (msg <- lines) err.addExtraMessage(msg) |
|
105 IsabellePlugin.errors.addError(err) |
|
106 } |
|
107 case _ => |
|
108 } |
|
109 }) |
|
110 |
|
111 |
|
112 // Isabelle process |
|
113 IsabellePlugin.isabelle = |
|
114 new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols") |
|
115 thread = new Thread (new Runnable { |
|
116 def run = { |
|
117 var result: IsabelleProcess.Result = null |
|
118 do { |
|
119 try { |
|
120 result = IsabellePlugin.isabelle.results.take |
|
121 } |
|
122 catch { |
|
123 case _: NullPointerException => result = null |
|
124 case _: InterruptedException => result = null |
|
125 } |
|
126 if (result != null) { |
|
127 System.err.println(result) // FIXME |
|
128 IsabellePlugin.consume(result) |
|
129 } |
|
130 if (result.kind == IsabelleProcess.Kind.EXIT) { |
|
131 result = null |
|
132 IsabellePlugin.consume(null) |
|
133 } |
|
134 } while (result != null) |
|
135 } |
|
136 }) |
|
137 thread.start |
|
138 } |
|
139 |
|
140 override def stop = { |
|
141 IsabellePlugin.isabelle.kill |
|
142 thread.interrupt; thread.join; thread = null |
|
143 IsabellePlugin.isabelle = null |
|
144 |
|
145 ErrorSource.unregisterErrorSource(IsabellePlugin.errors) |
|
146 IsabellePlugin.errors = null |
|
147 } |
|
148 } |
|