1 /* Title: Pure/PIDE/state.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Accumulated results from prover. |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 class State( |
|
12 val command: Command, |
|
13 val status: Command.Status.Value, |
|
14 val forks: Int, |
|
15 val reverse_results: List[XML.Tree], |
|
16 val markup_root: Markup_Text) |
|
17 { |
|
18 def this(command: Command) = |
|
19 this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) |
|
20 |
|
21 |
|
22 /* content */ |
|
23 |
|
24 private def set_status(st: Command.Status.Value): State = |
|
25 new State(command, st, forks, reverse_results, markup_root) |
|
26 |
|
27 private def add_forks(i: Int): State = |
|
28 new State(command, status, forks + i, reverse_results, markup_root) |
|
29 |
|
30 private def add_result(res: XML.Tree): State = |
|
31 new State(command, status, forks, res :: reverse_results, markup_root) |
|
32 |
|
33 private def add_markup(node: Markup_Tree): State = |
|
34 new State(command, status, forks, reverse_results, markup_root + node) |
|
35 |
|
36 lazy val results = reverse_results.reverse |
|
37 |
|
38 |
|
39 /* markup */ |
|
40 |
|
41 lazy val highlight: Markup_Text = |
|
42 { |
|
43 markup_root.filter(_.info match { |
|
44 case Command.HighlightInfo(_, _) => true |
|
45 case _ => false |
|
46 }) |
|
47 } |
|
48 |
|
49 private lazy val types: List[Markup_Node] = |
|
50 markup_root.filter(_.info match { |
|
51 case Command.TypeInfo(_) => true |
|
52 case _ => false }).flatten |
|
53 |
|
54 def type_at(pos: Int): Option[String] = |
|
55 { |
|
56 types.find(t => t.start <= pos && pos < t.stop) match { |
|
57 case Some(t) => |
|
58 t.info match { |
|
59 case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) |
|
60 case _ => None |
|
61 } |
|
62 case None => None |
|
63 } |
|
64 } |
|
65 |
|
66 private lazy val refs: List[Markup_Node] = |
|
67 markup_root.filter(_.info match { |
|
68 case Command.RefInfo(_, _, _, _) => true |
|
69 case _ => false }).flatten |
|
70 |
|
71 def ref_at(pos: Int): Option[Markup_Node] = |
|
72 refs.find(t => t.start <= pos && pos < t.stop) |
|
73 |
|
74 |
|
75 /* message dispatch */ |
|
76 |
|
77 def accumulate(message: XML.Tree): State = |
|
78 message match { |
|
79 case XML.Elem(Markup(Markup.STATUS, _), elems) => |
|
80 (this /: elems)((state, elem) => |
|
81 elem match { |
|
82 case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED) |
|
83 case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED) |
|
84 case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED) |
|
85 case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1) |
|
86 case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1) |
|
87 case _ => System.err.println("Ignored status message: " + elem); state |
|
88 }) |
|
89 |
|
90 case XML.Elem(Markup(Markup.REPORT, _), elems) => |
|
91 (this /: elems)((state, elem) => |
|
92 elem match { |
|
93 case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => |
|
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 { |
|
103 case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => |
|
104 state.add_markup(command.markup_node( |
|
105 begin - 1, end - 1, |
|
106 Command.RefInfo( |
|
107 Position.get_file(props), |
|
108 Position.get_line(props), |
|
109 Position.get_id(props), |
|
110 Position.get_offset(props)))) |
|
111 case _ => state |
|
112 } |
|
113 } |
|
114 else { |
|
115 state.add_markup( |
|
116 command.markup_node(begin - 1, end - 1, |
|
117 Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) |
|
118 } |
|
119 case _ => state |
|
120 } |
|
121 case _ => System.err.println("Ignored report message: " + elem); state |
|
122 }) |
|
123 case _ => add_result(message) |
|
124 } |
|
125 } |
|