src/Pure/PIDE/document.scala
changeset 67309 0e322d7325c3
parent 67293 2fe338d91d47
child 67825 f9c071cc958b
equal deleted inserted replaced
67308:760bbf416f1d 67309:0e322d7325c3
   536     def get_text(range: Text.Range): Option[String]
   536     def get_text(range: Text.Range): Option[String]
   537 
   537 
   538     def node_required: Boolean
   538     def node_required: Boolean
   539     def get_blob: Option[Blob]
   539     def get_blob: Option[Blob]
   540     def is_bibtex: Boolean = node_name.is_bibtex
   540     def is_bibtex: Boolean = node_name.is_bibtex
       
   541     def is_bibtex_theory: Boolean = node_name.is_bibtex_theory
   541     def bibtex_entries: List[Text.Info[String]]
   542     def bibtex_entries: List[Text.Info[String]]
   542 
   543 
   543     def node_edits(
   544     def node_edits(
   544       node_header: Node.Header,
   545       node_header: Node.Header,
   545       text_edits: List[Text.Edit],
   546       text_edits: List[Text.Edit],