src/Pure/System/session.scala
changeset 54521 744ea0025e11
parent 54519 5fed81762406
child 54559 39d91cac6e91
     1.1 --- a/src/Pure/System/session.scala	Tue Nov 19 19:43:26 2013 +0100
     1.2 +++ b/src/Pure/System/session.scala	Tue Nov 19 20:53:43 2013 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4    case class Statistics(props: Properties.T)
     1.5    case class Global_Options(options: Options)
     1.6    case object Caret_Focus
     1.7 -  case class Raw_Edits(edits: List[Document.Edit_Text])
     1.8 +  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     1.9    case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
    1.10    case class Commands_Changed(
    1.11      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    1.12 @@ -167,6 +167,7 @@
    1.13    //{{{
    1.14    private case class Text_Edits(
    1.15      previous: Future[Document.Version],
    1.16 +    doc_blobs: Document.Blobs,
    1.17      text_edits: List[Document.Edit_Text],
    1.18      version_result: Promise[Document.Version])
    1.19  
    1.20 @@ -177,14 +178,14 @@
    1.21        receive {
    1.22          case Stop => finished = true; reply(())
    1.23  
    1.24 -        case Text_Edits(previous, text_edits, version_result) =>
    1.25 +        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    1.26            val prev = previous.get_finished
    1.27 -          val (all_blobs, doc_edits, version) =
    1.28 +          val (doc_edits, version) =
    1.29              Timing.timeit("Thy_Load.text_edits", timing) {
    1.30 -              thy_load.text_edits(reparse_limit, prev, text_edits)
    1.31 +              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
    1.32              }
    1.33            version_result.fulfill(version)
    1.34 -          sender ! Change(all_blobs, doc_edits, prev, version)
    1.35 +          sender ! Change(doc_blobs, doc_edits, prev, version)
    1.36  
    1.37          case bad => System.err.println("change_parser: ignoring bad message " + bad)
    1.38        }
    1.39 @@ -250,7 +251,7 @@
    1.40    private case class Start(args: List[String])
    1.41    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    1.42    private case class Change(
    1.43 -    all_blobs: Map[Document.Node.Name, Bytes],
    1.44 +    doc_blobs: Document.Blobs,
    1.45      doc_edits: List[Document.Edit_Command],
    1.46      previous: Document.Version,
    1.47      version: Document.Version)
    1.48 @@ -349,7 +350,7 @@
    1.49  
    1.50      /* raw edits */
    1.51  
    1.52 -    def handle_raw_edits(edits: List[Document.Edit_Text])
    1.53 +    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    1.54      //{{{
    1.55      {
    1.56        prover.get.discontinue_execution()
    1.57 @@ -358,8 +359,8 @@
    1.58        val version = Future.promise[Document.Version]
    1.59        val change = global_state >>> (_.continue_history(previous, edits, version))
    1.60  
    1.61 -      raw_edits.event(Session.Raw_Edits(edits))
    1.62 -      change_parser ! Text_Edits(previous, edits, version)
    1.63 +      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
    1.64 +      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
    1.65      }
    1.66      //}}}
    1.67  
    1.68 @@ -379,7 +380,7 @@
    1.69            digest <- command.blobs_digests
    1.70            if !global_state().defined_blob(digest)
    1.71          } {
    1.72 -          change.all_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    1.73 +          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    1.74              case Some(blob) =>
    1.75                global_state >> (_.define_blob(digest))
    1.76                prover.get.define_blob(blob)
    1.77 @@ -523,7 +524,7 @@
    1.78          case Update_Options(options) if prover.isDefined =>
    1.79            if (is_ready) {
    1.80              prover.get.options(options)
    1.81 -            handle_raw_edits(Nil)
    1.82 +            handle_raw_edits(Map.empty, Nil)
    1.83            }
    1.84            global_options.event(Session.Global_Options(options))
    1.85            reply(())
    1.86 @@ -531,8 +532,8 @@
    1.87          case Cancel_Exec(exec_id) if prover.isDefined =>
    1.88            prover.get.cancel_exec(exec_id)
    1.89  
    1.90 -        case Session.Raw_Edits(edits) if prover.isDefined =>
    1.91 -          handle_raw_edits(edits)
    1.92 +        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
    1.93 +          handle_raw_edits(doc_blobs, edits)
    1.94            reply(())
    1.95  
    1.96          case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
    1.97 @@ -585,8 +586,8 @@
    1.98  
    1.99    def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
   1.100  
   1.101 -  def update(edits: List[Document.Edit_Text])
   1.102 -  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
   1.103 +  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   1.104 +  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
   1.105  
   1.106    def update_options(options: Options)
   1.107    { session_actor !? Update_Options(options) }