diff -r afba7ffd6492 -r 9fc4e144693c src/Pure/PIDE/document.scala --- 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 */