author | wenzelm |
Wed, 11 Aug 2010 22:41:26 +0200 | |
changeset 38355 | 8cb265fb12fe |
parent 38236 | d8c7be27e01d |
child 38358 | 15819cbd7b0e |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/state.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
5 |
Accumulated results from prover. |
36676 | 6 |
*/ |
34675 | 7 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34859
diff
changeset
|
8 |
package isabelle |
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, |
|
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
14 |
val forks: Int, |
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
37044
diff
changeset
|
15 |
val reverse_results: List[XML.Tree], |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
16 |
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
|
17 |
{ |
34697 | 18 |
def this(command: Command) = |
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
19 |
this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) |
34697 | 20 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
21 |
|
34697 | 22 |
/* content */ |
23 |
||
24 |
private def set_status(st: Command.Status.Value): State = |
|
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
25 |
new State(command, st, forks, reverse_results, markup_root) |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
26 |
|
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
27 |
private def add_forks(i: Int): State = |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
28 |
new State(command, status, forks + i, reverse_results, markup_root) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
29 |
|
34697 | 30 |
private def add_result(res: XML.Tree): State = |
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
31 |
new State(command, status, forks, res :: reverse_results, markup_root) |
34697 | 32 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
33 |
private def add_markup(node: Markup_Tree): State = |
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
34 |
new State(command, status, forks, reverse_results, markup_root + node) |
34697 | 35 |
|
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
37044
diff
changeset
|
36 |
lazy val results = reverse_results.reverse |
34697 | 37 |
|
34688 | 38 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
39 |
/* markup */ |
34697 | 40 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
41 |
lazy val highlight: Markup_Text = |
34688 | 42 |
{ |
43 |
markup_root.filter(_.info match { |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
44 |
case Command.HighlightInfo(_, _) => true |
34688 | 45 |
case _ => false |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
46 |
}) |
34688 | 47 |
} |
48 |
||
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
49 |
private lazy val types: List[Markup_Node] = |
34688 | 50 |
markup_root.filter(_.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
51 |
case Command.TypeInfo(_) => true |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
52 |
case _ => false }).flatten |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
53 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
54 |
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
|
55 |
{ |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
56 |
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
|
57 |
case Some(t) => |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
58 |
t.info match { |
37199
48a4414eb846
one extra space to accomodate symbolic indentifiers etc.;
wenzelm
parents:
37197
diff
changeset
|
59 |
case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
60 |
case _ => None |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
61 |
} |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
62 |
case None => None |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
63 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
64 |
} |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
65 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
66 |
private lazy val refs: List[Markup_Node] = |
34688 | 67 |
markup_root.filter(_.info match { |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34703
diff
changeset
|
68 |
case Command.RefInfo(_, _, _, _) => true |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
69 |
case _ => false }).flatten |
34688 | 70 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34715
diff
changeset
|
71 |
def ref_at(pos: Int): Option[Markup_Node] = |
34703 | 72 |
refs.find(t => t.start <= pos && pos < t.stop) |
34688 | 73 |
|
74 |
||
34697 | 75 |
/* message dispatch */ |
76 |
||
37178
d52f934f8ff6
accumulate only local results -- no proper history support yet;
wenzelm
parents:
37149
diff
changeset
|
77 |
def accumulate(message: XML.Tree): State = |
37129 | 78 |
message match { |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
79 |
case XML.Elem(Markup(Markup.STATUS, _), elems) => |
37129 | 80 |
(this /: elems)((state, elem) => |
81 |
elem match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
82 |
case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED) |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
83 |
case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED) |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
84 |
case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED) |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
85 |
case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1) |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
86 |
case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1) |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
87 |
case _ => System.err.println("Ignored status message: " + elem); state |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
88 |
}) |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
89 |
|
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
90 |
case XML.Elem(Markup(Markup.REPORT, _), elems) => |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
91 |
(this /: elems)((state, elem) => |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
92 |
elem match { |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
93 |
case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => |
37129 | 94 |
atts match { |
95 |
case Position.Range(begin, end) => |
|
96 |
if (kind == Markup.ML_TYPING) { |
|
97 |
val info = Pretty.string_of(body, margin = 40) |
|
98 |
state.add_markup( |
|
99 |
command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) |
|
100 |
} |
|
101 |
else if (kind == Markup.ML_REF) { |
|
102 |
body match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37199
diff
changeset
|
103 |
case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) => |
37129 | 104 |
state.add_markup(command.markup_node( |
105 |
begin - 1, end - 1, |
|
106 |
Command.RefInfo( |
|
107 |
Position.get_file(atts), |
|
108 |
Position.get_line(atts), |
|
109 |
Position.get_id(atts), |
|
110 |
Position.get_offset(atts)))) |
|
111 |
case _ => state |
|
36677 | 112 |
} |
37129 | 113 |
} |
114 |
else { |
|
115 |
state.add_markup( |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
116 |
command.markup_node(begin - 1, end - 1, |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
117 |
Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) |
37129 | 118 |
} |
119 |
case _ => state |
|
120 |
} |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38230
diff
changeset
|
121 |
case _ => System.err.println("Ignored report message: " + elem); state |
37129 | 122 |
}) |
123 |
case _ => add_result(message) |
|
124 |
} |
|
34675 | 125 |
} |