author | wenzelm |
Sun, 22 Aug 2010 12:54:12 +0200 | |
changeset 38572 | 0fe2c01ef7da |
parent 38564 | a6e2715fac5f |
child 38574 | 79cb7b4c908a |
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 |
{ |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
17 |
case class TypeInfo(ty: String) |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
18 |
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
|
19 |
command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? |
38361 | 20 |
|
21 |
||
38362 | 22 |
|
38361 | 23 |
/** accumulated results from prover **/ |
24 |
||
38362 | 25 |
case class State( |
38361 | 26 |
val command: Command, |
38480
e5eed57913d0
Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents:
38479
diff
changeset
|
27 |
val status: List[XML.Tree], |
38361 | 28 |
val reverse_results: List[XML.Tree], |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
29 |
val markup: Markup_Tree) |
38361 | 30 |
{ |
31 |
/* content */ |
|
32 |
||
38362 | 33 |
lazy val results = reverse_results.reverse |
38361 | 34 |
|
38362 | 35 |
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) |
38361 | 36 |
|
38564 | 37 |
def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node) |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
38 |
|
38564 | 39 |
def markup_root_node: Markup_Tree.Node[Any] = |
38480
e5eed57913d0
Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents:
38479
diff
changeset
|
40 |
new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status)) |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
41 |
def markup_root: Markup_Tree = markup + markup_root_node |
38361 | 42 |
|
43 |
||
44 |
/* markup */ |
|
45 |
||
38564 | 46 |
private lazy val types: List[Markup_Tree.Node[Any]] = |
38362 | 47 |
markup.filter(_.info match { |
38361 | 48 |
case Command.TypeInfo(_) => true |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
49 |
case _ => false }).flatten(markup_root_node) |
38361 | 50 |
|
38426 | 51 |
def type_at(pos: Text.Offset): Option[String] = |
38361 | 52 |
{ |
38427 | 53 |
types.find(_.range.contains(pos)) match { |
38361 | 54 |
case Some(t) => |
55 |
t.info match { |
|
38426 | 56 |
case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty) |
38361 | 57 |
case _ => None |
58 |
} |
|
59 |
case None => None |
|
60 |
} |
|
61 |
} |
|
62 |
||
38564 | 63 |
private lazy val refs: List[Markup_Tree.Node[Any]] = |
38362 | 64 |
markup.filter(_.info match { |
38361 | 65 |
case Command.RefInfo(_, _, _, _) => true |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
66 |
case _ => false }).flatten(markup_root_node) |
38361 | 67 |
|
38564 | 68 |
def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] = |
38427 | 69 |
refs.find(_.range.contains(pos)) |
38361 | 70 |
|
71 |
||
72 |
/* message dispatch */ |
|
73 |
||
74 |
def accumulate(message: XML.Tree): Command.State = |
|
75 |
message match { |
|
38480
e5eed57913d0
Command.status: full XML.Tree, i.e. Markup with potential "arguments";
wenzelm
parents:
38479
diff
changeset
|
76 |
case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
77 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
78 |
(this /: msgs)((state, msg) => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
79 |
msg match { |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
80 |
case XML.Elem(Markup(name, atts), args) |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
81 |
if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined => |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
82 |
val range = command.decode_range(Position.get_range(atts).get) |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
83 |
val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
84 |
val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args)) |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
85 |
add_markup(node) |
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
86 |
case _ => System.err.println("Ignored report message: " + msg); state |
38361 | 87 |
}) |
88 |
case _ => add_result(message) |
|
89 |
} |
|
90 |
} |
|
38367 | 91 |
|
92 |
||
93 |
/* unparsed dummy commands */ |
|
94 |
||
95 |
def unparsed(source: String) = |
|
96 |
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
|
97 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
98 |
|
38361 | 99 |
|
34697 | 100 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
101 |
val id: Document.Command_ID, |
38373 | 102 |
val span: List[Token]) |
34451 | 103 |
{ |
34859 | 104 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
105 |
|
36012 | 106 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 107 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 108 |
def is_malformed: Boolean = !is_command && !is_ignored |
109 |
||
38367 | 110 |
def is_unparsed = id == Document.NO_ID |
111 |
||
36012 | 112 |
def name: String = if (is_command) span.head.content else "" |
37129 | 113 |
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
|
114 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 115 |
|
34859 | 116 |
|
117 |
/* source text */ |
|
34451 | 118 |
|
34859 | 119 |
val source: String = span.map(_.source).mkString |
38426 | 120 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
34859 | 121 |
def length: Int = source.length |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
122 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
123 |
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
|
124 |
|
34859 | 125 |
lazy val symbol_index = new Symbol.Index(source) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
126 |
def decode_range(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
|
127 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
128 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
129 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
130 |
|
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38476
diff
changeset
|
131 |
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
|
132 |
} |