equal
deleted
inserted
replaced
500 |
500 |
501 def try_get_text(range: Text.Range): Option[String] |
501 def try_get_text(range: Text.Range): Option[String] |
502 |
502 |
503 def node_required: Boolean |
503 def node_required: Boolean |
504 def get_blob: Option[Blob] |
504 def get_blob: Option[Blob] |
|
505 def bibtex_entries: List[Text.Info[String]] |
505 |
506 |
506 def node_edits( |
507 def node_edits( |
507 node_header: Node.Header, |
508 node_header: Node.Header, |
508 text_edits: List[Text.Edit], |
509 text_edits: List[Text.Edit], |
509 perspective: Node.Perspective_Text): List[Edit_Text] = |
510 perspective: Node.Perspective_Text): List[Edit_Text] = |