src/Pure/PIDE/session.scala
changeset 56316 b1cf8ddc2e04
parent 56315 c20053f67093
child 56335 8953d4cc060a
     1.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 29 10:17:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 29 10:49:32 2014 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4      previous: Document.Version,
     1.5      doc_blobs: Document.Blobs,
     1.6      syntax_changed: Boolean,
     1.7 +    deps_changed: Boolean,
     1.8      doc_edits: List[Document.Edit_Command],
     1.9      version: Document.Version)
    1.10  
    1.11 @@ -190,8 +191,8 @@
    1.12          case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    1.13            val prev = previous.get_finished
    1.14            val change =
    1.15 -            Timing.timeit("parse_edits", timing) {
    1.16 -              resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits)
    1.17 +            Timing.timeit("parse_change", timing) {
    1.18 +              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    1.19              }
    1.20            version_result.fulfill(change.version)
    1.21            sender ! change
    1.22 @@ -402,8 +403,7 @@
    1.23        val assignment = global_state().the_assignment(change.previous).check_finished
    1.24        global_state >> (_.define_version(change.version, assignment))
    1.25        prover.get.update(change.previous.id, change.version.id, change.doc_edits)
    1.26 -
    1.27 -      if (change.syntax_changed) resources.syntax_changed()
    1.28 +      resources.commit(change)
    1.29      }
    1.30      //}}}
    1.31