src/Pure/System/session.scala
changeset 55134 1b67b17cdad5
parent 54559 39d91cac6e91
child 55316 885500f4aa6a
     1.1 --- a/src/Pure/System/session.scala	Sat Jan 25 13:55:09 2014 +0100
     1.2 +++ b/src/Pure/System/session.scala	Sat Jan 25 15:29:40 2014 +0100
     1.3 @@ -180,12 +180,12 @@
     1.4  
     1.5          case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
     1.6            val prev = previous.get_finished
     1.7 -          val (doc_edits, version) =
     1.8 +          val (syntax_changed, doc_edits, version) =
     1.9              Timing.timeit("Thy_Load.text_edits", timing) {
    1.10                thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
    1.11              }
    1.12            version_result.fulfill(version)
    1.13 -          sender ! Change(doc_blobs, doc_edits, prev, version)
    1.14 +          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
    1.15  
    1.16          case bad => System.err.println("change_parser: ignoring bad message " + bad)
    1.17        }
    1.18 @@ -252,6 +252,7 @@
    1.19    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    1.20    private case class Change(
    1.21      doc_blobs: Document.Blobs,
    1.22 +    syntax_changed: Boolean,
    1.23      doc_edits: List[Document.Edit_Command],
    1.24      previous: Document.Version,
    1.25      version: Document.Version)
    1.26 @@ -370,9 +371,7 @@
    1.27      def handle_change(change: Change)
    1.28      //{{{
    1.29      {
    1.30 -      val previous = change.previous
    1.31 -      val version = change.version
    1.32 -      val doc_edits = change.doc_edits
    1.33 +      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
    1.34  
    1.35        def id_command(command: Command)
    1.36        {
    1.37 @@ -380,7 +379,7 @@
    1.38            digest <- command.blobs_digests
    1.39            if !global_state().defined_blob(digest)
    1.40          } {
    1.41 -          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    1.42 +          doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    1.43              case Some(blob) =>
    1.44                global_state >> (_.define_blob(digest))
    1.45                prover.get.define_blob(blob)
    1.46 @@ -401,6 +400,8 @@
    1.47        val assignment = global_state().the_assignment(previous).check_finished
    1.48        global_state >> (_.define_version(version, assignment))
    1.49        prover.get.update(previous.id, version.id, doc_edits)
    1.50 +
    1.51 +      if (syntax_changed) thy_load.syntax_changed()
    1.52      }
    1.53      //}}}
    1.54