clarified Document.Blobs environment vs. actual edits of auxiliary files;
more robust handling of vacuous edits;
--- a/src/Pure/PIDE/document.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Pure/PIDE/document.scala Tue Nov 19 20:53:43 2013 +0100
@@ -47,6 +47,8 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[Command.Edit, Command.Perspective]
+ type Blobs = Map[Node.Name, Bytes]
+
object Node
{
val empty: Node = new Node()
@@ -125,7 +127,7 @@
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
case class Deps[A, B](header: Header) extends Edit[A, B]
case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
- case class Blob[A, B](blob: Bytes) extends Edit[A, B]
+ case class Blob[A, B]() extends Edit[A, B]
type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
--- a/src/Pure/System/session.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Pure/System/session.scala Tue Nov 19 20:53:43 2013 +0100
@@ -25,7 +25,7 @@
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])
@@ -167,6 +167,7 @@
//{{{
private case class Text_Edits(
previous: Future[Document.Version],
+ doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
version_result: Promise[Document.Version])
@@ -177,14 +178,14 @@
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)
}
@@ -250,7 +251,7 @@
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)
@@ -349,7 +350,7 @@
/* 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()
@@ -358,8 +359,8 @@
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)
}
//}}}
@@ -379,7 +380,7 @@
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)
@@ -523,7 +524,7 @@
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(())
@@ -531,8 +532,8 @@
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 =>
@@ -585,8 +586,8 @@
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) }
--- a/src/Pure/Thy/thy_load.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala Tue Nov 19 20:53:43 2013 +0100
@@ -99,8 +99,11 @@
/* theory text edits */
- def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
- : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
- Thy_Syntax.text_edits(this, reparse_limit, previous, edits)
+ def text_edits(
+ reparse_limit: Int,
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+ Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
}
--- a/src/Pure/Thy/thy_syntax.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Tue Nov 19 20:53:43 2013 +0100
@@ -256,14 +256,14 @@
syntax: Outer_Syntax,
node_name: Document.Node.Name,
span: List[Token],
- all_blobs: Map[Document.Node.Name, Bytes])
+ doc_blobs: Document.Blobs)
: List[Command.Blob] =
{
span_files(syntax, span).map(file =>
Exn.capture {
val name =
Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
- all_blobs.get(name) match {
+ doc_blobs.get(name) match {
case Some(blob) => (name, blob.sha1_digest)
case None => error("No such file: " + quote(name.toString))
}
@@ -286,7 +286,7 @@
private def reparse_spans(
thy_load: Thy_Load,
syntax: Outer_Syntax,
- all_blobs: Map[Document.Node.Name, Bytes],
+ doc_blobs: Document.Blobs,
name: Document.Node.Name,
commands: Linear_Set[Command],
first: Command, last: Command): Linear_Set[Command] =
@@ -294,7 +294,7 @@
val cmds0 = commands.iterator(first, last).toList
val spans0 =
parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
- map(span => (resolve_files(thy_load, syntax, name, span, all_blobs), span))
+ map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
val (cmds1, spans1) = chop_common(cmds0, spans0)
@@ -321,7 +321,7 @@
private def recover_spans(
thy_load: Thy_Load,
syntax: Outer_Syntax,
- all_blobs: Map[Document.Node.Name, Bytes],
+ doc_blobs: Document.Blobs,
name: Document.Node.Name,
perspective: Command.Perspective,
commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -337,7 +337,7 @@
case Some(first_unparsed) =>
val first = next_invisible_command(cmds.reverse, first_unparsed)
val last = next_invisible_command(cmds, first_unparsed)
- recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last))
+ recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
case None => cmds
}
recover(commands)
@@ -349,7 +349,7 @@
private def consolidate_spans(
thy_load: Thy_Load,
syntax: Outer_Syntax,
- all_blobs: Map[Document.Node.Name, Bytes],
+ doc_blobs: Document.Blobs,
reparse_limit: Int,
name: Document.Node.Name,
perspective: Command.Perspective,
@@ -369,7 +369,7 @@
last = it.next
i += last.length
}
- reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last)
+ reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
case None => commands
}
case None => commands
@@ -393,7 +393,7 @@
private def text_edit(
thy_load: Thy_Load,
syntax: Outer_Syntax,
- all_blobs: Map[Document.Node.Name, Bytes],
+ doc_blobs: Document.Blobs,
reparse_limit: Int,
node: Document.Node, edit: Document.Edit_Text): Document.Node =
{
@@ -404,7 +404,7 @@
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
val commands2 =
- recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1)
+ recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
node.update_commands(commands2)
case (_, Document.Node.Deps(_)) => node
@@ -416,10 +416,10 @@
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(thy_load, syntax, all_blobs, reparse_limit,
+ consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
name, visible, node.commands))
- case (_, Document.Node.Blob(_)) => node
+ case (_, Document.Node.Blob()) => node
}
}
@@ -427,56 +427,53 @@
thy_load: Thy_Load,
reparse_limit: Int,
previous: Document.Version,
+ doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text])
- : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
+ : (List[Document.Edit_Command], Document.Version) =
{
val (syntax, reparse0, nodes0, doc_edits0) =
header_edits(thy_load.base_syntax, previous, edits)
- val reparse =
- (reparse0 /: nodes0.entries)({
- case (reparse, (name, node)) =>
- if (node.thy_load_commands.isEmpty) reparse
- else name :: reparse
- })
- val reparse_set = reparse.toSet
+ if (edits.isEmpty)
+ (Nil, Document.Version.make(syntax, previous.nodes))
+ else {
+ val reparse =
+ (reparse0 /: nodes0.entries)({
+ case (reparse, (name, node)) =>
+ if (node.thy_load_commands.isEmpty) reparse
+ else name :: reparse
+ })
+ val reparse_set = reparse.toSet
- var nodes = nodes0
- val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+ var nodes = nodes0
+ val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+
+ val node_edits =
+ (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+ .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
- val node_edits =
- (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
- .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
+ node_edits foreach {
+ case (name, edits) =>
+ val node = nodes(name)
+ val commands = node.commands
- val all_blobs: Map[Document.Node.Name, Bytes] =
- (Map.empty[Document.Node.Name, Bytes] /: node_edits) {
- case (bs1, (_, es)) => (bs1 /: es) {
- case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob)
- case (bs, _) => bs
- }
+ val node1 =
+ if (reparse_set(name) && !commands.isEmpty)
+ node.update_commands(
+ reparse_spans(thy_load, syntax, doc_blobs,
+ name, commands, commands.head, commands.last))
+ else node
+ val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
+
+ if (!(node.same_perspective(node2.perspective)))
+ doc_edits += (name -> node2.perspective)
+
+ doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+ nodes += (name -> node2)
}
- node_edits foreach {
- case (name, edits) =>
- val node = nodes(name)
- val commands = node.commands
-
- val node1 =
- if (reparse_set(name) && !commands.isEmpty)
- node.update_commands(
- reparse_spans(thy_load, syntax, all_blobs,
- name, commands, commands.head, commands.last))
- else node
- val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _))
-
- if (!(node.same_perspective(node2.perspective)))
- doc_edits += (name -> node2.perspective)
-
- doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
-
- nodes += (name -> node2)
+ (doc_edits.toList, Document.Version.make(syntax, nodes))
}
-
- (all_blobs, doc_edits.toList, Document.Version.make(syntax, nodes))
}
}
--- a/src/Tools/jEdit/src/document_model.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Nov 19 20:53:43 2013 +0100
@@ -148,7 +148,7 @@
node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
node_name -> perspective)
else
- List(node_name -> Document.Node.Blob(blob()))
+ List(node_name -> Document.Node.Blob())
}
def node_edits(
@@ -171,7 +171,7 @@
node_name -> perspective)
}
else
- List(node_name -> Document.Node.Blob(blob()))
+ List(node_name -> Document.Node.Blob())
}
@@ -190,7 +190,7 @@
val clear = pending_clear
val edits = snapshot()
val perspective = node_perspective()
- if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) {
+ if (clear || !edits.isEmpty || last_perspective != perspective) {
pending_clear = false
pending.clear
last_perspective = perspective
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 19 20:53:43 2013 +0100
@@ -19,21 +19,21 @@
override def session: Session = PIDE.session
+ def document_models(): List[Document_Model] =
+ for {
+ buffer <- JEdit_Lib.jedit_buffers().toList
+ model <- PIDE.document_model(buffer)
+ } yield model
+
+ def document_blobs(): Document.Blobs =
+ document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
+
override def flush()
{
Swing_Thread.require()
- session.update(
- (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
- case (edits, buffer) =>
- JEdit_Lib.buffer_lock(buffer) {
- PIDE.document_model(buffer) match {
- case Some(model) => model.flushed_edits() ::: edits
- case None => edits
- }
- }
- }
- )
+ val edits = document_models().flatMap(_.flushed_edits())
+ if (!edits.isEmpty) session.update(document_blobs(), edits)
}
private val delay_flush =
--- a/src/Tools/jEdit/src/plugin.scala Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Nov 19 20:53:43 2013 +0100
@@ -113,7 +113,7 @@
model_edits ::: edits
}
}
- session.update(init_edits)
+ session.update(PIDE.editor.document_blobs(), init_edits)
}
}