author | wenzelm |
Wed, 25 Aug 2010 22:45:24 +0200 | |
changeset 38723 | 6a55b8978a56 |
parent 38722 | ba31936497c2 |
child 38872 | 26c505765024 |
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 |
|
34637 | 11 |
object Command |
12 |
{ |
|
38361 | 13 |
/** accumulated results from prover **/ |
14 |
||
38362 | 15 |
case class State( |
38361 | 16 |
val command: Command, |
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38579
diff
changeset
|
17 |
val status: List[Markup], |
38361 | 18 |
val reverse_results: List[XML.Tree], |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
19 |
val markup: Markup_Tree) |
38361 | 20 |
{ |
21 |
/* content */ |
|
22 |
||
38362 | 23 |
lazy val results = reverse_results.reverse |
38361 | 24 |
|
38714 | 25 |
def add_status(st: Markup): State = copy(status = st :: status) |
26 |
def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info) |
|
38362 | 27 |
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) |
38361 | 28 |
|
38658 | 29 |
def root_info: Text.Info[Any] = |
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38579
diff
changeset
|
30 |
new Text.Info(command.range, |
38658 | 31 |
XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil)))) |
32 |
def root_markup: Markup_Tree = markup + root_info |
|
38361 | 33 |
|
34 |
||
35 |
/* message dispatch */ |
|
36 |
||
37 |
def accumulate(message: XML.Tree): Command.State = |
|
38 |
message match { |
|
38714 | 39 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
40 |
(this /: msgs)((state, msg) => |
|
41 |
msg match { |
|
42 |
case XML.Elem(markup, Nil) => state.add_status(markup) |
|
43 |
case _ => System.err.println("Ignored status message: " + msg); state |
|
44 |
}) |
|
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38579
diff
changeset
|
45 |
|
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
46 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
47 |
(this /: msgs)((state, msg) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
48 |
msg match { |
38723 | 49 |
case XML.Elem(Markup(name, atts @ Position.Range(range)), args) |
50 |
if Position.Id.unapply(atts) == Some(command.id) => |
|
51 |
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
|
52 |
val info = |
|
53 |
Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args)) |
|
54 |
state.add_markup(info) |
|
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
55 |
case _ => System.err.println("Ignored report message: " + msg); state |
38361 | 56 |
}) |
57 |
case _ => add_result(message) |
|
58 |
} |
|
59 |
} |
|
38367 | 60 |
|
61 |
||
62 |
/* unparsed dummy commands */ |
|
63 |
||
64 |
def unparsed(source: String) = |
|
65 |
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
|
66 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
67 |
|
38361 | 68 |
|
34697 | 69 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
70 |
val id: Document.Command_ID, |
38373 | 71 |
val span: List[Token]) |
34451 | 72 |
{ |
34859 | 73 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
74 |
|
36012 | 75 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 76 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 77 |
def is_malformed: Boolean = !is_command && !is_ignored |
78 |
||
38367 | 79 |
def is_unparsed = id == Document.NO_ID |
80 |
||
36012 | 81 |
def name: String = if (is_command) span.head.content else "" |
37129 | 82 |
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
|
83 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 84 |
|
34859 | 85 |
|
86 |
/* source text */ |
|
34451 | 87 |
|
34859 | 88 |
val source: String = span.map(_.source).mkString |
38426 | 89 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
34859 | 90 |
def length: Int = source.length |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
91 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
92 |
val range: Text.Range = Text.Range(0, length) |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34835
diff
changeset
|
93 |
|
34859 | 94 |
lazy val symbol_index = new Symbol.Index(source) |
38579 | 95 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
96 |
def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
97 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
98 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
99 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
100 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
101 |
val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
102 |
} |