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