src/Pure/PIDE/session.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56335 8953d4cc060a
--- 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)
     }
     //}}}