src/Pure/PIDE/document_id.ML
author wenzelm
Fri Jul 05 23:10:18 2013 +0200 (2013-07-05)
changeset 52537 4b5941730bd8
parent 52531 21f8e0e151f5
child 52606 0d68d108d7e0
permissions -rw-r--r--
more uniform Counter in ML and Scala;
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@52531
    15
  val none: generic
wenzelm@52531
    16
  val make: unit -> generic
wenzelm@52531
    17
  val parse: string -> generic
wenzelm@52531
    18
  val print: generic -> string
wenzelm@52530
    19
end;
wenzelm@52530
    20
wenzelm@52530
    21
structure Document_ID: DOCUMENT_ID =
wenzelm@52530
    22
struct
wenzelm@52530
    23
wenzelm@52531
    24
type generic = int;
wenzelm@52531
    25
type version = generic;
wenzelm@52531
    26
type command = generic;
wenzelm@52531
    27
type exec = generic;
wenzelm@52530
    28
wenzelm@52530
    29
val none = 0;
wenzelm@52537
    30
val make = Counter.make ();
wenzelm@52530
    31
wenzelm@52530
    32
val parse = Markup.parse_int;
wenzelm@52530
    33
val print = Markup.print_int;
wenzelm@52530
    34
wenzelm@52530
    35
end;
wenzelm@52530
    36