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";
     1 (*  Title:      Pure/PIDE/document_id.ML
     2     Author:     Makarius
     3 
     4 Unique identifiers for document structure.
     5 
     6 NB: ML ticks forwards > 0, JVM ticks backwards < 0.
     7 *)
     8 
     9 signature DOCUMENT_ID =
    10 sig
    11   type generic = int
    12   type version = generic
    13   type command = generic
    14   type exec = generic
    15   type execution = generic
    16   val none: generic
    17   val make: unit -> generic
    18   val parse: string -> generic
    19   val print: generic -> string
    20 end;
    21 
    22 structure Document_ID: DOCUMENT_ID =
    23 struct
    24 
    25 type generic = int;
    26 type version = generic;
    27 type command = generic;
    28 type exec = generic;
    29 type execution = generic;
    30 
    31 val none = 0;
    32 val make = Counter.make ();
    33 
    34 val parse = Value.parse_int;
    35 val print = Value.print_int;
    36 
    37 end;
    38