--- 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)
}
//}}}