isabelle: src/Pure/PIDE/document_id.scala@448325de6e4f (annotated)

52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	1	/* Title: Pure/PIDE/document_id.scala
56744 0b74d1df4b8e tuned headers; wenzelm parents: 52537 diff changeset	2	Module: PIDE
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	3	Author: Makarius
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	4
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	5	Unique identifiers for document structure.
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	6
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	7	NB: ML ticks forwards > 0, JVM ticks backwards < 0.
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	8	*/
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	9
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	10	package isabelle
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	11
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	12
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	13	object Document_ID
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	14	{
52531 21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	15	type Generic = Long
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	16	type Version = Generic
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	17	type Command = Generic
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	18	type Exec = Generic
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	19
52531 21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	20	val none: Generic = 0
52537 4b5941730bd8 more uniform Counter in ML and Scala; wenzelm parents: 52531 diff changeset	21	val make = Counter.make()
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	22
52531 21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	23	def apply(id: Generic): String = Properties.Value.Long.apply(id)
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	24	def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	25	}
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	26

author	wenzelm
	Tue, 12 Aug 2014 17:28:07 +0200
changeset 57915	448325de6e4f
parent 56744	0b74d1df4b8e
child 63805	c272680df665
permissions	-rw-r--r--