src/Pure/PIDE/document_id.ML
author wenzelm
Mon Sep 05 23:11:00 2016 +0200 (2016-09-05 ago)
changeset 63806 c54a53ef1873
parent 52606 0d68d108d7e0
permissions -rw-r--r--
clarified modules;
     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