src/Pure/PIDE/document.ML
author wenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05)
changeset 38150 67fc24df3721
child 38355 8cb265fb12fe
permissions -rw-r--r--
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
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@38150
    10
  type state_id = string
wenzelm@38150
    11
  type command_id = string
wenzelm@38150
    12
  type version_id = string
wenzelm@38150
    13
  val no_id: string
wenzelm@38150
    14
  type edit = string * ((command_id * command_id option) list) option
wenzelm@38150
    15
end;
wenzelm@38150
    16
wenzelm@38150
    17
structure Document: DOCUMENT =
wenzelm@38150
    18
struct
wenzelm@38150
    19
wenzelm@38150
    20
(* unique identifiers *)
wenzelm@38150
    21
wenzelm@38150
    22
type state_id = string;
wenzelm@38150
    23
type command_id = string;
wenzelm@38150
    24
type version_id = string;
wenzelm@38150
    25
wenzelm@38150
    26
val no_id = "";
wenzelm@38150
    27
wenzelm@38150
    28
wenzelm@38150
    29
(* edits *)
wenzelm@38150
    30
wenzelm@38150
    31
type edit =
wenzelm@38150
    32
  string *  (*node name*)
wenzelm@38150
    33
  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
wenzelm@38150
    34
wenzelm@38150
    35
end;
wenzelm@38150
    36