--- a/src/Pure/PIDE/document.scala Thu Dec 21 22:56:51 2017 +0100
+++ b/src/Pure/PIDE/document.scala Fri Dec 22 11:39:49 2017 +0100
@@ -323,7 +323,7 @@
def command_start(cmd: Command): Option[Text.Offset] =
Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
- def get_text: String =
+ def source: String =
get_blob match {
case Some(blob) => blob.bytes.text
case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
--- a/src/Pure/Thy/present.scala Thu Dec 21 22:56:51 2017 +0100
+++ b/src/Pure/Thy/present.scala Fri Dec 22 11:39:49 2017 +0100
@@ -134,7 +134,7 @@
/* text document */
def text_document(snapshot: Document.Snapshot): XML.Body =
- snapshot.node.get_text match {
+ snapshot.node.source match {
case "" => Nil
case txt => List(XML.Text(Symbol.decode(txt)))
}
--- a/src/Pure/Tools/bibtex.scala Thu Dec 21 22:56:51 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala Fri Dec 22 11:39:49 2017 +0100
@@ -567,7 +567,7 @@
def present(snapshot: Document.Snapshot): String =
{
Isabelle_System.with_tmp_file("bib", "bib") { bib =>
- File.write(bib, snapshot.node.get_text)
+ File.write(bib, snapshot.node.source)
html_output(List(bib), style = "unsort")
}
}