| changeset 66114 | c137a9f038a6 |
| parent 66043 | f704c063e95d |
| child 66150 | c2e19b9e1398 |
--- 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]