clarified signature: persistent Node.source / Snapshot.source;

--- a/src/Pure/PIDE/document.scala	Thu Sep 22 16:29:26 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Sep 22 17:24:50 2022 +0200
@@ -333,7 +333,7 @@
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
 
-    def source: String =
+    lazy val source: String =
       get_blob match {
         case Some(blob) => blob.source
         case None => command_iterator().map({ case (cmd, _) => cmd.source }).mkString
@@ -530,6 +530,15 @@
       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
+      }
+
+
     /* edits */
 
     def is_outdated: Boolean = edits.nonEmpty
@@ -1152,8 +1161,7 @@
         } yield tree).toList
       }
       else {
-        val node_source = node.source
-        Text.Range(0, node_source.length).try_restrict(range) match {
+        Text.Range(0, node.source.length).try_restrict(range) match {
           case None => Nil
           case Some(node_range) =>
             val markup =
@@ -1164,7 +1172,7 @@
                   val markup_index = Command.Markup_Index(false, chunk_name)
                   command_markup(version, command, markup_index, node_range, elements)
               }
-            markup.to_XML(node_range, node_source, elements)
+            markup.to_XML(node_range, node.source, elements)
         }
       }
     }

--- a/src/Pure/Thy/bibtex.scala	Thu Sep 22 16:29:26 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala	Thu Sep 22 17:24:50 2022 +0200
@@ -32,7 +32,7 @@
         val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
-            File.write(bib, snapshot.node.source)
+            File.write(bib, snapshot.source)
             Bibtex.html_output(List(bib), style = "unsort", title = title)
           }
         Some(Browser_Info.HTML_Document(title, content))

--- a/src/Pure/Thy/browser_info.scala	Thu Sep 22 16:29:26 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Thu Sep 22 17:24:50 2022 +0200
@@ -265,7 +265,7 @@
       val name = snapshot.node_name
       if (plain_text) {
         val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
-        val body = HTML.text(snapshot.node.source)
+        val body = HTML.text(snapshot.source)
         html_document(title, body, fonts_css)
       }
       else {