src/Pure/PIDE/document.ML
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 38150 67fc24df3721
child 38363 af7f41a8a0a8
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm@38150
     1
(*  Title:      Pure/PIDE/document.ML
wenzelm@38150
     2
    Author:     Makarius
wenzelm@38150
     3
wenzelm@38150
     4
Document as collection of named nodes, each consisting of an editable
wenzelm@38150
     5
list of commands.
wenzelm@38150
     6
*)
wenzelm@38150
     7
wenzelm@38150
     8
signature DOCUMENT =
wenzelm@38150
     9
sig
wenzelm@38355
    10
  type state_id = int
wenzelm@38355
    11
  type command_id = int
wenzelm@38355
    12
  type version_id = int
wenzelm@38355
    13
  val no_id: int
wenzelm@38355
    14
  val parse_id: string -> int
wenzelm@38355
    15
  val print_id: int -> string
wenzelm@38150
    16
  type edit = string * ((command_id * command_id option) list) option
wenzelm@38150
    17
end;
wenzelm@38150
    18
wenzelm@38150
    19
structure Document: DOCUMENT =
wenzelm@38150
    20
struct
wenzelm@38150
    21
wenzelm@38150
    22
(* unique identifiers *)
wenzelm@38150
    23
wenzelm@38355
    24
type state_id = int;
wenzelm@38355
    25
type command_id = int;
wenzelm@38355
    26
type version_id = int;
wenzelm@38355
    27
wenzelm@38355
    28
val no_id = 0;
wenzelm@38150
    29
wenzelm@38355
    30
fun parse_id s =
wenzelm@38355
    31
  (case Int.fromString s of
wenzelm@38355
    32
    SOME i => i
wenzelm@38355
    33
  | NONE => raise Fail ("Bad id: " ^ quote s));
wenzelm@38355
    34
wenzelm@38355
    35
val print_id = signed_string_of_int;
wenzelm@38150
    36
wenzelm@38150
    37
wenzelm@38150
    38
(* edits *)
wenzelm@38150
    39
wenzelm@38150
    40
type edit =
wenzelm@38150
    41
  string *  (*node name*)
wenzelm@38150
    42
  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
wenzelm@38150
    43
wenzelm@38150
    44
end;
wenzelm@38150
    45