| author | wenzelm |
| Mon, 27 Feb 2023 15:09:59 +0100 | |
| changeset 77398 | 19e9cafaafc5 |
| parent 75393 | 87ebf5a50283 |
| child 80462 | 7a1f9e571046 |
| 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 = Counter.make() def apply(id: Generic): String = Value.Long.apply(id) def unapply(s: String): Option[Generic] = Value.Long.unapply(s) }