tuned signature;
authorwenzelm
Thu, 05 Jan 2023 22:16:13 +0100
changeset 76924 fc24cf493202
parent 76923 8a66a88cd5dc
child 76925 47f1b099497c
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/Tools/update.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 =
--- 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 =