author | wenzelm |
Mon, 31 Mar 2014 15:05:24 +0200 | |
changeset 56335 | 8953d4cc060a |
parent 56301 | 1da7b4c33db9 |
child 56359 | bca016a9a18d |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/command.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
52536 | 5 |
Prover commands with accumulated results from execution. |
36676 | 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 |
|
45644 | 11 |
import scala.collection.mutable |
38872 | 12 |
import scala.collection.immutable.SortedMap |
13 |
||
14 |
||
34637 | 15 |
object Command |
16 |
{ |
|
52849 | 17 |
type Edit = (Option[Command], Option[Command]) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
18 |
type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])] |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
19 |
|
52849 | 20 |
|
21 |
||
38361 | 22 |
/** accumulated results from prover **/ |
23 |
||
50507 | 24 |
/* results */ |
25 |
||
26 |
object Results |
|
27 |
{ |
|
51496
cb677987b7e3
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents:
51494
diff
changeset
|
28 |
type Entry = (Long, XML.Tree) |
50507 | 29 |
val empty = new Results(SortedMap.empty) |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
30 |
def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _) |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
31 |
def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _) |
50507 | 32 |
} |
33 |
||
51494 | 34 |
final class Results private(private val rep: SortedMap[Long, XML.Tree]) |
50507 | 35 |
{ |
36 |
def defined(serial: Long): Boolean = rep.isDefinedAt(serial) |
|
37 |
def get(serial: Long): Option[XML.Tree] = rep.get(serial) |
|
51496
cb677987b7e3
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents:
51494
diff
changeset
|
38 |
def entries: Iterator[Results.Entry] = rep.iterator |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
39 |
|
51496
cb677987b7e3
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm
parents:
51494
diff
changeset
|
40 |
def + (entry: Results.Entry): Results = |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
41 |
if (defined(entry._1)) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
42 |
else new Results(rep + entry) |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
43 |
|
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
44 |
def ++ (other: Results): Results = |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
45 |
if (this eq other) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
46 |
else if (rep.isEmpty) other |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
47 |
else (this /: other.entries)(_ + _) |
50540 | 48 |
|
51494 | 49 |
override def hashCode: Int = rep.hashCode |
50 |
override def equals(that: Any): Boolean = |
|
51 |
that match { |
|
52 |
case other: Results => rep == other.rep |
|
53 |
case _ => false |
|
54 |
} |
|
50540 | 55 |
override def toString: String = entries.mkString("Results(", ", ", ")") |
50507 | 56 |
} |
57 |
||
58 |
||
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
59 |
/* markup */ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
60 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
61 |
object Markup_Index |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
62 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
63 |
val markup: Markup_Index = Markup_Index(false, "") |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
64 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
65 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
66 |
sealed case class Markup_Index(status: Boolean, file_name: String) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
67 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
68 |
object Markups |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
69 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
70 |
val empty: Markups = new Markups(Map.empty) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
71 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
72 |
def init(markup: Markup_Tree): Markups = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
73 |
new Markups(Map(Markup_Index.markup -> markup)) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
74 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
75 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
76 |
final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
77 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
78 |
def apply(index: Markup_Index): Markup_Tree = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
79 |
rep.getOrElse(index, Markup_Tree.empty) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
80 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
81 |
def add(index: Markup_Index, markup: Text.Markup): Markups = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
82 |
new Markups(rep + (index -> (this(index) + markup))) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
83 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
84 |
override def hashCode: Int = rep.hashCode |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
85 |
override def equals(that: Any): Boolean = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
86 |
that match { |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
87 |
case other: Markups => rep == other.rep |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
88 |
case _ => false |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
89 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
90 |
override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
91 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
92 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
93 |
|
50507 | 94 |
/* state */ |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
95 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
96 |
object State |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
97 |
{ |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
98 |
def merge_results(states: List[State]): Command.Results = |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
99 |
Results.merge(states.map(_.results)) |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
100 |
|
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
101 |
def merge_markup(states: List[State], index: Markup_Index, |
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
102 |
range: Text.Range, elements: Document.Elements): Markup_Tree = |
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
103 |
Markup_Tree.merge(states.map(_.markup(index)), range, elements) |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
104 |
} |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
105 |
|
43714 | 106 |
sealed case class State( |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
107 |
command: Command, |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
108 |
status: List[Markup] = Nil, |
50507 | 109 |
results: Results = Results.empty, |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
110 |
markups: Markups = Markups.empty) |
38361 | 111 |
{ |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
112 |
/* markup */ |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
113 |
|
55650 | 114 |
def markup(index: Markup_Index): Markup_Tree = markups(index) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
115 |
|
49614 | 116 |
|
51494 | 117 |
/* content */ |
118 |
||
119 |
def eq_content(other: State): Boolean = |
|
120 |
command.source == other.command.source && |
|
121 |
status == other.status && |
|
122 |
results == other.results && |
|
55434 | 123 |
markups == other.markups |
38361 | 124 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
125 |
private def add_status(st: Markup): State = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
126 |
copy(status = st :: status) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
127 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
128 |
private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
129 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
130 |
val markups1 = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
131 |
if (status || Protocol.status_elements(m.info.name)) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
132 |
markups.add(Markup_Index(true, file_name), m) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
133 |
else markups |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
134 |
copy(markups = markups1.add(Markup_Index(false, file_name), m)) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
135 |
} |
38361 | 136 |
|
56295
a40e67ce4f84
clarified valid_id: always standardize towards static command.id;
wenzelm
parents:
55884
diff
changeset
|
137 |
def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State = |
38361 | 138 |
message match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
139 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
38714 | 140 |
(this /: msgs)((state, msg) => |
141 |
msg match { |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
142 |
case elem @ XML.Elem(markup, Nil) => |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
143 |
state. |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
144 |
add_status(markup). |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
145 |
add_markup(true, "", Text.Info(command.proper_range, elem)) |
52536 | 146 |
case _ => |
55618 | 147 |
System.err.println("Ignored status message: " + msg) |
52536 | 148 |
state |
38714 | 149 |
}) |
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
|
150 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
151 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
152 |
(this /: msgs)((state, msg) => |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
153 |
{ |
55618 | 154 |
def bad(): Unit = System.err.println("Ignored report message: " + msg) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
155 |
|
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
156 |
msg match { |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
157 |
case XML.Elem(Markup(name, |
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
158 |
atts @ Position.Reported(id, file_name, symbol_range)), args) |
56295
a40e67ce4f84
clarified valid_id: always standardize towards static command.id;
wenzelm
parents:
55884
diff
changeset
|
159 |
if valid_id(id) => |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
160 |
command.chunks.get(file_name) match { |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
161 |
case Some(chunk) => |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
162 |
chunk.incorporate(symbol_range) match { |
55548
a645277885cf
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents:
55434
diff
changeset
|
163 |
case Some(range) => |
55822
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
164 |
val props = Position.purge(atts) |
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
165 |
val info = Text.Info(range, XML.Elem(Markup(name, props), args)) |
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
166 |
state.add_markup(false, file_name, info) |
55548
a645277885cf
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents:
55434
diff
changeset
|
167 |
case None => bad(); state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
168 |
} |
55548
a645277885cf
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents:
55434
diff
changeset
|
169 |
case None => bad(); state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
170 |
} |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
171 |
|
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
172 |
case XML.Elem(Markup(name, atts), args) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
173 |
if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
174 |
val range = command.proper_range |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
175 |
val props = Position.purge(atts) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
176 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
177 |
state.add_markup(false, "", info) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
178 |
|
55548
a645277885cf
more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;
wenzelm
parents:
55434
diff
changeset
|
179 |
case _ => /* FIXME bad(); */ state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
180 |
} |
38361 | 181 |
}) |
52930
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
182 |
case XML.Elem(Markup(name, props), body) => |
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
183 |
props match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
184 |
case Markup.Serial(i) => |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
185 |
val message1 = XML.Elem(Markup(Markup.message(name), props), body) |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
186 |
val message2 = XML.Elem(Markup(name, props), body) |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
187 |
|
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
188 |
var st = copy(results = results + (i -> message1)) |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
189 |
if (Protocol.is_inlined(message)) { |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
190 |
for { |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
191 |
(file_name, chunk) <- command.chunks |
56295
a40e67ce4f84
clarified valid_id: always standardize towards static command.id;
wenzelm
parents:
55884
diff
changeset
|
192 |
range <- Protocol.message_positions(valid_id, chunk, message) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
193 |
} st = st.add_markup(false, file_name, Text.Info(range, message2)) |
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
194 |
} |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
195 |
st |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
196 |
|
52536 | 197 |
case _ => |
55618 | 198 |
System.err.println("Ignored message without serial number: " + message) |
52536 | 199 |
this |
38872 | 200 |
} |
56295
a40e67ce4f84
clarified valid_id: always standardize towards static command.id;
wenzelm
parents:
55884
diff
changeset
|
201 |
} |
38361 | 202 |
} |
38367 | 203 |
|
204 |
||
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
205 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
206 |
/** static content **/ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
207 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
208 |
/* text chunks */ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
209 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
210 |
abstract class Chunk |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
211 |
{ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
212 |
def file_name: String |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
213 |
def length: Int |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
214 |
def range: Text.Range |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
215 |
def decode(symbol_range: Symbol.Range): Text.Range |
55822
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
216 |
|
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
217 |
def incorporate(symbol_range: Symbol.Range): Option[Text.Range] = |
55822
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
218 |
{ |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
219 |
def inc(r: Symbol.Range): Option[Text.Range] = |
55822
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
220 |
range.try_restrict(decode(r)) match { |
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
221 |
case Some(r1) if !r1.is_singularity => Some(r1) |
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
222 |
case _ => None |
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
223 |
} |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
224 |
inc(symbol_range) orElse inc(symbol_range - 1) |
55822
ccf2d784be97
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
wenzelm
parents:
55785
diff
changeset
|
225 |
} |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
226 |
} |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
227 |
|
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
228 |
// file name and position information, *without* persistent text |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
229 |
class File(val file_name: String, text: CharSequence) extends Chunk |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
230 |
{ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
231 |
val length = text.length |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
232 |
val range = Text.Range(0, length) |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
233 |
private val symbol_index = Symbol.Index(text) |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
234 |
def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range) |
55777 | 235 |
|
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
236 |
private val hash: Int = (file_name, length, symbol_index).hashCode |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
237 |
override def hashCode: Int = hash |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
238 |
override def equals(that: Any): Boolean = |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
239 |
that match { |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
240 |
case other: File => |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
241 |
hash == other.hash && |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
242 |
file_name == other.file_name && |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
243 |
length == other.length && |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
244 |
symbol_index == other.symbol_index |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
245 |
case _ => false |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56301
diff
changeset
|
246 |
} |
55777 | 247 |
override def toString: String = "Command.File(" + file_name + ")" |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
248 |
} |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
249 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
250 |
|
45644 | 251 |
/* make commands */ |
252 |
||
54462 | 253 |
def name(span: List[Token]): String = |
254 |
span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" } |
|
48745 | 255 |
|
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
256 |
private def source_span(span: List[Token]): (String, List[Token]) = |
45644 | 257 |
{ |
258 |
val source: String = |
|
48745 | 259 |
span match { |
45644 | 260 |
case List(tok) => tok.source |
48745 | 261 |
case _ => span.map(_.source).mkString |
45644 | 262 |
} |
263 |
||
48745 | 264 |
val span1 = new mutable.ListBuffer[Token] |
45644 | 265 |
var i = 0 |
48745 | 266 |
for (Token(kind, s) <- span) { |
45644 | 267 |
val n = s.length |
268 |
val s1 = source.substring(i, i + n) |
|
48745 | 269 |
span1 += Token(kind, s1) |
45644 | 270 |
i += n |
271 |
} |
|
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
272 |
(source, span1.toList) |
45644 | 273 |
} |
274 |
||
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
275 |
def apply( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
276 |
id: Document_ID.Command, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
277 |
node_name: Document.Node.Name, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
278 |
blobs: List[Blob], |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
279 |
span: List[Token]): Command = |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
280 |
{ |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
281 |
val (source, span1) = source_span(span) |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
282 |
new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty) |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
283 |
} |
49414 | 284 |
|
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
285 |
val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil) |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
286 |
|
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
287 |
def unparsed( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
288 |
id: Document_ID.Command, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
289 |
source: String, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
290 |
results: Results, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
291 |
markup: Markup_Tree): Command = |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
292 |
{ |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
293 |
val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source))) |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
294 |
new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup) |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
295 |
} |
49414 | 296 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
297 |
def unparsed(source: String): Command = |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
298 |
unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty) |
44384 | 299 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
300 |
def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = |
49414 | 301 |
{ |
49466 | 302 |
val text = XML.content(body) |
303 |
val markup = Markup_Tree.from_XML(body) |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
304 |
unparsed(id, text, results, markup) |
49414 | 305 |
} |
49359
c1262d7389fb
refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents:
49037
diff
changeset
|
306 |
|
44384 | 307 |
|
308 |
/* perspective */ |
|
309 |
||
44474 | 310 |
object Perspective |
311 |
{ |
|
312 |
val empty: Perspective = Perspective(Nil) |
|
313 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
314 |
|
44474 | 315 |
sealed case class Perspective(commands: List[Command]) // visible commands in canonical order |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
316 |
{ |
44474 | 317 |
def same(that: Perspective): Boolean = |
318 |
{ |
|
319 |
val cmds1 = this.commands |
|
320 |
val cmds2 = that.commands |
|
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
321 |
require(!cmds1.exists(_.is_undefined)) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
322 |
require(!cmds2.exists(_.is_undefined)) |
44474 | 323 |
cmds1.length == cmds2.length && |
324 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) |
|
325 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
326 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
327 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
328 |
|
38361 | 329 |
|
46712 | 330 |
final class Command private( |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
331 |
val id: Document_ID.Command, |
44615 | 332 |
val node_name: Document.Node.Name, |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
333 |
val blobs: List[Command.Blob], |
52535
b7badd371e4d
tuned signature -- eliminated pointless type synonym;
wenzelm
parents:
52531
diff
changeset
|
334 |
val span: List[Token], |
49414 | 335 |
val source: String, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
336 |
val init_results: Command.Results, |
49414 | 337 |
val init_markup: Markup_Tree) |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
338 |
extends Command.Chunk |
34451 | 339 |
{ |
34859 | 340 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
341 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
342 |
def is_undefined: Boolean = id == Document_ID.none |
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
343 |
val is_unparsed: Boolean = span.exists(_.is_unparsed) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
344 |
val is_unfinished: Boolean = span.exists(_.is_unfinished) |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
345 |
|
48599 | 346 |
val is_ignored: Boolean = !span.exists(_.is_proper) |
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
347 |
val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error)) |
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46910
diff
changeset
|
348 |
def is_command: Boolean = !is_ignored && !is_malformed |
34859 | 349 |
|
54462 | 350 |
def name: String = Command.name(span) |
47012
0e246130486b
clarified command span classification: strict Command.is_command, permissive Command.name;
wenzelm
parents:
46910
diff
changeset
|
351 |
|
37129 | 352 |
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
|
353 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 354 |
|
34859 | 355 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
356 |
/* blobs */ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
357 |
|
55785 | 358 |
def blobs_changed(doc_blobs: Document.Blobs): Boolean = |
359 |
blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false }) |
|
360 |
||
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
361 |
def blobs_names: List[Document.Node.Name] = |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
362 |
for (Exn.Res((name, _)) <- blobs) yield name |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
363 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
364 |
def blobs_digests: List[SHA1.Digest] = |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
365 |
for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
366 |
|
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
367 |
val chunks: Map[String, Command.Chunk] = |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
368 |
(("" -> this) :: |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
369 |
(for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
370 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
371 |
|
52509 | 372 |
/* source */ |
34451 | 373 |
|
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
374 |
def file_name: String = "" |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
375 |
|
46813 | 376 |
def length: Int = source.length |
377 |
val range: Text.Range = Text.Range(0, length) |
|
378 |
||
379 |
val proper_range: Text.Range = |
|
51048
123be08eed88
clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
wenzelm
parents:
50540
diff
changeset
|
380 |
Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) |
46813 | 381 |
|
38426 | 382 |
def source(range: Text.Range): String = source.substring(range.start, range.stop) |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
383 |
|
55430 | 384 |
private lazy val symbol_index = Symbol.Index(source) |
55884
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
385 |
def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset) |
f2c0eaedd579
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents:
55822
diff
changeset
|
386 |
def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
387 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
388 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
389 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
390 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
391 |
val init_state: Command.State = |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
392 |
Command.State(this, results = init_results, markups = Command.Markups.init(init_markup)) |
52527
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52524
diff
changeset
|
393 |
|
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52524
diff
changeset
|
394 |
val empty_state: Command.State = Command.State(this) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
395 |
} |