--- a/src/Pure/PIDE/document.scala Thu Jan 05 21:33:49 2023 +0100
+++ b/src/Pure/PIDE/document.scala Thu Jan 05 22:16:13 2023 +0100
@@ -48,7 +48,7 @@
chunk: Symbol.Text_Chunk,
changed: Boolean
) {
- def is_wellformed_text: Boolean = bytes.wellformed_text.nonEmpty
+ def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
def unchanged: Item = copy(changed = false)
}
@@ -343,9 +343,9 @@
def command_start(cmd: Command): Option[Text.Offset] =
Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
- lazy val is_wellformed_text: Boolean =
+ lazy val source_wellformed: Boolean =
get_blob match {
- case Some(blob) => blob.is_wellformed_text
+ case Some(blob) => blob.source_wellformed
case None => true
}
@@ -659,7 +659,7 @@
for {
Exn.Res(blob) <- command.blobs
blob_node = get_node(blob.name)
- if blob_node.is_wellformed_text
+ if blob_node.source_wellformed
}
yield {
val text = blob_node.source
@@ -1218,7 +1218,7 @@
tree <- markup.to_XML(command_range, command.source, elements).iterator
} yield tree).toList
}
- else if (node.is_wellformed_text) {
+ else if (node.source_wellformed) {
Text.Range.length(node.source).try_restrict(range) match {
case Some(node_range) =>
val markup =
--- a/src/Pure/Tools/update.scala Thu Jan 05 21:33:49 2023 +0100
+++ b/src/Pure/Tools/update.scala Thu Jan 05 22:16:13 2023 +0100
@@ -85,7 +85,7 @@
theory_snapshot <- Build_Job.read_theory(theory_context)
node_name <- theory_snapshot.node_files
snapshot = theory_snapshot.switch(node_name)
- if snapshot.node.is_wellformed_text
+ if snapshot.node.source_wellformed
} {
progress.expose_interrupt()
val source1 =