diff -r 20304512a33b -r c137a9f038a6 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Jun 17 20:24:22 2017 +0200 +++ b/src/Pure/PIDE/document.scala Mon Jun 19 17:28:48 2017 +0200 @@ -498,6 +498,8 @@ def is_theory: Boolean = node_name.is_theory override def toString: String = node_name.toString + def try_get_text(range: Text.Range): Option[String] + def node_required: Boolean def get_blob: Option[Blob]