src/Pure/PIDE/document_id.scala
author wenzelm
Fri, 05 Jul 2013 23:10:18 +0200
changeset 52537 4b5941730bd8
parent 52531 21f8e0e151f5
child 56744 0b74d1df4b8e
permissions -rw-r--r--
more uniform Counter in ML and Scala;

/*  Title:      Pure/PIDE/document_id.scala
    Author:     Makarius

Unique identifiers for document structure.

NB: ML ticks forwards > 0, JVM ticks backwards < 0.
*/

package isabelle


object Document_ID
{
  type Generic = Long
  type Version = Generic
  type Command = Generic
  type Exec = Generic

  val none: Generic = 0
  val make = Counter.make()

  def apply(id: Generic): String = Properties.Value.Long.apply(id)
  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
}