changeset 64649 | d67c3094a0c2 |
parent 64647 | bbfcef118acb |
child 64650 | 011629dda937 |
--- 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