src/Pure/PIDE/document.scala
changeset 67014 e6a695d6a6b2
parent 66849 42311fd08899
child 67110 3156faac30a7
equal deleted inserted replaced
67013:335a7dce7cb3 67014:e6a695d6a6b2
   506 
   506 
   507     def node_name: Node.Name
   507     def node_name: Node.Name
   508     def is_theory: Boolean = node_name.is_theory
   508     def is_theory: Boolean = node_name.is_theory
   509     override def toString: String = node_name.toString
   509     override def toString: String = node_name.toString
   510 
   510 
   511     def try_get_text(range: Text.Range): Option[String]
   511     def get_text(range: Text.Range): Option[String]
   512 
   512 
   513     def node_required: Boolean
   513     def node_required: Boolean
   514     def get_blob: Option[Blob]
   514     def get_blob: Option[Blob]
   515     def bibtex_entries: List[Text.Info[String]]
   515     def bibtex_entries: List[Text.Info[String]]
   516 
   516