| author | wenzelm | 
| Wed, 30 Dec 2015 20:12:26 +0100 | |
| changeset 61992 | 6d02bb8b5fe1 | 
| parent 56744 | 0b74d1df4b8e | 
| child 63805 | c272680df665 | 
| permissions | -rw-r--r-- | 
/* Title: Pure/PIDE/document_id.scala Module: PIDE 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) }