tuned signature;
authorwenzelm
Fri, 22 Dec 2017 11:39:49 +0100
changeset 67251 573077aa2826
parent 67250 6c837185aa61
child 67252 c7f859868b7c
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/Thy/present.scala
src/Pure/Tools/bibtex.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
--- 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")
     }
   }