# HG changeset patch
# User wenzelm
# Date 1546254151 -3600
# Node ID 0a38f23ca4c54e73b040ef441c22b82583e98482
# Parent  b85f4c5cb58882ed6c47933138376e6182a3ff29
clarified signature;

diff -r b85f4c5cb588 -r 0a38f23ca4c5 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Dec 30 17:44:33 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Dec 31 12:02:31 2018 +0100
@@ -293,6 +293,11 @@
 
     def has_header: Boolean = header != Node.no_header
 
+    override def toString: String =
+      if (is_empty) "empty"
+      else if (get_blob.isDefined) "blob"
+      else "node"
+
     def commands: Linear_Set[Command] = _commands.commands
     def load_commands: List[Command] = _commands.load_commands
     def load_commands_changed(doc_blobs: Blobs): Boolean =
@@ -528,6 +533,7 @@
 
     def node_name: Node.Name
     def node: Node
+    def nodes: List[(Node.Name, Node)]
 
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
@@ -1024,6 +1030,10 @@
         val node_name: Node.Name = name
         val node: Node = version.nodes(name)
 
+        def nodes: List[(Node.Name, Node)] =
+          (node_name :: node.load_commands.flatMap(_.blobs_names)).
+            map(name => (name, version.nodes(name)))
+
         val commands_loading: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.commands_loading(node_name)