author | wenzelm |
Thu, 03 Sep 2009 17:26:25 +0200 | |
changeset 34700 | 0e1d098940a7 |
parent 34697 | 3d4874198e62 |
child 34703 | ff037c17332a |
permissions | -rw-r--r-- |
34675 | 1 |
/* |
2 |
* Accumulating results from prover |
|
3 |
* |
|
4 |
* @author Fabian Immler, TU Munich |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.prover |
|
8 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
9 |
|
34697 | 10 |
class State( |
11 |
val command: Command, |
|
12 |
val status: Command.Status.Value, |
|
13 |
rev_results: List[XML.Tree], |
|
14 |
val markup_root: MarkupNode) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
15 |
{ |
34697 | 16 |
def this(command: Command) = |
17 |
this(command, Command.Status.UNPROCESSED, Nil, command.empty_root_node) |
|
18 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
19 |
|
34697 | 20 |
/* content */ |
21 |
||
22 |
private def set_status(st: Command.Status.Value): State = |
|
23 |
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
|
24 |
|
34697 | 25 |
private def add_result(res: XML.Tree): State = |
26 |
new State(command, status, res :: rev_results, markup_root) |
|
27 |
||
28 |
private def add_markup(markup: MarkupNode): State = |
|
29 |
new State(command, status, rev_results, markup_root + markup) |
|
30 |
||
31 |
lazy val results = rev_results.reverse |
|
32 |
||
34688 | 33 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
34 |
/* markup */ |
34697 | 35 |
|
34688 | 36 |
lazy val highlight_node: MarkupNode = |
37 |
{ |
|
38 |
markup_root.filter(_.info match { |
|
39 |
case RootInfo() | HighlightInfo(_) => true |
|
40 |
case _ => false |
|
41 |
}).head |
|
42 |
} |
|
43 |
||
44 |
lazy private val types = |
|
45 |
markup_root.filter(_.info match { |
|
46 |
case TypeInfo(_) => true |
|
47 |
case _ => false }).flatten(_.flatten) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
48 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
49 |
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
|
50 |
{ |
34688 | 51 |
types.find(t => t.start <= pos && t.stop > pos).map(t => |
52 |
t.content + ": " + (t.info match { |
|
53 |
case TypeInfo(i) => i |
|
54 |
case _ => "" })). |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
55 |
getOrElse(null) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
56 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
57 |
|
34688 | 58 |
lazy private val refs = |
59 |
markup_root.filter(_.info match { |
|
60 |
case RefInfo(_, _, _, _) => true |
|
61 |
case _ => false }).flatten(_.flatten) |
|
62 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
63 |
def ref_at(pos: Int): Option[MarkupNode] = |
34688 | 64 |
refs.find(t => t.start <= pos && t.stop > pos) |
65 |
||
66 |
||
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
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 = |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
73 |
message match { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
74 |
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _) |
34697 | 75 |
| XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _) |
76 |
| XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) => |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
77 |
add_result(message) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
78 |
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
79 |
set_status(Command.Status.FAILED).add_result(message) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
80 |
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => |
34697 | 81 |
(this /: elems) ((st, e) => |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
82 |
e match { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
83 |
// command status |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
84 |
case XML.Elem(Markup.UNPROCESSED, _, _) => |
34697 | 85 |
st.set_status(Command.Status.UNPROCESSED) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
86 |
case XML.Elem(Markup.FINISHED, _, _) => |
34697 | 87 |
st.set_status(Command.Status.FINISHED) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
88 |
case XML.Elem(Markup.FAILED, _, _) => |
34697 | 89 |
st.set_status(Command.Status.FAILED) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
90 |
case XML.Elem(kind, attr, body) => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
91 |
val (begin, end) = Position.offsets_of(attr) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
92 |
if (begin.isDefined && end.isDefined) { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
93 |
if (kind == Markup.ML_TYPING) { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
94 |
val info = body.first.asInstanceOf[XML.Text].content |
34697 | 95 |
st.add_markup(command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))) |
96 |
} |
|
97 |
else if (kind == Markup.ML_REF) { |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
98 |
body match { |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
99 |
case List(XML.Elem(Markup.ML_DEF, attr, _)) => |
34697 | 100 |
st.add_markup(command.markup_node( |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
101 |
begin.get - 1, end.get - 1, |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
102 |
RefInfo( |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
103 |
Position.file_of(attr), |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
104 |
Position.line_of(attr), |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
105 |
Position.id_of(attr), |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
106 |
Position.offset_of(attr)))) |
34697 | 107 |
case _ => st |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
108 |
} |
34697 | 109 |
} |
110 |
else { |
|
111 |
st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
112 |
} |
34697 | 113 |
} |
114 |
else st |
|
115 |
case _ => st |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
116 |
}) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
117 |
case _ => |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
118 |
System.err.println("ignored: " + message) |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
119 |
this |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
120 |
} |
34697 | 121 |
command.changed() |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
122 |
changed |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
123 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
124 |
|
34675 | 125 |
} |