author | wenzelm |
Sun, 30 May 2010 21:59:15 +0200 | |
changeset 37199 | 48a4414eb846 |
parent 37197 | 953fc4983439 |
child 38230 | ed147003de4b |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/state.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Accumulating results from prover. |
|
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 { |
79 |
case XML.Elem(Markup.STATUS, _, elems) => |
|
80 |
(this /: elems)((state, elem) => |
|
81 |
elem match { |
|
82 |
case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) |
|
83 |
case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) |
|
84 |
case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) |
|
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
85 |
case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1) |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37178
diff
changeset
|
86 |
case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1) |
37178
d52f934f8ff6
accumulate only local results -- no proper history support yet;
wenzelm
parents:
37149
diff
changeset
|
87 |
case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) => |
37129 | 88 |
atts match { |
89 |
case Position.Range(begin, end) => |
|
90 |
if (kind == Markup.ML_TYPING) { |
|
91 |
val info = Pretty.string_of(body, margin = 40) |
|
92 |
state.add_markup( |
|
93 |
command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) |
|
94 |
} |
|
95 |
else if (kind == Markup.ML_REF) { |
|
96 |
body match { |
|
97 |
case List(XML.Elem(Markup.ML_DEF, atts, _)) => |
|
98 |
state.add_markup(command.markup_node( |
|
99 |
begin - 1, end - 1, |
|
100 |
Command.RefInfo( |
|
101 |
Position.get_file(atts), |
|
102 |
Position.get_line(atts), |
|
103 |
Position.get_id(atts), |
|
104 |
Position.get_offset(atts)))) |
|
105 |
case _ => state |
|
36677 | 106 |
} |
37129 | 107 |
} |
108 |
else { |
|
109 |
state.add_markup( |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
110 |
command.markup_node(begin - 1, end - 1, |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
111 |
Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) |
37129 | 112 |
} |
113 |
case _ => state |
|
114 |
} |
|
115 |
case _ => |
|
37189 | 116 |
System.err.println("Ignored status report: " + elem) |
37129 | 117 |
state |
118 |
}) |
|
119 |
case _ => add_result(message) |
|
120 |
} |
|
34675 | 121 |
} |