src/Pure/PIDE/document_id.ML
author wenzelm
Tue Aug 12 18:36:43 2014 +0200 (2014-08-12)
changeset 57916 2c2c24dbf0a4
parent 52606 0d68d108d7e0
child 63806 c54a53ef1873
permissions -rw-r--r--
generic process wrapping in Prover;
clarified module arrangement;
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@52530
    34
val parse = Markup.parse_int;
wenzelm@52530
    35
val print = Markup.print_int;
wenzelm@52530
    36
wenzelm@52530
    37
end;
wenzelm@52530
    38