|
1 /* |
|
2 * Prover commands with semantic state |
|
3 * |
|
4 * @author Johannes Hölzl, TU Munich |
|
5 * @author Fabian Immler, TU Munich |
|
6 */ |
|
7 |
|
8 package isabelle.prover |
|
9 |
|
10 |
|
11 import scala.actors.Actor, Actor._ |
|
12 |
|
13 import scala.collection.mutable |
|
14 |
|
15 import isabelle.proofdocument.{Token, ProofDocument} |
|
16 import isabelle.jedit.{Isabelle, Plugin} |
|
17 import isabelle.XML |
|
18 |
|
19 |
|
20 trait Accumulator extends Actor |
|
21 { |
|
22 start() // start actor |
|
23 |
|
24 protected var _state: State |
|
25 def state = _state |
|
26 |
|
27 override def act() { |
|
28 loop { |
|
29 react { |
|
30 case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message) |
|
31 case bad => System.err.println("prover: ignoring bad message " + bad) |
|
32 } |
|
33 } |
|
34 } |
|
35 } |
|
36 |
|
37 |
|
38 object Command |
|
39 { |
|
40 object Status extends Enumeration |
|
41 { |
|
42 val UNPROCESSED = Value("UNPROCESSED") |
|
43 val FINISHED = Value("FINISHED") |
|
44 val FAILED = Value("FAILED") |
|
45 } |
|
46 |
|
47 case class HighlightInfo(highlight: String) { override def toString = highlight } |
|
48 case class TypeInfo(ty: String) |
|
49 case class RefInfo(file: Option[String], line: Option[Int], |
|
50 command_id: Option[String], offset: Option[Int]) |
|
51 } |
|
52 |
|
53 |
|
54 class Command( |
|
55 val tokens: List[Token], |
|
56 val starts: Map[Token, Int]) extends Accumulator |
|
57 { |
|
58 require(!tokens.isEmpty) |
|
59 |
|
60 val id = Isabelle.system.id() |
|
61 override def hashCode = id.hashCode |
|
62 |
|
63 |
|
64 /* content */ |
|
65 |
|
66 override def toString = name |
|
67 |
|
68 val name = tokens.head.content |
|
69 val content: String = Token.string_from_tokens(tokens, starts) |
|
70 def content(i: Int, j: Int): String = content.substring(i, j) |
|
71 val symbol_index = new Symbol.Index(content) |
|
72 |
|
73 def start(doc: ProofDocument) = doc.token_start(tokens.first) |
|
74 def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length |
|
75 |
|
76 def contains(p: Token) = tokens.contains(p) |
|
77 |
|
78 protected override var _state = new State(this) |
|
79 |
|
80 |
|
81 /* markup */ |
|
82 |
|
83 lazy val empty_markup = new Markup_Text(Nil, content) |
|
84 |
|
85 def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = |
|
86 { |
|
87 val start = symbol_index.decode(begin) |
|
88 val stop = symbol_index.decode(end) |
|
89 new Markup_Tree(new Markup_Node(start, stop, info), Nil) |
|
90 } |
|
91 |
|
92 |
|
93 /* results, markup, ... */ |
|
94 |
|
95 private val empty_cmd_state = new Command_State(this) |
|
96 private def cmd_state(doc: ProofDocument) = |
|
97 doc.states.getOrElse(this, empty_cmd_state) |
|
98 |
|
99 def status(doc: ProofDocument) = cmd_state(doc).state.status |
|
100 def results(doc: ProofDocument) = cmd_state(doc).results |
|
101 def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root |
|
102 def highlight(doc: ProofDocument) = cmd_state(doc).highlight |
|
103 def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset) |
|
104 def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset) |
|
105 } |
|
106 |
|
107 |
|
108 class Command_State(val command: Command) extends Accumulator |
|
109 { |
|
110 protected override var _state = new State(command) |
|
111 |
|
112 def results: List[XML.Tree] = |
|
113 command.state.results ::: state.results |
|
114 |
|
115 def markup_root: Markup_Text = |
|
116 (command.state.markup_root /: state.markup_root.markup)(_ + _) |
|
117 |
|
118 def type_at(pos: Int): Option[String] = state.type_at(pos) |
|
119 |
|
120 def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos) |
|
121 |
|
122 def highlight: Markup_Text = |
|
123 (command.state.highlight /: state.highlight.markup)(_ + _) |
|
124 } |