src/Pure/PIDE/document_id.scala
author wenzelm
Fri, 05 Jul 2013 16:01:45 +0200
changeset 52531 21f8e0e151f5
parent 52530 99dd8b4ef3fe
child 52537 4b5941730bd8
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff changeset
    12
object Document_ID
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff changeset
    13
{
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    14
  type Generic = Long
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    15
  type Version = Generic
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    16
  type Command = Generic
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    17
  type Exec = Generic
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff changeset
    18
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    19
  val none: Generic = 0
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    20
  val make = Counter()
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff changeset
    21
52531
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    22
  def apply(id: Generic): String = Properties.Value.Long.apply(id)
21f8e0e151f5 tuned signature;
wenzelm
parents: 52530
diff changeset
    23
  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
    24
}
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff changeset
    25