author wenzelm
Thu, 05 Aug 2010 14:35:35 +0200
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;

(*  Title:      Pure/PIDE/document.ML
    Author:     Makarius

Document as collection of named nodes, each consisting of an editable
list of commands.

signature DOCUMENT =
  type state_id = string
  type command_id = string
  type version_id = string
  val no_id: string
  type edit = string * ((command_id * command_id option) list) option

structure Document: DOCUMENT =

(* unique identifiers *)

type state_id = string;
type command_id = string;
type version_id = string;

val no_id = "";

(* edits *)

type edit =
  string *  (*node name*)
  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)