# HG changeset patch # User wenzelm # Date 1396271124 -7200 # Node ID 8953d4cc060abd46f107114ae495fc5d525984e7 # Parent 6b3739fee456ed44af90988445bfbbf4649d4a04 store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index; diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/General/symbol.scala Mon Mar 31 15:05:24 2014 +0200 @@ -165,6 +165,13 @@ else index(i).chr + sym - index(i).sym } def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_)) + + override def hashCode: Int = index.hashCode + override def equals(that: Any): Boolean = + that match { + case other: Index => index.sameElements(other.index) + case _ => false + } } diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/PIDE/command.scala Mon Mar 31 15:05:24 2014 +0200 @@ -225,6 +225,7 @@ } } + // file name and position information, *without* persistent text class File(val file_name: String, text: CharSequence) extends Chunk { val length = text.length @@ -232,6 +233,17 @@ private val symbol_index = Symbol.Index(text) def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range) + private val hash: Int = (file_name, length, symbol_index).hashCode + override def hashCode: Int = hash + override def equals(that: Any): Boolean = + that match { + case other: File => + hash == other.hash && + file_name == other.file_name && + length == other.length && + symbol_index == other.symbol_index + case _ => false + } override def toString: String = "Command.File(" + file_name + ")" } diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/PIDE/document.scala Mon Mar 31 15:05:24 2014 +0200 @@ -46,20 +46,25 @@ /* document blobs: auxiliary files */ sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean) + { + def unchanged: Blob = copy(changed = false) + } object Blobs { - def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs) + def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty) val empty: Blobs = apply(Map.empty) } - final class Blobs private(blobs: Map[Node.Name, Blob]) + final class Blobs private(blobs: Map[Node.Name, Blob], default_nodes: Nodes) { private lazy val digests: Map[SHA1.Digest, Blob] = for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob) def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest) - def get(name: Node.Name): Option[Blob] = blobs.get(name) + + def get(name: Node.Name): Option[Blob] = + blobs.get(name) orElse default_nodes(name).get_blob def changed(name: Node.Name): Boolean = get(name) match { @@ -67,6 +72,8 @@ case None => false } + def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes) + override def toString: String = blobs.mkString("Blobs(", ",", ")") } @@ -157,7 +164,7 @@ } } case class Clear[A, B]() extends Edit[A, B] - case class Blob[A, B]() extends Edit[A, B] + case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] @@ -222,7 +229,7 @@ } final class Node private( - val is_blob: Boolean = false, + val get_blob: Option[Document.Blob] = None, val header: Node.Header = Node.bad_header("Bad theory header"), val perspective: Node.Perspective_Command = Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty), @@ -230,13 +237,13 @@ { def clear: Node = new Node(header = header) - def init_blob: Node = new Node(is_blob = true) + def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged)) def update_header(new_header: Node.Header): Node = - new Node(is_blob, new_header, perspective, _commands) + new Node(get_blob, new_header, perspective, _commands) def update_perspective(new_perspective: Node.Perspective_Command): Node = - new Node(is_blob, header, new_perspective, _commands) + new Node(get_blob, header, new_perspective, _commands) def same_perspective(other_perspective: Node.Perspective_Command): Boolean = perspective.required == other_perspective.required && @@ -248,7 +255,7 @@ def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this - else new Node(is_blob, header, perspective, Node.Commands(new_commands)) + else new Node(get_blob, header, perspective, Node.Commands(new_commands)) def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.range(i) diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Mon Mar 31 15:05:24 2014 +0200 @@ -319,9 +319,8 @@ { /* inlined files */ - def define_blob(blob: Document.Blob): Unit = - protocol_command_raw( - "Document.define_blob", Bytes(blob.bytes.sha1_digest.toString), blob.bytes) + def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = + protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes) /* commands */ diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/PIDE/session.scala Mon Mar 31 15:05:24 2014 +0200 @@ -384,7 +384,7 @@ change.doc_blobs.get(digest) match { case Some(blob) => global_state >> (_.define_blob(digest)) - prover.get.define_blob(blob) + prover.get.define_blob(digest, blob.bytes) case None => System.err.println("Missing blob for SHA1 digest " + digest) } diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 31 15:05:24 2014 +0200 @@ -262,14 +262,14 @@ syntax: Outer_Syntax, node_name: Document.Node.Name, span: List[Token], - doc_blobs: Document.Blobs) + doc_blobs_default: Document.Blobs) : List[Command.Blob] = { span_files(syntax, span).map(file_name => Exn.capture { val name = Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) - val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) + val blob = doc_blobs_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) (name, blob) }) } @@ -292,7 +292,7 @@ private def reparse_spans( resources: Resources, syntax: Outer_Syntax, - doc_blobs: Document.Blobs, + doc_blobs_default: Document.Blobs, name: Document.Node.Name, commands: Linear_Set[Command], first: Command, last: Command): Linear_Set[Command] = @@ -300,7 +300,7 @@ val cmds0 = commands.iterator(first, last).toList val blobs_spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). - map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span)) + map(span => (resolve_files(resources, syntax, name, span, doc_blobs_default), span)) val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0) @@ -327,7 +327,7 @@ private def recover_spans( resources: Resources, syntax: Outer_Syntax, - doc_blobs: Document.Blobs, + doc_blobs_default: Document.Blobs, name: Document.Node.Name, perspective: Command.Perspective, commands: Linear_Set[Command]): Linear_Set[Command] = @@ -343,7 +343,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(resources, syntax, doc_blobs, name, cmds, first, last)) + recover(reparse_spans(resources, syntax, doc_blobs_default, name, cmds, first, last)) case None => cmds } recover(commands) @@ -355,7 +355,7 @@ private def consolidate_spans( resources: Resources, syntax: Outer_Syntax, - doc_blobs: Document.Blobs, + doc_blobs_default: Document.Blobs, reparse_limit: Int, name: Document.Node.Name, perspective: Command.Perspective, @@ -375,7 +375,8 @@ last = it.next i += last.length } - reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last) + reparse_spans( + resources, syntax, doc_blobs_default, name, commands, first_unfinished, last) case None => commands } case None => commands @@ -399,24 +400,25 @@ private def text_edit( resources: Resources, syntax: Outer_Syntax, - doc_blobs: Document.Blobs, + doc_blobs_default: Document.Blobs, reparse_limit: Int, node: Document.Node, edit: Document.Edit_Text): Document.Node = { edit match { case (_, Document.Node.Clear()) => node.clear - case (_, Document.Node.Blob()) => node.init_blob + case (_, Document.Node.Blob(blob)) => node.init_blob(blob) case (name, Document.Node.Edits(text_edits)) => - if (node.is_blob) node - else { + if (name.is_theory) { val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) val commands2 = - recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1) + recover_spans( + resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1) node.update_commands(commands2) } + else node case (_, Document.Node.Deps(_)) => node @@ -427,7 +429,7 @@ if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(resources, syntax, doc_blobs, reparse_limit, + consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit, name, visible, node.commands)) } } @@ -454,6 +456,8 @@ }) val reparse_set = reparse.toSet + val doc_blobs_default = doc_blobs.default(previous.nodes) + var nodes = nodes0 val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 @@ -469,11 +473,11 @@ val node1 = if (reparse_set(name) && !commands.isEmpty) node.update_commands( - reparse_spans(resources, syntax, doc_blobs, + reparse_spans(resources, syntax, doc_blobs_default, name, commands, commands.head, commands.last)) else node val node2 = - (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) + (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _)) if (!(node.same_perspective(node2.perspective))) doc_edits += (name -> node2.perspective) diff -r 6b3739fee456 -r 8953d4cc060a src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Mar 31 12:35:39 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Mar 31 15:05:24 2014 +0200 @@ -164,28 +164,25 @@ /* edits */ def node_edits( - clear: Boolean, - text_edits: List[Text.Edit], - perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = - { - Swing_Thread.require() - - if (is_theory) { - val header_edit = session.header_edit(node_name, node_header()) - if (clear) - List(header_edit, - node_name -> Document.Node.Clear(), - node_name -> Document.Node.Edits(text_edits), - node_name -> perspective) - else - List(header_edit, - node_name -> Document.Node.Edits(text_edits), - node_name -> perspective) + clear: Boolean, + text_edits: List[Text.Edit], + perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = + get_blob() match { + case None => + val header_edit = session.header_edit(node_name, node_header()) + if (clear) + List(header_edit, + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) + else + List(header_edit, + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) + case Some(blob) => + List(node_name -> Document.Node.Blob(blob), + node_name -> Document.Node.Edits(text_edits)) } - else - List(node_name -> Document.Node.Blob(), - node_name -> Document.Node.Edits(text_edits)) - } /* pending edits */