src/Pure/PIDE/document_id.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 63806 c54a53ef1873
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@52530
     1
(*  Title:      Pure/PIDE/document_id.ML
wenzelm@52530
     2
    Author:     Makarius
wenzelm@52530
     3
wenzelm@52530
     4
Unique identifiers for document structure.
wenzelm@52530
     5
wenzelm@52530
     6
NB: ML ticks forwards > 0, JVM ticks backwards < 0.
wenzelm@52530
     7
*)
wenzelm@52530
     8
wenzelm@52530
     9
signature DOCUMENT_ID =
wenzelm@52530
    10
sig
wenzelm@52531
    11
  type generic = int
wenzelm@52531
    12
  type version = generic
wenzelm@52531
    13
  type command = generic
wenzelm@52531
    14
  type exec = generic
wenzelm@52606
    15
  type execution = generic
wenzelm@52531
    16
  val none: generic
wenzelm@52531
    17
  val make: unit -> generic
wenzelm@52531
    18
  val parse: string -> generic
wenzelm@52531
    19
  val print: generic -> string
wenzelm@52530
    20
end;
wenzelm@52530
    21
wenzelm@52530
    22
structure Document_ID: DOCUMENT_ID =
wenzelm@52530
    23
struct
wenzelm@52530
    24
wenzelm@52531
    25
type generic = int;
wenzelm@52531
    26
type version = generic;
wenzelm@52531
    27
type command = generic;
wenzelm@52531
    28
type exec = generic;
wenzelm@52606
    29
type execution = generic;
wenzelm@52530
    30
wenzelm@52530
    31
val none = 0;
wenzelm@52537
    32
val make = Counter.make ();
wenzelm@52530
    33
wenzelm@63806
    34
val parse = Value.parse_int;
wenzelm@63806
    35
val print = Value.print_int;
wenzelm@52530
    36
wenzelm@52530
    37
end;
wenzelm@52530
    38