author | wenzelm |
Tue, 08 Dec 2009 16:30:20 +0100 | |
changeset 34760 | dc7f5e0d9d27 |
parent 34759 | bfea7839d9e1 |
child 34777 | 91d6089cef88 |
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 |
||
34760 | 8 |
package isabelle.proofdocument |
34675 | 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], |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
15 |
val markup_root: Markup_Text) |
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) = |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
18 |
this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup) |
34697 | 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 |
||
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
29 |
private def add_markup(node: Markup_Tree): State = |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
30 |
new State(command, status, rev_results, markup_root + node) |
34697 | 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 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
37 |
lazy val highlight: Markup_Text = |
34688 | 38 |
{ |
39 |
markup_root.filter(_.info match { |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
40 |
case Command.HighlightInfo(_) => true |
34688 | 41 |
case _ => false |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
42 |
}) |
34688 | 43 |
} |
44 |
||
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
45 |
private lazy val types: List[Markup_Node] = |
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 |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
48 |
case _ => false }).flatten |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
49 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
50 |
def type_at(pos: Int): Option[String] = |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
51 |
{ |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
52 |
types.find(t => t.start <= pos && pos < t.stop) match { |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
53 |
case Some(t) => |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
54 |
t.info match { |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
55 |
case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty) |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
56 |
case _ => None |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
57 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
58 |
case None => None |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
59 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
60 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
61 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
62 |
private lazy val refs: List[Markup_Node] = |
34688 | 63 |
markup_root.filter(_.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
64 |
case Command.RefInfo(_, _, _, _) => true |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
65 |
case _ => false }).flatten |
34688 | 66 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
67 |
def ref_at(pos: Int): Option[Markup_Node] = |
34703 | 68 |
refs.find(t => t.start <= pos && pos < t.stop) |
34688 | 69 |
|
70 |
||
34697 | 71 |
/* message dispatch */ |
72 |
||
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34717
diff
changeset
|
73 |
def + (prover: Prover, message: XML.Tree): State = |
34697 | 74 |
{ |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
75 |
val changed: State = |
34703 | 76 |
message match { |
77 |
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => |
|
34715 | 78 |
(this /: elems)((state, elem) => |
79 |
elem match { |
|
80 |
case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) |
|
81 |
case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) |
|
82 |
case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) |
|
83 |
case XML.Elem(kind, atts, body) => |
|
84 |
val (begin, end) = Position.offsets_of(atts) |
|
85 |
if (begin.isEmpty || end.isEmpty) state |
|
86 |
else if (kind == Markup.ML_TYPING) { |
|
87 |
val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!? |
|
88 |
state.add_markup( |
|
89 |
command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) |
|
90 |
} |
|
91 |
else if (kind == Markup.ML_REF) { |
|
92 |
body match { |
|
93 |
case List(XML.Elem(Markup.ML_DEF, atts, _)) => |
|
94 |
state.add_markup(command.markup_node( |
|
95 |
begin.get - 1, end.get - 1, |
|
96 |
Command.RefInfo( |
|
97 |
Position.file_of(atts), |
|
98 |
Position.line_of(atts), |
|
99 |
Position.id_of(atts), |
|
100 |
Position.offset_of(atts)))) |
|
101 |
case _ => state |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
102 |
} |
34697 | 103 |
} |
34715 | 104 |
else { |
105 |
state.add_markup( |
|
106 |
command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) |
|
107 |
} |
|
108 |
case _ => |
|
109 |
System.err.println("ignored status report: " + elem) |
|
110 |
state |
|
34703 | 111 |
}) |
34715 | 112 |
case _ => add_result(message) |
34703 | 113 |
} |
34724
b1079c3ba1da
Prover: keep command_change/document_change event buses here, not in ProofDocument, Command, State, Plugin;
wenzelm
parents:
34717
diff
changeset
|
114 |
if (!(this eq changed)) prover.command_change.event(command) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
115 |
changed |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
116 |
} |
34675 | 117 |
} |