isabelle: src/Pure/PIDE/document_id.scala@5b8fccf0a48a (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
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	2	Author: Makarius
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	3
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	4	Unique identifiers for document structure.
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	5
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	6	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	7	*/
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	package isabelle
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	10
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	11
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 71601 diff changeset	12	object Document_ID {
52531 21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	13	type Generic = Long
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	14	type Version = Generic
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	15	type Command = Generic
21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	16	type Exec = Generic
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	17
52531 21f8e0e151f5 tuned signature; wenzelm parents: 52530 diff changeset	18	val none: Generic = 0
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 66415 diff changeset	19	val make: Counter = Counter.make()
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	20
63805 c272680df665 clarified modules; wenzelm parents: 56744 diff changeset	21	def apply(id: Generic): String = Value.Long.apply(id)
c272680df665 clarified modules; wenzelm parents: 56744 diff changeset	22	def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
80462 7a1f9e571046 clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml; wenzelm parents: 75393 diff changeset	23
7a1f9e571046 clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml; wenzelm parents: 75393 diff changeset	24	def encode(id: Generic): XML.Body = XML.Encode.long(id)
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: diff changeset	25	}

author	wenzelm
	Sat, 10 Aug 2024 20:20:59 +0200
changeset 80684	5b8fccf0a48a
parent 80462	7a1f9e571046
permissions	-rw-r--r--