diff -r c20053f67093 -r b1cf8ddc2e04 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Mar 29 10:49:32 2014 +0100 @@ -91,15 +91,15 @@ with_thy_text(name, check_thy_text(name, _)) - /* theory text edits */ + /* document changes */ - def parse_edits( + def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Session.Change = - Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits) + Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) - def syntax_changed() { } + def commit(change: Session.Change) { } }