src/Pure/PIDE/resources.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56387 d92eb5c3960d
equal deleted inserted replaced
56315:c20053f67093 56316:b1cf8ddc2e04
    89 
    89 
    90   def check_thy(name: Document.Node.Name): Document.Node.Header =
    90   def check_thy(name: Document.Node.Name): Document.Node.Header =
    91     with_thy_text(name, check_thy_text(name, _))
    91     with_thy_text(name, check_thy_text(name, _))
    92 
    92 
    93 
    93 
    94   /* theory text edits */
    94   /* document changes */
    95 
    95 
    96   def parse_edits(
    96   def parse_change(
    97       reparse_limit: Int,
    97       reparse_limit: Int,
    98       previous: Document.Version,
    98       previous: Document.Version,
    99       doc_blobs: Document.Blobs,
    99       doc_blobs: Document.Blobs,
   100       edits: List[Document.Edit_Text]): Session.Change =
   100       edits: List[Document.Edit_Text]): Session.Change =
   101     Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
   101     Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
   102 
   102 
   103   def syntax_changed() { }
   103   def commit(change: Session.Change) { }
   104 }
   104 }
   105 
   105