src/Pure/PIDE/resources.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56387 d92eb5c3960d
--- 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) { }
 }