# HG changeset patch
# User wenzelm
# Date 1673019831 -3600
# Node ID dd53bb198eb1e89950dd89eae4db9b588cbe3924
# Parent  f88c239d1a838959d29bd235549b3b3fa3b4de4f
tuned signature: more uniform operations;

diff -r f88c239d1a83 -r dd53bb198eb1 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Jan 06 15:35:48 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Jan 06 16:43:51 2023 +0100
@@ -580,15 +580,6 @@
       node_name :: node.load_commands.flatMap(_.blobs_names)
 
 
-    /* source text */
-
-    def source: String =
-      snippet_command match {
-        case Some(command) => command.source
-        case None => node.source
-      }
-
-
     /* pending edits */
 
     def is_outdated: Boolean = !pending_edits.is_stable
diff -r f88c239d1a83 -r dd53bb198eb1 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Jan 06 15:35:48 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 06 16:43:51 2023 +0100
@@ -35,7 +35,7 @@
         val title = "Bibliography " + quote(snapshot.node_name.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
-            File.write(bib, snapshot.source)
+            File.write(bib, snapshot.node.source)
             Bibtex.html_output(List(bib), style = "unsort", title = title)
           }
         Some(Browser_Info.HTML_Document(title, content))
diff -r f88c239d1a83 -r dd53bb198eb1 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Jan 06 15:35:48 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala	Fri Jan 06 16:43:51 2023 +0100
@@ -265,7 +265,7 @@
       val name = snapshot.node_name
       if (plain_text) {
         val title = "File " + Symbol.cartouche_decoded(name.file_name)
-        val body = HTML.text(snapshot.source)
+        val body = HTML.text(snapshot.node.source)
         html_document(title, body, fonts_css)
       }
       else {
diff -r f88c239d1a83 -r dd53bb198eb1 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jan 06 15:35:48 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 06 16:43:51 2023 +0100
@@ -135,7 +135,7 @@
                     rendering.text_messages(Text.Range.full)
                       .filter(message => verbose || Protocol.is_exported(message.info))
                   if (messages.nonEmpty) {
-                    val line_document = Line.Document(snapshot.source)
+                    val line_document = Line.Document(snapshot.node.source)
                     val buffer = new mutable.ListBuffer[String]
                     for (Text.Info(range, elem) <- messages) {
                       val line = line_document.position(range.start).line1