author | wenzelm |
Sat, 14 Aug 2010 23:01:53 +0200 | |
changeset 38415 | f3220ef79d51 |
parent 38373 | e8197eea3cd0 |
child 38426 | 2858ec7b6dd8 |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/command.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Prover commands with semantic state. |
|
6 |
*/ |
|
34407 | 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:
34865
diff
changeset
|
8 |
package isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
34451 | 10 |
|
34699 | 11 |
import scala.actors.Actor, Actor._ |
34497 | 12 |
import scala.collection.mutable |
34486 | 13 |
|
34451 | 14 |
|
34637 | 15 |
object Command |
16 |
{ |
|
17 |
object Status extends Enumeration |
|
18 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
val UNPROCESSED = Value("UNPROCESSED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
val FINISHED = Value("FINISHED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
val FAILED = Value("FAILED") |
36990
449628c148cf
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
wenzelm
parents:
36676
diff
changeset
|
22 |
val UNDEFINED = Value("UNDEFINED") |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
} |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
24 |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
25 |
case class HighlightInfo(kind: String, sub_kind: Option[String]) { |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
26 |
override def toString = kind |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
27 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
28 |
case class TypeInfo(ty: String) |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
29 |
case class RefInfo(file: Option[String], line: Option[Int], |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38362
diff
changeset
|
30 |
command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? |
38361 | 31 |
|
32 |
||
38362 | 33 |
|
38361 | 34 |
/** accumulated results from prover **/ |
35 |
||
38362 | 36 |
case class State( |
38361 | 37 |
val command: Command, |
38 |
val status: Command.Status.Value, |
|
39 |
val forks: Int, |
|
40 |
val reverse_results: List[XML.Tree], |
|
38362 | 41 |
val markup: Markup_Text) |
38361 | 42 |
{ |
43 |
/* content */ |
|
44 |
||
38362 | 45 |
lazy val results = reverse_results.reverse |
38361 | 46 |
|
38362 | 47 |
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) |
38361 | 48 |
|
38362 | 49 |
def add_markup(node: Markup_Tree): State = copy(markup = markup + node) |
38361 | 50 |
|
51 |
||
52 |
/* markup */ |
|
53 |
||
54 |
lazy val highlight: Markup_Text = |
|
55 |
{ |
|
38362 | 56 |
markup.filter(_.info match { |
38361 | 57 |
case Command.HighlightInfo(_, _) => true |
58 |
case _ => false |
|
59 |
}) |
|
60 |
} |
|
61 |
||
62 |
private lazy val types: List[Markup_Node] = |
|
38362 | 63 |
markup.filter(_.info match { |
38361 | 64 |
case Command.TypeInfo(_) => true |
65 |
case _ => false }).flatten |
|
66 |
||
67 |
def type_at(pos: Int): Option[String] = |
|
68 |
{ |
|
69 |
types.find(t => t.start <= pos && pos < t.stop) match { |
|
70 |
case Some(t) => |
|
71 |
t.info match { |
|
72 |
case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) |
|
73 |
case _ => None |
|
74 |
} |
|
75 |
case None => None |
|
76 |
} |
|
77 |
} |
|
78 |
||
79 |
private lazy val refs: List[Markup_Node] = |
|
38362 | 80 |
markup.filter(_.info match { |
38361 | 81 |
case Command.RefInfo(_, _, _, _) => true |
82 |
case _ => false }).flatten |
|
83 |
||
84 |
def ref_at(pos: Int): Option[Markup_Node] = |
|
85 |
refs.find(t => t.start <= pos && pos < t.stop) |
|
86 |
||
87 |
||
88 |
/* message dispatch */ |
|
89 |
||
90 |
def accumulate(message: XML.Tree): Command.State = |
|
91 |
message match { |
|
92 |
case XML.Elem(Markup(Markup.STATUS, _), elems) => |
|
93 |
(this /: elems)((state, elem) => |
|
94 |
elem match { |
|
38362 | 95 |
case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED) |
96 |
case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED) |
|
97 |
case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED) |
|
98 |
case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1) |
|
99 |
case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1) |
|
38361 | 100 |
case _ => System.err.println("Ignored status message: " + elem); state |
101 |
}) |
|
102 |
||
103 |
case XML.Elem(Markup(Markup.REPORT, _), elems) => |
|
104 |
(this /: elems)((state, elem) => |
|
105 |
elem match { |
|
106 |
case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => |
|
107 |
atts match { |
|
108 |
case Position.Range(begin, end) => |
|
109 |
if (kind == Markup.ML_TYPING) { |
|
110 |
val info = Pretty.string_of(body, margin = 40) |
|
111 |
state.add_markup( |
|
112 |
command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) |
|
113 |
} |
|
114 |
else if (kind == Markup.ML_REF) { |
|
115 |
body match { |
|
116 |
case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => |
|
38362 | 117 |
state.add_markup( |
118 |
command.markup_node( |
|
119 |
begin - 1, end - 1, |
|
120 |
Command.RefInfo( |
|
121 |
Position.get_file(props), |
|
122 |
Position.get_line(props), |
|
123 |
Position.get_id(props), |
|
124 |
Position.get_offset(props)))) |
|
38361 | 125 |
case _ => state |
126 |
} |
|
127 |
} |
|
128 |
else { |
|
129 |
state.add_markup( |
|
130 |
command.markup_node(begin - 1, end - 1, |
|
131 |
Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) |
|
132 |
} |
|
133 |
case _ => state |
|
134 |
} |
|
135 |
case _ => System.err.println("Ignored report message: " + elem); state |
|
136 |
}) |
|
137 |
case _ => add_result(message) |
|
138 |
} |
|
139 |
} |
|
38367 | 140 |
|
141 |
||
142 |
/* unparsed dummy commands */ |
|
143 |
||
144 |
def unparsed(source: String) = |
|
145 |
new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source))) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
147 |
|
38361 | 148 |
|
34697 | 149 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
150 |
val id: Document.Command_ID, |
38373 | 151 |
val span: List[Token]) |
34451 | 152 |
{ |
34859 | 153 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
154 |
|
36012 | 155 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 156 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 157 |
def is_malformed: Boolean = !is_command && !is_ignored |
158 |
||
38367 | 159 |
def is_unparsed = id == Document.NO_ID |
160 |
||
36012 | 161 |
def name: String = if (is_command) span.head.content else "" |
37129 | 162 |
override def toString = |
37373
25078ba44436
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
wenzelm
parents:
37197
diff
changeset
|
163 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 164 |
|
34859 | 165 |
|
166 |
/* source text */ |
|
34451 | 167 |
|
34859 | 168 |
val source: String = span.map(_.source).mkString |
169 |
def source(i: Int, j: Int): String = source.substring(i, j) |
|
170 |
def length: Int = source.length |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34835
diff
changeset
|
171 |
|
34859 | 172 |
lazy val symbol_index = new Symbol.Index(source) |
34593 | 173 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
174 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
175 |
/* markup */ |
34508 | 176 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
177 |
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = |
34699 | 178 |
{ |
34703 | 179 |
val start = symbol_index.decode(begin) |
180 |
val stop = symbol_index.decode(end) |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
181 |
new Markup_Tree(new Markup_Node(start, stop, info), Nil) |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
182 |
} |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
183 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
184 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
185 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
186 |
|
38415
f3220ef79d51
Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
wenzelm
parents:
38373
diff
changeset
|
187 |
val empty_state: Command.State = |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
188 |
Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source)) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
189 |
} |