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(