tuned signature -- more static typing;

--- 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(", ",", ")")
   }
 

--- 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)