# HG changeset patch # User wenzelm # Date 1396272494 -7200 # Node ID 60434514ec0ae0444d00d08cbc569f5e5463de6f # Parent 8953d4cc060abd46f107114ae495fc5d525984e7 tuned signature -- more static typing; diff -r 8953d4cc060a -r 60434514ec0a src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Mar 31 15:05:24 2014 +0200 +++ b/src/Pure/PIDE/document.scala Mon Mar 31 15:28:14 2014 +0200 @@ -52,19 +52,17 @@ object Blobs { - def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty) + 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], default_nodes: Nodes) + final class Blobs private(blobs: Map[Node.Name, Blob]) { 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) orElse default_nodes(name).get_blob + def get(name: Node.Name): Option[Blob] = blobs.get(name) def changed(name: Node.Name): Boolean = get(name) match { @@ -72,8 +70,6 @@ case None => false } - def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes) - override def toString: String = blobs.mkString("Blobs(", ",", ")") } diff -r 8953d4cc060a -r 60434514ec0a src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Mar 31 15:05:24 2014 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 31 15:28:14 2014 +0200 @@ -262,14 +262,14 @@ syntax: Outer_Syntax, node_name: Document.Node.Name, span: List[Token], - doc_blobs_default: Document.Blobs) + get_blob: Document.Node.Name => Option[Document.Blob]) : 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_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) + val blob = get_blob(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_default: Document.Blobs, + get_blob: Document.Node.Name => Option[Document.Blob], 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_default), span)) + map(span => (resolve_files(resources, syntax, name, span, get_blob), 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_default: Document.Blobs, + get_blob: Document.Node.Name => Option[Document.Blob], 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_default, name, cmds, first, last)) + recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last)) case None => cmds } recover(commands) @@ -355,7 +355,7 @@ private def consolidate_spans( resources: Resources, syntax: Outer_Syntax, - doc_blobs_default: Document.Blobs, + get_blob: Document.Node.Name => Option[Document.Blob], reparse_limit: Int, name: Document.Node.Name, perspective: Command.Perspective, @@ -375,8 +375,7 @@ last = it.next i += last.length } - reparse_spans( - resources, syntax, doc_blobs_default, name, commands, first_unfinished, last) + reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last) case None => commands } case None => commands @@ -400,7 +399,7 @@ private def text_edit( resources: Resources, syntax: Outer_Syntax, - doc_blobs_default: Document.Blobs, + get_blob: Document.Node.Name => Option[Document.Blob], reparse_limit: Int, node: Document.Node, edit: Document.Edit_Text): Document.Node = { @@ -414,8 +413,7 @@ val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) val commands2 = - recover_spans( - resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1) + recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1) node.update_commands(commands2) } else node @@ -429,7 +427,7 @@ if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit, + consolidate_spans(resources, syntax, get_blob, reparse_limit, name, visible, node.commands)) } } @@ -441,6 +439,9 @@ doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Session.Change = { + def get_blob(name: Document.Node.Name) = + doc_blobs.get(name) orElse previous.nodes(name).get_blob + val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = header_edits(resources.base_syntax, previous, edits) @@ -456,8 +457,6 @@ }) 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 @@ -473,11 +472,11 @@ val node1 = if (reparse_set(name) && !commands.isEmpty) node.update_commands( - reparse_spans(resources, syntax, doc_blobs_default, + reparse_spans(resources, syntax, get_blob, name, commands, commands.head, commands.last)) else node val node2 = - (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _)) + (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _)) if (!(node.same_perspective(node2.perspective))) doc_edits += (name -> node2.perspective)