src/Pure/PIDE/document.ML
author wenzelm
Sat Aug 14 22:45:23 2010 +0200 (2010-08-14 ago)
changeset 38414 49f1f657adc2
parent 38373 e8197eea3cd0
child 38418 9a7af64d71bb
permissions -rw-r--r--
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;
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@38363
    10
  type id = int
wenzelm@38373
    11
  type version_id = id
wenzelm@38363
    12
  type command_id = id
wenzelm@38373
    13
  type exec_id = id
wenzelm@38363
    14
  val no_id: id
wenzelm@38363
    15
  val parse_id: string -> id
wenzelm@38363
    16
  val print_id: id -> string
wenzelm@38150
    17
  type edit = string * ((command_id * command_id option) list) option
wenzelm@38150
    18
end;
wenzelm@38150
    19
wenzelm@38150
    20
structure Document: DOCUMENT =
wenzelm@38150
    21
struct
wenzelm@38150
    22
wenzelm@38150
    23
(* unique identifiers *)
wenzelm@38150
    24
wenzelm@38363
    25
type id = int;
wenzelm@38373
    26
type version_id = id;
wenzelm@38363
    27
type command_id = id;
wenzelm@38373
    28
type exec_id = id;
wenzelm@38355
    29
wenzelm@38355
    30
val no_id = 0;
wenzelm@38150
    31
wenzelm@38414
    32
val parse_id = Markup.parse_int;
wenzelm@38414
    33
val print_id = Markup.print_int;
wenzelm@38150
    34
wenzelm@38150
    35
wenzelm@38150
    36
(* edits *)
wenzelm@38150
    37
wenzelm@38150
    38
type edit =
wenzelm@38150
    39
  string *  (*node name*)
wenzelm@38150
    40
  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
wenzelm@38150
    41
wenzelm@38150
    42
end;
wenzelm@38150
    43