src/Pure/PIDE/line.scala
changeset 64649 d67c3094a0c2
parent 64647 bbfcef118acb
child 64650 011629dda937
equal deleted inserted replaced
64648:5d7f741aaccb 64649:d67c3094a0c2
    56 
    56 
    57     def print: String =
    57     def print: String =
    58       if (start == stop) start.print
    58       if (start == stop) start.print
    59       else start.print + ".." + stop.print
    59       else start.print + ".." + stop.print
    60   }
    60   }
       
    61 
       
    62 
       
    63   /* positions within document node */
       
    64 
       
    65   sealed case class Position_Node(pos: Position, name: String)
       
    66   sealed case class Range_Node(range: Range, name: String)
    61 
    67 
    62 
    68 
    63   /* document with newline as separator (not terminator) */
    69   /* document with newline as separator (not terminator) */
    64 
    70 
    65   object Document
    71   object Document