author | wenzelm |
Fri, 05 Jul 2013 18:37:44 +0200 | |
changeset 52534 | 341ae9cd4743 |
parent 52531 | 21f8e0e151f5 |
child 52537 | 4b5941730bd8 |
permissions | -rw-r--r-- |
/* 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() def apply(id: Generic): String = Properties.Value.Long.apply(id) def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s) }