equal
deleted
inserted
replaced
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 /* theory text edits */ |
95 |
95 |
96 def text_edits( |
96 def parse_edits( |
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]): (Boolean, List[Document.Edit_Command], Document.Version) = |
100 edits: List[Document.Edit_Text]): Session.Change = |
101 Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits) |
101 Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits) |
102 |
102 |
103 def syntax_changed() { } |
103 def syntax_changed() { } |
104 } |
104 } |
105 |
105 |