src/Pure/PIDE/document_id.scala
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 56744 0b74d1df4b8e
child 63805 c272680df665
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/PIDE/document_id.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Unique identifiers for document structure.
     6 
     7 NB: ML ticks forwards > 0, JVM ticks backwards < 0.
     8 */
     9 
    10 package isabelle
    11 
    12 
    13 object Document_ID
    14 {
    15   type Generic = Long
    16   type Version = Generic
    17   type Command = Generic
    18   type Exec = Generic
    19 
    20   val none: Generic = 0
    21   val make = Counter.make()
    22 
    23   def apply(id: Generic): String = Properties.Value.Long.apply(id)
    24   def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
    25 }
    26