diff -r 3c380380beac -r 67fc24df3721 src/Pure/PIDE/document.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document.ML	Thu Aug 05 14:35:35 2010 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/PIDE/document.ML
+    Author:     Makarius
+
+Document as collection of named nodes, each consisting of an editable
+list of commands.
+*)
+
+signature DOCUMENT =
+sig
+  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
+end;
+
+structure Document: DOCUMENT =
+struct
+
+(* 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*)
+
+end;
+