# HG changeset patch
# User wenzelm
# Date 1513939189 -3600
# Node ID 573077aa2826d9e1e2a213488aec1543e8889e40
# Parent  6c837185aa61d0bf8ce75fd6282009928a5d0310
tuned signature;

diff -r 6c837185aa61 -r 573077aa2826 src/Pure/PIDE/document.scala
--- 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
diff -r 6c837185aa61 -r 573077aa2826 src/Pure/Thy/present.scala
--- 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)))
     }
diff -r 6c837185aa61 -r 573077aa2826 src/Pure/Tools/bibtex.scala
--- 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")
     }
   }