equal
deleted
inserted
replaced
98 |
98 |
99 |
99 |
100 /* theory text edits */ |
100 /* theory text edits */ |
101 |
101 |
102 def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text]) |
102 def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text]) |
103 : (List[Document.Edit_Command], Document.Version) = |
103 : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) = |
104 Thy_Syntax.text_edits(this, reparse_limit, previous, edits) |
104 Thy_Syntax.text_edits(this, reparse_limit, previous, edits) |
105 } |
105 } |
106 |
106 |