--- 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()
--- 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 */
--- 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(())
--- 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)
- }
- )
+ })
}
--- 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 */
--- 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 =
--- 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])
{