# HG changeset patch # User wenzelm # Date 1672953373 -3600 # Node ID fc24cf493202cdd4a44454797025c23b2ea4da4c # Parent 8a66a88cd5dced991a83cd725e50d3deaf8105d6 tuned signature; diff -r 8a66a88cd5dc -r fc24cf493202 src/Pure/PIDE/document.scala --- 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 = diff -r 8a66a88cd5dc -r fc24cf493202 src/Pure/Tools/update.scala --- 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 =