diff -r c20053f67093 -r b1cf8ddc2e04 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Mar 29 10:17:09 2014 +0100 +++ b/src/Pure/PIDE/session.scala Sat Mar 29 10:49:32 2014 +0100 @@ -24,6 +24,7 @@ previous: Document.Version, doc_blobs: Document.Blobs, syntax_changed: Boolean, + deps_changed: Boolean, doc_edits: List[Document.Edit_Command], version: Document.Version) @@ -190,8 +191,8 @@ case Text_Edits(previous, doc_blobs, text_edits, version_result) => val prev = previous.get_finished val change = - Timing.timeit("parse_edits", timing) { - resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits) + Timing.timeit("parse_change", timing) { + resources.parse_change(reparse_limit, prev, doc_blobs, text_edits) } version_result.fulfill(change.version) sender ! change @@ -402,8 +403,7 @@ val assignment = global_state().the_assignment(change.previous).check_finished global_state >> (_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits) - - if (change.syntax_changed) resources.syntax_changed() + resources.commit(change) } //}}}