|
1 package isabelle.prover |
|
2 |
|
3 import isabelle.proofdocument.Token |
|
4 import isabelle.{ YXML, XML } |
|
5 |
|
6 object Command { |
|
7 object Phase extends Enumeration { |
|
8 val UNPROCESSED = Value("UNPROCESSED") |
|
9 val FINISHED = Value("FINISHED") |
|
10 val REMOVE = Value("REMOVE") |
|
11 val REMOVED = Value("REMOVED") |
|
12 val FAILED = Value("FAILED") |
|
13 } |
|
14 |
|
15 private var nextId : Long = 0 |
|
16 def generateId : Long = { |
|
17 nextId = nextId + 1 |
|
18 return nextId |
|
19 } |
|
20 |
|
21 def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36)) |
|
22 } |
|
23 |
|
24 class Command(val first : Token[Command], val last : Token[Command]) { |
|
25 import Command._ |
|
26 |
|
27 { |
|
28 var t = first |
|
29 while(t != null) { |
|
30 t.command = this |
|
31 t = if (t == last) null else t.next |
|
32 } |
|
33 } |
|
34 |
|
35 val id : Long = generateId |
|
36 var phase = Phase.UNPROCESSED |
|
37 |
|
38 var results = Nil : List[XML.Tree] |
|
39 |
|
40 def idString = java.lang.Long.toString(id, 36) |
|
41 def document = XML.document(results match { |
|
42 case Nil => XML.Elem("message", List(), List()) |
|
43 case List(elem) => elem |
|
44 case _ => |
|
45 XML.Elem("messages", List(), List(results.first, |
|
46 results.last)) |
|
47 }, "style") |
|
48 def addResult(tree : XML.Tree) { |
|
49 results = results ::: List(tree) |
|
50 } |
|
51 |
|
52 def next = if (last.next != null) last.next.command else null |
|
53 def previous = if (first.previous != null) first.previous.command else null |
|
54 |
|
55 def start = first start |
|
56 def stop = last stop |
|
57 |
|
58 def properStart = start |
|
59 def properStop = { |
|
60 var i = last |
|
61 while (i != first && i.isComment) |
|
62 i = i.previous |
|
63 i.stop |
|
64 } |
|
65 } |