src/Pure/PIDE/document.ML
author wenzelm
Thu, 12 Aug 2010 15:19:11 +0200
changeset 38363 af7f41a8a0a8
parent 38355 8cb265fb12fe
child 38373 e8197eea3cd0
permissions -rw-r--r--
clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/PIDE/document.ML
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     3
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     4
Document as collection of named nodes, each consisting of an editable
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     5
list of commands.
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     6
*)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     7
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     8
signature DOCUMENT =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
     9
sig
38363
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    10
  type id = int
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    11
  type exec_id = id
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    12
  type command_id = id
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    13
  type version_id = id
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    14
  val no_id: id
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    15
  val parse_id: string -> id
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    16
  val print_id: id -> string
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    17
  type edit = string * ((command_id * command_id option) list) option
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    18
end;
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    19
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    20
structure Document: DOCUMENT =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    21
struct
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    22
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    23
(* unique identifiers *)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    24
38363
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    25
type id = int;
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    26
type exec_id = id;
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    27
type command_id = id;
af7f41a8a0a8 clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents: 38355
diff changeset
    28
type version_id = id;
38355
8cb265fb12fe 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
parents: 38150
diff changeset
    29
8cb265fb12fe 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
parents: 38150
diff changeset
    30
val no_id = 0;
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    31
38355
8cb265fb12fe 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
parents: 38150
diff changeset
    32
fun parse_id s =
8cb265fb12fe 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
parents: 38150
diff changeset
    33
  (case Int.fromString s of
8cb265fb12fe 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
parents: 38150
diff changeset
    34
    SOME i => i
8cb265fb12fe 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
parents: 38150
diff changeset
    35
  | NONE => raise Fail ("Bad id: " ^ quote s));
8cb265fb12fe 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
parents: 38150
diff changeset
    36
8cb265fb12fe 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
parents: 38150
diff changeset
    37
val print_id = signed_string_of_int;
38150
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    38
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    39
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    40
(* edits *)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    41
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    42
type edit =
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    43
  string *  (*node name*)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    44
  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    45
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    46
end;
67fc24df3721 simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff changeset
    47