author | wenzelm |
Fri, 05 Jul 2013 23:10:18 +0200 | |
changeset 52537 | 4b5941730bd8 |
parent 52531 | 21f8e0e151f5 |
child 52606 | 0d68d108d7e0 |
permissions | -rw-r--r-- |
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.ML |
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 |
signature DOCUMENT_ID = |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
10 |
sig |
52531 | 11 |
type generic = int |
12 |
type version = generic |
|
13 |
type command = generic |
|
14 |
type exec = generic |
|
15 |
val none: generic |
|
16 |
val make: unit -> generic |
|
17 |
val parse: string -> generic |
|
18 |
val print: generic -> string |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
19 |
end; |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
20 |
|
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
21 |
structure Document_ID: DOCUMENT_ID = |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
22 |
struct |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
23 |
|
52531 | 24 |
type generic = int; |
25 |
type version = generic; |
|
26 |
type command = generic; |
|
27 |
type exec = generic; |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
28 |
|
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
29 |
val none = 0; |
52537 | 30 |
val make = Counter.make (); |
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
31 |
|
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
32 |
val parse = Markup.parse_int; |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
33 |
val print = Markup.print_int; |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
34 |
|
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
35 |
end; |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
diff
changeset
|
36 |