author | wenzelm |
Wed, 05 May 2010 23:09:34 +0200 | |
changeset 36677 | 1225dd15827d |
parent 36676 | ac7961d42ac3 |
child 36735 | 42b7f881f5fc |
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, |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34777
diff
changeset
|
14 |
val 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 { |
34859 | 55 |
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
|
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 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
73 |
def + (session: Session, 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) => |
|
36677 | 84 |
atts match { |
85 |
case Position.Range(begin, end) => |
|
86 |
if (kind == Markup.ML_TYPING) { |
|
87 |
val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!? |
|
88 |
state.add_markup( |
|
89 |
command.markup_node(begin - 1, end - 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 - 1, end - 1, |
|
96 |
Command.RefInfo( |
|
97 |
Position.get_file(atts), |
|
98 |
Position.get_line(atts), |
|
99 |
Position.get_id(atts), |
|
100 |
Position.get_offset(atts)))) |
|
101 |
case _ => state |
|
102 |
} |
|
103 |
} |
|
104 |
else { |
|
105 |
state.add_markup( |
|
106 |
command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind))) |
|
107 |
} |
|
108 |
case _ => state |
|
34715 | 109 |
} |
110 |
case _ => |
|
111 |
System.err.println("ignored status report: " + elem) |
|
112 |
state |
|
34703 | 113 |
}) |
34715 | 114 |
case _ => add_result(message) |
34703 | 115 |
} |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
116 |
if (!(this eq changed)) session.command_change.event(command) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
117 |
changed |
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
118 |
} |
34675 | 119 |
} |