author | wenzelm |
Wed, 18 Aug 2010 11:25:09 +0200 | |
changeset 38476 | d72479a07882 |
parent 38429 | 9951852fae91 |
child 38479 | e628da370072 |
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 |
{ |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
17 |
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
|
18 |
override def toString = kind |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
19 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
20 |
case class TypeInfo(ty: String) |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
21 |
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
|
22 |
command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? |
38361 | 23 |
|
24 |
||
38362 | 25 |
|
38361 | 26 |
/** accumulated results from prover **/ |
27 |
||
38362 | 28 |
case class State( |
38361 | 29 |
val command: Command, |
38429
9951852fae91
simplified command status: interpret stacked markup on demand;
wenzelm
parents:
38427
diff
changeset
|
30 |
val status: List[Markup], |
38361 | 31 |
val reverse_results: List[XML.Tree], |
38362 | 32 |
val markup: Markup_Text) |
38361 | 33 |
{ |
34 |
/* content */ |
|
35 |
||
38362 | 36 |
lazy val results = reverse_results.reverse |
38361 | 37 |
|
38362 | 38 |
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) |
38361 | 39 |
|
38362 | 40 |
def add_markup(node: Markup_Tree): State = copy(markup = markup + node) |
38361 | 41 |
|
42 |
||
43 |
/* markup */ |
|
44 |
||
45 |
lazy val highlight: Markup_Text = |
|
46 |
{ |
|
38362 | 47 |
markup.filter(_.info match { |
38361 | 48 |
case Command.HighlightInfo(_, _) => true |
49 |
case _ => false |
|
50 |
}) |
|
51 |
} |
|
52 |
||
53 |
private lazy val types: List[Markup_Node] = |
|
38362 | 54 |
markup.filter(_.info match { |
38361 | 55 |
case Command.TypeInfo(_) => true |
56 |
case _ => false }).flatten |
|
57 |
||
38426 | 58 |
def type_at(pos: Text.Offset): Option[String] = |
38361 | 59 |
{ |
38427 | 60 |
types.find(_.range.contains(pos)) match { |
38361 | 61 |
case Some(t) => |
62 |
t.info match { |
|
38426 | 63 |
case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty) |
38361 | 64 |
case _ => None |
65 |
} |
|
66 |
case None => None |
|
67 |
} |
|
68 |
} |
|
69 |
||
70 |
private lazy val refs: List[Markup_Node] = |
|
38362 | 71 |
markup.filter(_.info match { |
38361 | 72 |
case Command.RefInfo(_, _, _, _) => true |
73 |
case _ => false }).flatten |
|
74 |
||
38426 | 75 |
def ref_at(pos: Text.Offset): Option[Markup_Node] = |
38427 | 76 |
refs.find(_.range.contains(pos)) |
38361 | 77 |
|
78 |
||
79 |
/* message dispatch */ |
|
80 |
||
81 |
def accumulate(message: XML.Tree): Command.State = |
|
82 |
message match { |
|
83 |
case XML.Elem(Markup(Markup.STATUS, _), elems) => |
|
38429
9951852fae91
simplified command status: interpret stacked markup on demand;
wenzelm
parents:
38427
diff
changeset
|
84 |
copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status) |
38361 | 85 |
|
86 |
case XML.Elem(Markup(Markup.REPORT, _), elems) => |
|
87 |
(this /: elems)((state, elem) => |
|
88 |
elem match { |
|
89 |
case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => |
|
90 |
atts match { |
|
91 |
case Position.Range(begin, end) => |
|
92 |
if (kind == Markup.ML_TYPING) { |
|
93 |
val info = Pretty.string_of(body, margin = 40) |
|
94 |
state.add_markup( |
|
38476 | 95 |
command.markup_node(begin, end, Command.TypeInfo(info))) |
38361 | 96 |
} |
97 |
else if (kind == Markup.ML_REF) { |
|
98 |
body match { |
|
99 |
case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => |
|
38362 | 100 |
state.add_markup( |
101 |
command.markup_node( |
|
38476 | 102 |
begin, end, |
38362 | 103 |
Command.RefInfo( |
104 |
Position.get_file(props), |
|
105 |
Position.get_line(props), |
|
106 |
Position.get_id(props), |
|
107 |
Position.get_offset(props)))) |
|
38361 | 108 |
case _ => state |
109 |
} |
|
110 |
} |
|
111 |
else { |
|
112 |
state.add_markup( |
|
38476 | 113 |
command.markup_node(begin, end, |
38361 | 114 |
Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) |
115 |
} |
|
116 |
case _ => state |
|
117 |
} |
|
118 |
case _ => System.err.println("Ignored report message: " + elem); state |
|
119 |
}) |
|
120 |
case _ => add_result(message) |
|
121 |
} |
|
122 |
} |
|
38367 | 123 |
|
124 |
||
125 |
/* unparsed dummy commands */ |
|
126 |
||
127 |
def unparsed(source: String) = |
|
128 |
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
|
129 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
130 |
|
38361 | 131 |
|
34697 | 132 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
133 |
val id: Document.Command_ID, |
38373 | 134 |
val span: List[Token]) |
34451 | 135 |
{ |
34859 | 136 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
137 |
|
36012 | 138 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 139 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 140 |
def is_malformed: Boolean = !is_command && !is_ignored |
141 |
||
38367 | 142 |
def is_unparsed = id == Document.NO_ID |
143 |
||
36012 | 144 |
def name: String = if (is_command) span.head.content else "" |
37129 | 145 |
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
|
146 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 147 |
|
34859 | 148 |
|
149 |
/* source text */ |
|
34451 | 150 |
|
34859 | 151 |
val source: String = span.map(_.source).mkString |
38426 | 152 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
34859 | 153 |
def length: Int = source.length |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34835
diff
changeset
|
154 |
|
34859 | 155 |
lazy val symbol_index = new Symbol.Index(source) |
34593 | 156 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
157 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
158 |
/* markup */ |
34508 | 159 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
160 |
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = |
34699 | 161 |
{ |
38476 | 162 |
val start = symbol_index.decode(begin - 1) |
163 |
val stop = symbol_index.decode(end - 1) |
|
38426 | 164 |
new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil) |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
165 |
} |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
166 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
167 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
168 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
169 |
|
38429
9951852fae91
simplified command status: interpret stacked markup on demand;
wenzelm
parents:
38427
diff
changeset
|
170 |
val empty_state: Command.State = Command.State(this, Nil, 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
|
171 |
} |