# HG changeset patch
# User wenzelm
# Date 1513892308 -3600
# Node ID 3a965131801526263ef7ad3424149f7176766d42
# Parent  4cedf44f2af168266646d436d5dca21ef0898213
clarified signature;

diff -r 4cedf44f2af1 -r 3a9651318015 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Dec 21 22:07:30 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Dec 21 22:38:28 2017 +0100
@@ -119,6 +119,8 @@
 
       def path: Path = Path.explode(File.standard_path(node))
 
+      def is_bibtex: Boolean = Bibtex.check_name(node)
+
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
@@ -320,6 +322,12 @@
 
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
+
+    def get_text: String =
+      get_blob match {
+        case Some(blob) => blob.bytes.text
+        case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
+      }
   }
 
 
@@ -528,6 +536,7 @@
 
     def node_required: Boolean
     def get_blob: Option[Blob]
+    def is_bibtex: Boolean = node_name.is_bibtex
     def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
diff -r 4cedf44f2af1 -r 3a9651318015 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Dec 21 22:07:30 2017 +0100
+++ b/src/Pure/Thy/present.scala	Thu Dec 21 22:38:28 2017 +0100
@@ -134,14 +134,10 @@
   /* text document */
 
   def text_document(snapshot: Document.Snapshot): XML.Body =
-  {
-    val text =
-      snapshot.node.get_blob match {
-        case Some(blob) => blob.bytes.text
-        case None => ""
-      }
-    if (text.isEmpty) Nil else List(XML.Text(Symbol.decode(text)))
-  }
+    snapshot.node.get_text match {
+      case "" => Nil
+      case txt => List(XML.Text(Symbol.decode(txt)))
+    }
 
 
 
diff -r 4cedf44f2af1 -r 3a9651318015 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:07:30 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:38:28 2017 +0100
@@ -436,8 +436,6 @@
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
 
-  def is_bibtex: Boolean = Bibtex.check_name(node_name)
-
   def bibtex_entries: List[Text.Info[String]] =
     if (is_bibtex) content.bibtex_entries else Nil