author | wenzelm |
Wed, 25 Aug 2010 22:37:53 +0200 | |
changeset 38722 | ba31936497c2 |
parent 38714 | 31da698fc4e5 |
child 38723 | 6a55b8978a56 |
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 { |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
49 |
case XML.Elem(Markup(name, atts), args) => |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
50 |
atts match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
51 |
case Position.Range(range) if Position.Id.unapply(atts) == Some(command.id) => |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
52 |
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
53 |
val info = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
54 |
Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args)) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
55 |
state.add_markup(info) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
56 |
case _ => System.err.println("Ignored report message: " + msg); state |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38714
diff
changeset
|
57 |
} |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
58 |
case _ => System.err.println("Ignored report message: " + msg); state |
38361 | 59 |
}) |
60 |
case _ => add_result(message) |
|
61 |
} |
|
62 |
} |
|
38367 | 63 |
|
64 |
||
65 |
/* unparsed dummy commands */ |
|
66 |
||
67 |
def unparsed(source: String) = |
|
68 |
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
|
69 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
70 |
|
38361 | 71 |
|
34697 | 72 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
73 |
val id: Document.Command_ID, |
38373 | 74 |
val span: List[Token]) |
34451 | 75 |
{ |
34859 | 76 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
77 |
|
36012 | 78 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 79 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 80 |
def is_malformed: Boolean = !is_command && !is_ignored |
81 |
||
38367 | 82 |
def is_unparsed = id == Document.NO_ID |
83 |
||
36012 | 84 |
def name: String = if (is_command) span.head.content else "" |
37129 | 85 |
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
|
86 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 87 |
|
34859 | 88 |
|
89 |
/* source text */ |
|
34451 | 90 |
|
34859 | 91 |
val source: String = span.map(_.source).mkString |
38426 | 92 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
34859 | 93 |
def length: Int = source.length |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
94 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
95 |
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
|
96 |
|
34859 | 97 |
lazy val symbol_index = new Symbol.Index(source) |
38579 | 98 |
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
99 |
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
|
100 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
101 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
102 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
103 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
104 |
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
|
105 |
} |