# HG changeset patch
# User wenzelm
# Date 1393506424 -3600
# Node ID da0513d951556ae4aebc2b9fc10beda47c6bf47c
# Parent  47ed6a67a304c0580109614a2419d4ed235c6094
more formal Document.Blobs;
removed junk;

diff -r 47ed6a67a304 -r da0513d95155 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -43,14 +43,39 @@
   }
 
 
-  /* individual nodes */
+  /* document blobs: auxiliary files */
+
+  sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+
+  object Blobs
+  {
+    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
+    val empty: Blobs = apply(Map.empty)
+  }
+
+  final class Blobs private(blobs: Map[Node.Name, Blob])
+  {
+    override def toString: String = blobs.mkString("Blobs(", ",", ")")
+
+    def get(name: Node.Name): Option[Blob] = blobs.get(name)
+
+    def changed(name: Node.Name): Boolean =
+      get(name) match {
+        case Some(blob) => blob.changed
+        case None => false
+      }
+
+    def retrieve(digest: SHA1.Digest): Option[Blob] =
+      blobs.collectFirst({ case (_, blob) if blob.bytes.sha1_digest == digest => blob })
+  }
+
+
+  /* document nodes: theories and auxiliary files */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
-  type Blobs = Map[Node.Name, (Bytes, Command.File)]
-
   object Node
   {
     val empty: Node = new Node()
diff -r 47ed6a67a304 -r da0513d95155 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -315,8 +315,9 @@
 {
   /* inlined files */
 
-  def define_blob(blob: Bytes): Unit =
-    protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
+  def define_blob(blob: Document.Blob): Unit =
+    protocol_command_raw(
+      "Document.define_blob", Bytes(blob.bytes.sha1_digest.toString), blob.bytes)
 
 
   /* commands */
diff -r 47ed6a67a304 -r da0513d95155 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/System/session.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -378,11 +378,12 @@
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          doc_blobs.collectFirst({ case (_, (b, _)) if b.sha1_digest == digest => b }) match {
+          doc_blobs.retrieve(digest) 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)
+            case None =>
+              System.err.println("Missing blob for SHA1 digest " + digest)
           }
         }
 
@@ -524,7 +525,7 @@
         case Update_Options(options) if prover.isDefined =>
           if (is_ready) {
             prover.get.options(options)
-            handle_raw_edits(Map.empty, Nil)
+            handle_raw_edits(Document.Blobs.empty, Nil)
           }
           global_options.event(Session.Global_Options(options))
           reply(())
diff -r 47ed6a67a304 -r da0513d95155 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -268,14 +268,9 @@
       Exn.capture {
         val name =
           Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
-        val blob =
-          doc_blobs.get(name) match {
-            case Some((bytes, file)) => Some((bytes.sha1_digest, file))
-            case None => None
-          }
+        val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
         (name, blob)
-      }
-    )
+      })
   }
 
 
diff -r 47ed6a67a304 -r da0513d95155 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -99,8 +99,7 @@
   val empty_perspective: Document.Node.Perspective_Text =
     Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
 
-  def node_perspective(changed_blobs: Set[Document.Node.Name])
-    : (Boolean, Document.Node.Perspective_Text) =
+  def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   {
     Swing_Thread.require()
 
@@ -127,7 +126,7 @@
         } yield range
 
       val reparse =
-        snapshot.node.thy_load_commands.exists(cmd => cmd.blobs_names.exists(changed_blobs(_)))
+        snapshot.node.thy_load_commands.exists(cmd => cmd.blobs_names.exists(doc_blobs.changed))
 
       (reparse,
         Document.Node.Perspective(node_required,
@@ -144,15 +143,21 @@
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
-  def blob(): (Bytes, Command.File) =
+  def get_blob(): Option[Document.Blob] =
     Swing_Thread.require {
-      _blob match {
-        case Some(x) => x
-        case None =>
-          val b = PIDE.thy_load.file_content(buffer)
-          val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
-          _blob = Some((b, file))
-          (b, file)
+      if (is_theory) None
+      else {
+        val (bytes, file) =
+          _blob match {
+            case Some(x) => x
+            case None =>
+              val bytes = PIDE.thy_load.file_content(buffer)
+              val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
+              _blob = Some((bytes, file))
+              (bytes, file)
+          }
+        val changed = pending_edits.is_pending()
+        Some(Document.Blob(bytes, file, changed))
       }
     }
 
@@ -165,7 +170,7 @@
 
     val header = node_header()
     val text = JEdit_Lib.buffer_text(buffer)
-    val (_, perspective) = node_perspective(Set.empty)
+    val (_, perspective) = node_perspective(Document.Blobs.empty)
 
     if (is_theory)
       List(session.header_edit(node_name, header),
@@ -213,11 +218,11 @@
     def is_pending(): Boolean = pending_clear || !pending.isEmpty
     def snapshot(): List[Text.Edit] = pending.toList
 
-    def flushed_edits(changed_blobs: Set[Document.Node.Name]): List[Document.Edit_Text] =
+    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
     {
       val clear = pending_clear
       val edits = snapshot()
-      val (reparse, perspective) = node_perspective(changed_blobs)
+      val (reparse, perspective) = node_perspective(doc_blobs)
       if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
         pending_clear = false
         pending.clear
@@ -240,14 +245,11 @@
     }
   }
 
-  def has_pending_edits(): Boolean =
-    Swing_Thread.require { pending_edits.is_pending() }
-
   def snapshot(): Document.Snapshot =
     Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
 
-  def flushed_edits(changed_blobs: Set[Document.Node.Name]): List[Document.Edit_Text] =
-    Swing_Thread.require { pending_edits.flushed_edits(changed_blobs) }
+  def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
+    Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
 
 
   /* buffer listener */
diff -r 47ed6a67a304 -r da0513d95155 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -26,17 +26,9 @@
   {
     Swing_Thread.require()
 
-    val models = PIDE.document_models()
-    val changed_blobs =
-      (for {
-        model <- models.iterator
-        if !model.is_theory && model.has_pending_edits
-      } yield model.node_name).toSet
-
-    System.console.writer.println("\nchanged_blobs = " + changed_blobs)
-
-    val edits = models.flatMap(_.flushed_edits(changed_blobs))
-    if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
+    val doc_blobs = PIDE.document_blobs()
+    val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
+    if (!edits.isEmpty) session.update(doc_blobs, edits)
   }
 
   private val delay_flush =
diff -r 47ed6a67a304 -r da0513d95155 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -83,11 +83,12 @@
     } yield model
 
   def document_blobs(): Document.Blobs =
-    (for {
-      buffer <- JEdit_Lib.jedit_buffers()
-      model <- document_model(buffer)
-      if !model.is_theory
-    } yield (model.node_name -> model.blob())).toMap
+    Document.Blobs(
+      (for {
+        buffer <- JEdit_Lib.jedit_buffers()
+        model <- document_model(buffer)
+        blob <- model.get_blob()
+      } yield (model.node_name -> blob)).toMap)
 
   def exit_models(buffers: List[Buffer])
   {