src/Pure/PIDE/resources.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56387 d92eb5c3960d
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -91,15 +91,15 @@
     1.4      with_thy_text(name, check_thy_text(name, _))
     1.5  
     1.6  
     1.7 -  /* theory text edits */
     1.8 +  /* document changes */
     1.9  
    1.10 -  def parse_edits(
    1.11 +  def parse_change(
    1.12        reparse_limit: Int,
    1.13        previous: Document.Version,
    1.14        doc_blobs: Document.Blobs,
    1.15        edits: List[Document.Edit_Text]): Session.Change =
    1.16 -    Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
    1.17 +    Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
    1.18  
    1.19 -  def syntax_changed() { }
    1.20 +  def commit(change: Session.Change) { }
    1.21  }
    1.22