src/Pure/PIDE/document_id.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 66416 96ad7d5ff613
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     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 }