author | wenzelm |
Sat, 07 Jan 2017 19:36:40 +0100 | |
changeset 64823 | 78df3d65a1cc |
parent 64802 | adc4c84b692c |
child 64824 | 330ec9bc4b75 |
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 |
59705 | 13 |
import scala.util.parsing.input.CharSequenceReader |
38872 | 14 |
|
15 |
||
34637 | 16 |
object Command |
17 |
{ |
|
52849 | 18 |
type Edit = (Option[Command], Option[Command]) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
19 |
|
56746 | 20 |
type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])] |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
21 |
type Blobs_Info = (List[Blob], Int) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
22 |
val no_blobs: Blobs_Info = (Nil, -1) |
52849 | 23 |
|
24 |
||
38361 | 25 |
/** accumulated results from prover **/ |
26 |
||
50507 | 27 |
/* results */ |
28 |
||
29 |
object Results |
|
30 |
{ |
|
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
|
31 |
type Entry = (Long, XML.Tree) |
50507 | 32 |
val empty = new Results(SortedMap.empty) |
59072 | 33 |
def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) |
34 |
def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) |
|
50507 | 35 |
} |
36 |
||
51494 | 37 |
final class Results private(private val rep: SortedMap[Long, XML.Tree]) |
50507 | 38 |
{ |
64802 | 39 |
def is_empty: Boolean = rep.isEmpty |
50507 | 40 |
def defined(serial: Long): Boolean = rep.isDefinedAt(serial) |
41 |
def get(serial: Long): Option[XML.Tree] = rep.get(serial) |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
42 |
def iterator: Iterator[Results.Entry] = rep.iterator |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
43 |
|
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
|
44 |
def + (entry: Results.Entry): Results = |
50508
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
45 |
if (defined(entry._1)) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
46 |
else new Results(rep + entry) |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
47 |
|
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
48 |
def ++ (other: Results): Results = |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
49 |
if (this eq other) this |
5b7150395568
tuned implementation according to Library.insert/merge in ML;
wenzelm
parents:
50507
diff
changeset
|
50 |
else if (rep.isEmpty) other |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
51 |
else (this /: other.iterator)(_ + _) |
50540 | 52 |
|
51494 | 53 |
override def hashCode: Int = rep.hashCode |
54 |
override def equals(that: Any): Boolean = |
|
55 |
that match { |
|
56 |
case other: Results => rep == other.rep |
|
57 |
case _ => false |
|
58 |
} |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56359
diff
changeset
|
59 |
override def toString: String = iterator.mkString("Results(", ", ", ")") |
50507 | 60 |
} |
61 |
||
62 |
||
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
63 |
/* markup */ |
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 |
object Markup_Index |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
66 |
{ |
56746 | 67 |
val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
68 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
69 |
|
56746 | 70 |
sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) |
55649
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 |
object Markups |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
73 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
74 |
val empty: Markups = new Markups(Map.empty) |
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 |
def init(markup: Markup_Tree): Markups = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
77 |
new Markups(Map(Markup_Index.markup -> markup)) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
78 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
79 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
80 |
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
|
81 |
{ |
56489 | 82 |
def is_empty: Boolean = rep.isEmpty |
83 |
||
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
84 |
def apply(index: Markup_Index): Markup_Tree = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
85 |
rep.getOrElse(index, Markup_Tree.empty) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
86 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
87 |
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
|
88 |
new Markups(rep + (index -> (this(index) + markup))) |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
89 |
|
56475 | 90 |
def redirection_iterator: Iterator[Document_ID.Generic] = |
56746 | 91 |
for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) |
56475 | 92 |
yield id |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
93 |
|
56475 | 94 |
def redirect(other_id: Document_ID.Generic): Markups = |
56489 | 95 |
{ |
96 |
val rep1 = |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
97 |
(for { |
56746 | 98 |
(Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
99 |
if other_id == id |
56746 | 100 |
} yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap |
56489 | 101 |
if (rep1.isEmpty) Markups.empty else new Markups(rep1) |
102 |
} |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
103 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
104 |
override def hashCode: Int = rep.hashCode |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
105 |
override def equals(that: Any): Boolean = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
106 |
that match { |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
107 |
case other: Markups => rep == other.rep |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
108 |
case _ => false |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
109 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
110 |
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
|
111 |
} |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
112 |
|
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
113 |
|
50507 | 114 |
/* state */ |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
115 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
116 |
object State |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
117 |
{ |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
118 |
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
|
119 |
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
|
120 |
|
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
121 |
def merge_markup(states: List[State], index: Markup_Index, |
56743 | 122 |
range: Text.Range, elements: Markup.Elements): Markup_Tree = |
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
123 |
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
|
124 |
} |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
56295
diff
changeset
|
125 |
|
43714 | 126 |
sealed case class State( |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
127 |
command: Command, |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
128 |
status: List[Markup] = Nil, |
50507 | 129 |
results: Results = Results.empty, |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
130 |
markups: Markups = Markups.empty) |
38361 | 131 |
{ |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
132 |
lazy val protocol_status: Protocol.Status = |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
133 |
{ |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
134 |
val warnings = |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59072
diff
changeset
|
135 |
if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
136 |
List(Markup(Markup.WARNING, Nil)) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
137 |
else Nil |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
138 |
val errors = |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
139 |
if (results.iterator.exists(p => Protocol.is_error(p._2))) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
140 |
List(Markup(Markup.ERROR, Nil)) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
141 |
else Nil |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
142 |
Protocol.Status.make((warnings ::: errors ::: status).iterator) |
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
143 |
} |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
144 |
|
55650 | 145 |
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
|
146 |
|
56489 | 147 |
def redirect(other_command: Command): Option[State] = |
148 |
{ |
|
149 |
val markups1 = markups.redirect(other_command.id) |
|
150 |
if (markups1.is_empty) None |
|
151 |
else Some(new State(other_command, Nil, Results.empty, markups1)) |
|
152 |
} |
|
49614 | 153 |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
154 |
private def add_status(st: Markup): State = |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
155 |
copy(status = st :: status) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
156 |
|
56746 | 157 |
private def add_markup( |
158 |
status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = |
|
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
159 |
{ |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
160 |
val markups1 = |
56395
0546e036d1c0
more direct warning within persistent Protocol.Status;
wenzelm
parents:
56372
diff
changeset
|
161 |
if (status || Protocol.liberal_status_elements(m.info.name)) |
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
162 |
markups.add(Markup_Index(true, chunk_name), m) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
163 |
else markups |
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
164 |
copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
165 |
} |
38361 | 166 |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
167 |
def accumulate( |
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
168 |
self_id: Document_ID.Generic => Boolean, |
56746 | 169 |
other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
170 |
message: XML.Elem): State = |
38361 | 171 |
message match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
172 |
case XML.Elem(Markup(Markup.STATUS, _), msgs) => |
38714 | 173 |
(this /: msgs)((state, msg) => |
174 |
msg match { |
|
46152
793cecd4ffc0
accumulate status as regular markup for command range;
wenzelm
parents:
45709
diff
changeset
|
175 |
case elem @ XML.Elem(markup, Nil) => |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
176 |
state. |
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
177 |
add_status(markup). |
56746 | 178 |
add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem)) |
52536 | 179 |
case _ => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56746
diff
changeset
|
180 |
Output.warning("Ignored status message: " + msg) |
52536 | 181 |
state |
38714 | 182 |
}) |
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
|
183 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
184 |
case XML.Elem(Markup(Markup.REPORT, _), msgs) => |
38572
0fe2c01ef7da
Command.State: accumulate markup reports uniformly;
wenzelm
parents:
38564
diff
changeset
|
185 |
(this /: msgs)((state, msg) => |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
186 |
{ |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56746
diff
changeset
|
187 |
def bad(): Unit = Output.warning("Ignored report message: " + msg) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
188 |
|
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
189 |
msg match { |
57911
dcb758188aa6
clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents:
57910
diff
changeset
|
190 |
case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) => |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
191 |
|
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
192 |
val target = |
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
193 |
if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) |
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
194 |
Some((chunk_name, command.chunks(chunk_name))) |
56746 | 195 |
else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
196 |
else None |
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
197 |
|
57911
dcb758188aa6
clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents:
57910
diff
changeset
|
198 |
(target, atts) match { |
dcb758188aa6
clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents:
57910
diff
changeset
|
199 |
case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
200 |
target_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
|
201 |
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
|
202 |
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
|
203 |
val info = Text.Info(range, XML.Elem(Markup(name, props), args)) |
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
204 |
state.add_markup(false, target_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
|
205 |
case None => bad(); state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
206 |
} |
57911
dcb758188aa6
clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents:
57910
diff
changeset
|
207 |
case _ => |
56514
db929027e701
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
wenzelm
parents:
56489
diff
changeset
|
208 |
// silently ignore excessive reports |
56476 | 209 |
state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
210 |
} |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
211 |
|
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
212 |
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
|
213 |
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
|
214 |
val range = command.proper_range |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
215 |
val props = Position.purge(atts) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
216 |
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) |
56746 | 217 |
state.add_markup(false, Symbol.Text_Chunk.Default, info) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
218 |
|
56470
8eda56033203
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
wenzelm
parents:
56469
diff
changeset
|
219 |
case _ => bad(); state |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
220 |
} |
38361 | 221 |
}) |
52930
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
222 |
case XML.Elem(Markup(name, props), body) => |
5fab62ae3532
retain original messages properties, e.g. for retrieval via Command.Results;
wenzelm
parents:
52849
diff
changeset
|
223 |
props match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
224 |
case Markup.Serial(i) => |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset
|
225 |
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
|
226 |
val message2 = XML.Elem(Markup(name, props), body) |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50158
diff
changeset
|
227 |
|
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
228 |
var st = copy(results = results + (i -> message1)) |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
229 |
if (Protocol.is_inlined(message)) { |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
230 |
for { |
56469 | 231 |
(chunk_name, chunk) <- command.chunks.iterator |
59713 | 232 |
range <- Protocol_Message.positions( |
59735 | 233 |
self_id, command.span.position, chunk_name, chunk, message) |
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
234 |
} st = st.add_markup(false, chunk_name, Text.Info(range, message2)) |
55433
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
235 |
} |
d2960d67f163
clarified message_positions: cover alt_id as well;
wenzelm
parents:
55432
diff
changeset
|
236 |
st |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
237 |
|
52536 | 238 |
case _ => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56746
diff
changeset
|
239 |
Output.warning("Ignored message without serial number: " + message) |
52536 | 240 |
this |
38872 | 241 |
} |
56295
a40e67ce4f84
clarified valid_id: always standardize towards static command.id;
wenzelm
parents:
55884
diff
changeset
|
242 |
} |
38361 | 243 |
} |
38367 | 244 |
|
245 |
||
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
246 |
|
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
247 |
/** static content **/ |
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
248 |
|
45644 | 249 |
/* make commands */ |
250 |
||
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
251 |
def apply( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
252 |
id: Document_ID.Command, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
253 |
node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
254 |
blobs_info: Blobs_Info, |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
255 |
span: Command_Span.Span): Command = |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
256 |
{ |
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
257 |
val (source, span1) = span.compact_source |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
258 |
new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
259 |
} |
49414 | 260 |
|
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
261 |
val empty: Command = |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
262 |
Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
263 |
|
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
264 |
def unparsed( |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
265 |
id: Document_ID.Command, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
266 |
source: String, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
267 |
results: Results, |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
268 |
markup: Markup_Tree): Command = |
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
269 |
{ |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
270 |
val (source1, span1) = Command_Span.unparsed(source).compact_source |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
271 |
new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup) |
55648
38f264741609
tuned signature -- avoid obscure default arguments;
wenzelm
parents:
55622
diff
changeset
|
272 |
} |
49414 | 273 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
274 |
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
|
275 |
unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty) |
44384 | 276 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
277 |
def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = |
49414 | 278 |
{ |
49466 | 279 |
val text = XML.content(body) |
280 |
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
|
281 |
unparsed(id, text, results, markup) |
49414 | 282 |
} |
49359
c1262d7389fb
refined output panel: more value-oriented approach to update and caret focus;
wenzelm
parents:
49037
diff
changeset
|
283 |
|
44384 | 284 |
|
285 |
/* perspective */ |
|
286 |
||
44474 | 287 |
object Perspective |
288 |
{ |
|
289 |
val empty: Perspective = Perspective(Nil) |
|
290 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
291 |
|
44474 | 292 |
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
|
293 |
{ |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56782
diff
changeset
|
294 |
def is_empty: Boolean = commands.isEmpty |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56782
diff
changeset
|
295 |
|
44474 | 296 |
def same(that: Perspective): Boolean = |
297 |
{ |
|
298 |
val cmds1 = this.commands |
|
299 |
val cmds2 = that.commands |
|
48754
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
300 |
require(!cmds1.exists(_.is_undefined)) |
c2c1e5944536
clarified undefined, unparsed, unfinished command spans;
wenzelm
parents:
48745
diff
changeset
|
301 |
require(!cmds2.exists(_.is_undefined)) |
44474 | 302 |
cmds1.length == cmds2.length && |
303 |
(cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) |
|
304 |
} |
|
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset
|
305 |
} |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
306 |
|
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
307 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
308 |
/* blobs: inlined errors and auxiliary files */ |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
309 |
|
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
310 |
private def clean_tokens(tokens: List[Token]): List[(Token, Int)] = |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
311 |
{ |
61579 | 312 |
val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
313 |
def clean(toks: List[(Token, Int)]): List[(Token, Int)] = |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
314 |
toks match { |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
315 |
case (t1, i1) :: (t2, i2) :: rest => |
61579 | 316 |
if (t1.is_keyword && markers(t1.source)) clean(rest) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
317 |
else (t1, i1) :: clean((t2, i2) :: rest) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
318 |
case _ => toks |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
319 |
} |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
320 |
clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper })) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
321 |
} |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
322 |
|
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
323 |
private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] = |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
324 |
if (tokens.exists({ case (t, _) => t.is_command })) { |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
325 |
tokens.dropWhile({ case (t, _) => !t.is_command }). |
64471
c40c2975fb02
more uniform path syntax, as in ML (see 5a7c919a4ada);
wenzelm
parents:
63584
diff
changeset
|
326 |
collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
327 |
} |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
328 |
else None |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
329 |
|
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
62969
diff
changeset
|
330 |
def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) = |
59735 | 331 |
syntax.load_command(span.name) match { |
332 |
case Some(exts) => |
|
333 |
find_file(clean_tokens(span.content)) match { |
|
334 |
case Some((file, i)) => |
|
335 |
if (exts.isEmpty) (List(file), i) |
|
336 |
else (exts.map(ext => file + "." + ext), i) |
|
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
337 |
case None => (Nil, -1) |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
338 |
} |
59735 | 339 |
case None => (Nil, -1) |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
340 |
} |
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
341 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
342 |
def blobs_info( |
59699 | 343 |
resources: Resources, |
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
62969
diff
changeset
|
344 |
syntax: Outer_Syntax, |
59699 | 345 |
get_blob: Document.Node.Name => Option[Document.Blob], |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
346 |
can_import: Document.Node.Name => Boolean, |
59699 | 347 |
node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
348 |
span: Command_Span.Span): Blobs_Info = |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
349 |
{ |
59735 | 350 |
span.name match { |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
351 |
// inlined errors |
59735 | 352 |
case Thy_Header.THEORY => |
59705 | 353 |
val header = |
64823 | 354 |
resources.check_thy_reader( |
355 |
"", node_name, new CharSequenceReader(Token.implode(span.content))) |
|
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
356 |
val errors = |
59708
aed304412e43
more markup, which helps to create missing imports;
wenzelm
parents:
59706
diff
changeset
|
357 |
for ((imp, pos) <- header.imports if !can_import(imp)) yield { |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
358 |
val msg = |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
359 |
"Bad theory import " + |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
360 |
Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos) |
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
361 |
Exn.Exn(ERROR(msg)): Command.Blob |
59708
aed304412e43
more markup, which helps to create missing imports;
wenzelm
parents:
59706
diff
changeset
|
362 |
} |
59715
4f0d0e4ad68d
avoid duplicate header errors, more precise positions;
wenzelm
parents:
59713
diff
changeset
|
363 |
(errors, -1) |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
364 |
|
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
365 |
// auxiliary files |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
366 |
case _ => |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
367 |
val (files, index) = span_files(syntax, span) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
368 |
val blobs = |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
369 |
files.map(file => |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
370 |
(Exn.capture { |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
371 |
val name = |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
372 |
Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file))) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
373 |
val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
374 |
(name, blob) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
375 |
}).user_error) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
376 |
(blobs, index) |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
377 |
} |
59689
7968c57ea240
simplified Command.resolve_files in ML, using blobs_index from Scala;
wenzelm
parents:
59684
diff
changeset
|
378 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
379 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
380 |
|
38361 | 381 |
|
46712 | 382 |
final class Command private( |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
383 |
val id: Document_ID.Command, |
44615 | 384 |
val node_name: Document.Node.Name, |
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
385 |
val blobs_info: Command.Blobs_Info, |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
386 |
val span: Command_Span.Span, |
49414 | 387 |
val source: String, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
388 |
val init_results: Command.Results, |
49414 | 389 |
val init_markup: Markup_Tree) |
34451 | 390 |
{ |
57912 | 391 |
override def toString: String = id + "/" + span.kind.toString |
34495 | 392 |
|
57910 | 393 |
|
394 |
/* classification */ |
|
395 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
396 |
def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57904
diff
changeset
|
397 |
def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span |
57904 | 398 |
|
399 |
def is_undefined: Boolean = id == Document_ID.none |
|
400 |
val is_unparsed: Boolean = span.content.exists(_.is_unparsed) |
|
401 |
val is_unfinished: Boolean = span.content.exists(_.is_unfinished) |
|
402 |
||
34859 | 403 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
404 |
/* blobs */ |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
405 |
|
59702
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
406 |
def blobs: List[Command.Blob] = blobs_info._1 |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
407 |
def blobs_index: Int = blobs_info._2 |
58dfaa369c11
hybrid use of command blobs: inlined errors and auxiliary files;
wenzelm
parents:
59699
diff
changeset
|
408 |
|
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
409 |
def blobs_names: List[Document.Node.Name] = |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
410 |
for (Exn.Res((name, _)) <- blobs) yield name |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54524
diff
changeset
|
411 |
|
60916
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60215
diff
changeset
|
412 |
def blobs_undefined: List[Document.Node.Name] = |
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60215
diff
changeset
|
413 |
for (Exn.Res((name, None)) <- blobs) yield name |
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60215
diff
changeset
|
414 |
|
57842
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
415 |
def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = |
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
416 |
for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest) |
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
417 |
|
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
418 |
def blobs_changed(doc_blobs: Document.Blobs): Boolean = |
8e4ae2db1849
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
wenzelm
parents:
57615
diff
changeset
|
419 |
blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false }) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54517
diff
changeset
|
420 |
|
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
421 |
|
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56395
diff
changeset
|
422 |
/* source chunks */ |
55431
e0f20a44ff9d
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
wenzelm
parents:
55430
diff
changeset
|
423 |
|
56746 | 424 |
val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) |
56473 | 425 |
|
56746 | 426 |
val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = |
427 |
((Symbol.Text_Chunk.Default -> chunk) :: |
|
56473 | 428 |
(for (Exn.Res((name, Some((_, file)))) <- blobs) |
60215 | 429 |
yield Symbol.Text_Chunk.File(name.node) -> file)).toMap |
56473 | 430 |
|
46813 | 431 |
def length: Int = source.length |
56473 | 432 |
def range: Text.Range = chunk.range |
46813 | 433 |
|
434 |
val proper_range: Text.Range = |
|
57901
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
435 |
Text.Range(0, |
e1abca2527da
more explicit type Span in Scala, according to ML version;
wenzelm
parents:
57842
diff
changeset
|
436 |
(length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) |
46813 | 437 |
|
38426 | 438 |
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
|
439 |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
440 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
441 |
/* accumulated results */ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
442 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
443 |
val init_state: Command.State = |
55649
1532ab0dc67b
more general / abstract Command.Markups, with separate index for status elements;
wenzelm
parents:
55648
diff
changeset
|
444 |
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
|
445 |
|
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52524
diff
changeset
|
446 |
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
|
447 |
} |