--- a/src/Pure/PIDE/resources.scala Sat Mar 29 09:34:51 2014 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Mar 29 10:17:09 2014 +0100
@@ -93,12 +93,12 @@
/* theory text edits */
- def text_edits(
- reparse_limit: Int,
- previous: Document.Version,
- doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
- Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+ def parse_edits(
+ 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)
def syntax_changed() { }
}