--- 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
--- 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))
--- 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 {
--- 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