equal
deleted
inserted
replaced
89 |
89 |
90 def check_thy(name: Document.Node.Name): Document.Node.Header = |
90 def check_thy(name: Document.Node.Name): Document.Node.Header = |
91 with_thy_text(name, check_thy_text(name, _)) |
91 with_thy_text(name, check_thy_text(name, _)) |
92 |
92 |
93 |
93 |
94 /* theory text edits */ |
94 /* document changes */ |
95 |
95 |
96 def parse_edits( |
96 def parse_change( |
97 reparse_limit: Int, |
97 reparse_limit: Int, |
98 previous: Document.Version, |
98 previous: Document.Version, |
99 doc_blobs: Document.Blobs, |
99 doc_blobs: Document.Blobs, |
100 edits: List[Document.Edit_Text]): Session.Change = |
100 edits: List[Document.Edit_Text]): Session.Change = |
101 Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits) |
101 Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) |
102 |
102 |
103 def syntax_changed() { } |
103 def commit(change: Session.Change) { } |
104 } |
104 } |
105 |
105 |