src/Pure/PIDE/document.scala
changeset 66714 9fc4e144693c
parent 66379 6392766f3c25
child 66716 8737b866bd1c
--- a/src/Pure/PIDE/document.scala	Fri Sep 29 17:03:33 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Sep 29 17:28:44 2017 +0200
@@ -126,6 +126,11 @@
       def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     }
 
+    sealed case class Entry(name: Node.Name, header: Node.Header)
+    {
+      override def toString: String = name.toString
+    }
+
 
     /* node overlays */