author | wenzelm |
Sun, 06 Sep 2009 15:43:02 +0200 | |
changeset 34715 | 826e476947f9 |
parent 34709 | 2f0c18f9b6c7 |
child 34717 | 3f32e08bbb6c |
permissions | -rw-r--r-- |
34675 | 1 |
/* |
2 |
* Accumulating results from prover |
|
3 |
* |
|
4 |
* @author Fabian Immler, TU Munich |
|
34715 | 5 |
* @author Makarius |
34675 | 6 |
*/ |
7 |
||
8 |
package isabelle.prover |
|
9 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
10 |
|
34697 | 11 |
class State( |
12 |
val command: Command, |
|
13 |
val status: Command.Status.Value, |
|
14 |
rev_results: List[XML.Tree], |
|
15 |
val markup_root: MarkupNode) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
16 |
{ |
34697 | 17 |
def this(command: Command) = |
18 |
this(command, Command.Status.UNPROCESSED, Nil, command.empty_root_node) |
|
19 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
20 |
|
34697 | 21 |
/* content */ |
22 |
||
23 |
private def set_status(st: Command.Status.Value): State = |
|
24 |
new State(command, st, rev_results, markup_root) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
25 |
|
34697 | 26 |
private def add_result(res: XML.Tree): State = |
27 |
new State(command, status, res :: rev_results, markup_root) |
|
28 |
||
29 |
private def add_markup(markup: MarkupNode): State = |
|
30 |
new State(command, status, rev_results, markup_root + markup) |
|
31 |
||
32 |
lazy val results = rev_results.reverse |
|
33 |
||
34688 | 34 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
35 |
/* markup */ |
34697 | 36 |
|
34688 | 37 |
lazy val highlight_node: MarkupNode = |
38 |
{ |
|
39 |
markup_root.filter(_.info match { |
|
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
40 |
case Command.RootInfo | Command.HighlightInfo(_) => true |
34688 | 41 |
case _ => false |
42 |
}).head |
|
43 |
} |
|
44 |
||
34709 | 45 |
private lazy val types = |
34688 | 46 |
markup_root.filter(_.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
47 |
case Command.TypeInfo(_) => true |
34688 | 48 |
case _ => false }).flatten(_.flatten) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
49 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
50 |
def type_at(pos: Int): String = |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
51 |
{ |
34709 | 52 |
types.find(t => t.start <= pos && pos < t.stop).map(t => |
34688 | 53 |
t.content + ": " + (t.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
54 |
case Command.TypeInfo(i) => i |
34688 | 55 |
case _ => "" })). |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
56 |
getOrElse(null) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
57 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
58 |
|
34709 | 59 |
private lazy val refs = |
34688 | 60 |
markup_root.filter(_.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
61 |
case Command.RefInfo(_, _, _, _) => true |
34688 | 62 |
case _ => false }).flatten(_.flatten) |
63 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
64 |
def ref_at(pos: Int): Option[MarkupNode] = |
34703 | 65 |
refs.find(t => t.start <= pos && pos < t.stop) |
34688 | 66 |
|
67 |
||
34697 | 68 |
/* message dispatch */ |
69 |
||
70 |
def + (message: XML.Tree): State = |
|
71 |
{ |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
72 |
val changed: State = |
34703 | 73 |
message match { |
74 |
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => |
|
34715 | 75 |
(this /: elems)((state, elem) => |
76 |
elem match { |
|
77 |
case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) |
|
78 |
case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) |
|
79 |
case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) |
|
80 |
case XML.Elem(kind, atts, body) => |
|
81 |
val (begin, end) = Position.offsets_of(atts) |
|
82 |
if (begin.isEmpty || end.isEmpty) state |
|
83 |
else if (kind == Markup.ML_TYPING) { |
|
84 |
val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!? |
|
85 |
state.add_markup( |
|
86 |
command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) |
|
87 |
} |
|
88 |
else if (kind == Markup.ML_REF) { |
|
89 |
body match { |
|
90 |
case List(XML.Elem(Markup.ML_DEF, atts, _)) => |
|
91 |
state.add_markup(command.markup_node( |
|
92 |
begin.get - 1, end.get - 1, |
|
93 |
Command.RefInfo( |
|
94 |
Position.file_of(atts), |
|
95 |
Position.line_of(atts), |
|
96 |
Position.id_of(atts), |
|
97 |
Position.offset_of(atts)))) |
|
98 |
case _ => state |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
99 |
} |
34697 | 100 |
} |
34715 | 101 |
else { |
102 |
state.add_markup( |
|
103 |
command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) |
|
104 |
} |
|
105 |
case _ => |
|
106 |
System.err.println("ignored status report: " + elem) |
|
107 |
state |
|
34703 | 108 |
}) |
34715 | 109 |
case _ => add_result(message) |
34703 | 110 |
} |
34715 | 111 |
if (!(this eq changed)) command.changed() |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
112 |
changed |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
113 |
} |
34675 | 114 |
} |