src/Pure/PIDE/document_id.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 64370 865b39487b5d
child 66416 96ad7d5ff613
permissions -rw-r--r--
clarified modules;
     1 /*  Title:      Pure/PIDE/document_id.scala
     2     Author:     Makarius
     3 
     4 Unique identifiers for document structure.
     5 
     6 NB: ML ticks forwards > 0, JVM ticks backwards < 0.
     7 */
     8 
     9 package isabelle
    10 
    11 
    12 object Document_ID
    13 {
    14   type Generic = Long
    15   type Version = Generic
    16   type Command = Generic
    17   type Exec = Generic
    18 
    19   val none: Generic = 0
    20   val make = Counter.make()
    21 
    22   def apply(id: Generic): String = Value.Long.apply(id)
    23   def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
    24 }
    25