author | immler@in.tum.de |
Wed, 10 Dec 2008 14:45:04 +0100 | |
changeset 34401 | 44241a37b74a |
parent 34393 | f0e1608a774f |
child 34406 | f81cd75ae331 |
permissions | -rw-r--r-- |
34393 | 1 |
/* |
2 |
* IsabelleSKParser.scala |
|
3 |
* |
|
4 |
* To change this template, choose Tools | Template Manager |
|
5 |
* and open the template in the editor. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle.prover |
|
9 |
||
10 |
import isabelle.jedit.Plugin |
|
11 |
import sidekick.{SideKickParser, SideKickParsedData, IAsset} |
|
12 |
import org.gjt.sp.jedit.Buffer |
|
13 |
import javax.swing.tree.DefaultMutableTreeNode |
|
14 |
import errorlist.DefaultErrorSource; |
|
15 |
||
16 |
class IsabelleSKParser() extends SideKickParser("isabelle") { |
|
17 |
||
18 |
override def parse(b : Buffer, |
|
19 |
errorSource : DefaultErrorSource) |
|
20 |
: SideKickParsedData = { |
|
21 |
if(Plugin.plugin == null || Plugin.plugin.theoryView == null |
|
22 |
|| Plugin.plugin.theoryView.buffer == null |
|
23 |
|| !Plugin.plugin.theoryView.buffer.equals(b)) |
|
24 |
{ |
|
25 |
val data = new SideKickParsedData("WARNING:") |
|
26 |
data.root.add(new DefaultMutableTreeNode("can only parse buffer which is activated via IsabellePlugin -> activate")) |
|
27 |
data |
|
28 |
} else{ |
|
29 |
val plugin = Plugin.plugin |
|
30 |
val prover = plugin.prover |
|
31 |
val buffer = Plugin.plugin.theoryView.buffer.asInstanceOf[Buffer] |
|
32 |
val document = prover.document |
|
33 |
val data = new SideKickParsedData(buffer.getPath) |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34393
diff
changeset
|
34 |
|
34393 | 35 |
for(command <- document.commands){ |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34393
diff
changeset
|
36 |
data.root.add(command.root_node.swing_node) |
34393 | 37 |
} |
38 |
data |
|
39 |
} |
|
40 |
} |
|
41 |
||
42 |
} |