diff -r 5d7f741aaccb -r d67c3094a0c2 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 21 21:18:37 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 21 22:27:38 2016 +0100
@@ -60,6 +60,12 @@
   }
 
 
+  /* positions within document node */
+
+  sealed case class Position_Node(pos: Position, name: String)
+  sealed case class Range_Node(range: Range, name: String)
+
+
   /* document with newline as separator (not terminator) */
 
   object Document