src/Pure/PIDE/document_id.ML
author wenzelm
Sat Mar 01 22:46:31 2014 +0100 (2014-03-01)
changeset 55828 42ac3cfb89f6
parent 52606 0d68d108d7e0
child 63806 c54a53ef1873
permissions -rw-r--r--
clarified language markup: added "delimited" property;
type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche);
observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
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