src/Pure/System/session.scala

 
   //{{{
   case class Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
-  case class Raw_Edits(edits: List[Document.Edit_Text])
+  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase

   /** pipelined change parsing **/
 
   //{{{
   private case class Text_Edits(
     previous: Future[Document.Version],
+    doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
     version_result: Promise[Document.Version])
 
   private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
   {
     var finished = false
     while (!finished) {
       receive {
         case Stop => finished = true; reply(())
 
-        case Text_Edits(previous, text_edits, version_result) =>
+        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
-          val (all_blobs, doc_edits, version) =
+          val (doc_edits, version) =
             Timing.timeit("Thy_Load.text_edits", timing) {
-              thy_load.text_edits(reparse_limit, prev, text_edits)
+              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(version)
-          sender ! Change(all_blobs, doc_edits, prev, version)
+          sender ! Change(doc_blobs, doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
     }
   }

   /* actor messages */
 
   private case class Start(args: List[String])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
-    all_blobs: Map[Document.Node.Name, Bytes],
+    doc_blobs: Document.Blobs,
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Messages(msgs: List[Isabelle_Process.Message])

     }
 
 
     /* raw edits */
 
-    def handle_raw_edits(edits: List[Document.Edit_Text])
+    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     //{{{
     {
       prover.get.discontinue_execution()
 
       val previous = global_state().history.tip.version
       val version = Future.promise[Document.Version]
       val change = global_state >>> (_.continue_history(previous, edits, version))
 
-      raw_edits.event(Session.Raw_Edits(edits))
-      change_parser ! Text_Edits(previous, edits, version)
+      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
+      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
     }
     //}}}
 
 
     /* resulting changes */

       {
         for {
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          change.all_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)
             case None => System.err.println("Missing blob for SHA1 digest " + digest)
           }

           reply(())
 
         case Update_Options(options) if prover.isDefined =>
           if (is_ready) {
             prover.get.options(options)
-            handle_raw_edits(Nil)
+            handle_raw_edits(Map.empty, Nil)
           }
           global_options.event(Session.Global_Options(options))
           reply(())
 
         case Cancel_Exec(exec_id) if prover.isDefined =>
           prover.get.cancel_exec(exec_id)
 
-        case Session.Raw_Edits(edits) if prover.isDefined =>
-          handle_raw_edits(edits)
+        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
+          handle_raw_edits(doc_blobs, edits)
           reply(())
 
         case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
           prover.get.dialog_result(serial, result)
           handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))

   def protocol_command(name: String, args: String*)
   { session_actor ! Protocol_Command(name, args.toList) }
 
   def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
 
-  def update(edits: List[Document.Edit_Text])
-  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
+  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
 
   def update_options(options: Options)
   { session_actor !? Update_Options(options) }
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)