# HG changeset patch
# User blanchet
# Date 1282057291 -7200
# Node ID 8a7ff1c257737fdbebfe0e3873c95e432559307b
# Parent  1f51486da674f8467a5d436d42ae14f9c089b43a# Parent  f7e51d981a9fd296506359b039bdcc32f3e50f33
merged

diff -r f7e51d981a9f -r 8a7ff1c25773 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Aug 17 16:49:51 2010 +0200
+++ b/CONTRIBUTORS	Tue Aug 17 17:01:31 2010 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* July 2010: Florian Haftmann, TUM
+  Reworking and extension of the Isabelle/HOL framework.
+
 
 Contributions to Isabelle2009-2
 --------------------------------------
diff -r f7e51d981a9f -r 8a7ff1c25773 NEWS
--- a/NEWS	Tue Aug 17 16:49:51 2010 +0200
+++ b/NEWS	Tue Aug 17 17:01:31 2010 +0200
@@ -35,11 +35,17 @@
 
 *** HOL ***
 
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
 * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
 in Library/State_Monad has been changed to avoid ambiguities.
 INCOMPATIBILITY.
 
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
 to standard output.  INCOMPATIBILITY.
 
 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
 INCOMPATIBILITY.
 
 * Inductive package: offers new command "inductive_simps" to automatically
-  derive instantiated and simplified equations for inductive predicates,
-  similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
 
 
 *** ML ***
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/Foundations.thy
--- a/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 17:01:31 2010 +0200
@@ -7,7 +7,6 @@
 subsection {* Code generator architecture \label{sec:architecture} *}
 
 text {*
-
   The code generator is actually a framework consisting of different
   components which can be customised individually.
 
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 17:01:31 2010 +0200
@@ -70,23 +70,17 @@
 text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
 
 
-subsection {* Datatypes \label{sec:datatypes} *}
+subsection {* Datatype refinement *}
 
 text {*
-  Conceptually, any datatype is spanned by a set of
-  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
-  "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
-  @{text "\<tau>"}.  The HOL datatype package by default registers any new
-  datatype in the table of datatypes, which may be inspected using the
-  @{command print_codesetup} command.
-
-  In some cases, it is appropriate to alter or extend this table.  As
-  an example, we will develop an alternative representation of the
-  queue example given in \secref{sec:queue_example}.  The amortised
-  representation is convenient for generating code but exposes its
-  \qt{implementation} details, which may be cumbersome when proving
-  theorems about it.  Therefore, here is a simple, straightforward
-  representation of queues:
+  Selecting specific code equations \emph{and} datatype constructors
+  leads to datatype refinement.  As an example, we will develop an
+  alternative representation of the queue example given in
+  \secref{sec:queue_example}.  The amortised representation is
+  convenient for generating code but exposes its \qt{implementation}
+  details, which may be cumbersome when proving theorems about it.
+  Therefore, here is a simple, straightforward representation of
+  queues:
 *}
 
 datatype %quote 'a queue = Queue "'a list"
@@ -115,7 +109,18 @@
   \noindent Here we define a \qt{constructor} @{const "AQueue"} which
   is defined in terms of @{text "Queue"} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
-  to be.  Equipped with this, we are able to prove the following equations
+  to be.
+
+  The prerequisite for datatype constructors is only syntactical: a
+  constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+  "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+  @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype.  The
+  HOL datatype package by default registers any new datatype with its
+  constructors, but this may be changed using @{command
+  code_datatype}; the currently chosen constructors can be inspected
+  using the @{command print_codesetup} command.
+
+  Equipped with this, we are able to prove the following equations
   for our primitive queue operations which \qt{implement} the simple
   queues in an amortised fashion:
 *}
@@ -151,28 +156,21 @@
 text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
 
 text {*
-  \noindent From this example, it can be glimpsed that using own
-  constructor sets is a little delicate since it changes the set of
-  valid patterns for values of that type.  Without going into much
-  detail, here some practical hints:
-
-  \begin{itemize}
-
-    \item When changing the constructor set for datatypes, take care
-      to provide alternative equations for the @{text case} combinator.
+  The same techniques can also be applied to types which are not
+  specified as datatypes, e.g.~type @{typ int} is originally specified
+  as quotient type by means of @{command typedef}, but for code
+  generation constants allowing construction of binary numeral values
+  are used as constructors for @{typ int}.
 
-    \item Values in the target language need not to be normalised --
-      different values in the target language may represent the same
-      value in the logic.
+  This approach however fails if the representation of a type demands
+  invariants; this issue is discussed in the next section.
+*}
+
 
-    \item Usually, a good methodology to deal with the subtleties of
-      pattern matching is to see the type as an abstract type: provide
-      a set of operations which operate on the concrete representation
-      of the type, and derive further operations by combinations of
-      these primitive ones, without relying on a particular
-      representation.
+subsection {* Datatype refinement involving invariants *}
 
-  \end{itemize}
+text {*
+  FIXME
 *}
 
 end
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 17:01:31 2010 +0200
@@ -1,5 +1,5 @@
 theory Setup
-imports Complex_Main
+imports Complex_Main More_List
 uses
   "../../antiquote_setup.ML"
   "../../more_antiquote.ML"
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 17:01:31 2010 +0200
@@ -141,7 +141,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
 \hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
 \hspace*{0pt}\\
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 17:01:31 2010 +0200
@@ -191,24 +191,19 @@
 %
 \endisadelimquote
 %
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+\isamarkupsubsection{Datatype refinement%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Conceptually, any datatype is spanned by a set of
-  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
-  \isa{{\isasymtau}}.  The HOL datatype package by default registers any new
-  datatype in the table of datatypes, which may be inspected using the
-  \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
-
-  In some cases, it is appropriate to alter or extend this table.  As
-  an example, we will develop an alternative representation of the
-  queue example given in \secref{sec:queue_example}.  The amortised
-  representation is convenient for generating code but exposes its
-  \qt{implementation} details, which may be cumbersome when proving
-  theorems about it.  Therefore, here is a simple, straightforward
-  representation of queues:%
+Selecting specific code equations \emph{and} datatype constructors
+  leads to datatype refinement.  As an example, we will develop an
+  alternative representation of the queue example given in
+  \secref{sec:queue_example}.  The amortised representation is
+  convenient for generating code but exposes its \qt{implementation}
+  details, which may be cumbersome when proving theorems about it.
+  Therefore, here is a simple, straightforward representation of
+  queues:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -267,7 +262,16 @@
 \noindent Here we define a \qt{constructor} \isa{AQueue} which
   is defined in terms of \isa{Queue} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
-  to be.  Equipped with this, we are able to prove the following equations
+  to be.
+
+  The prerequisite for datatype constructors is only syntactical: a
+  constructor must be of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
+  \isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype.  The
+  HOL datatype package by default registers any new datatype with its
+  constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+  using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+  Equipped with this, we are able to prove the following equations
   for our primitive queue operations which \qt{implement} the simple
   queues in an amortised fashion:%
 \end{isamarkuptext}%
@@ -347,7 +351,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
 \hspace*{0pt} ~val null :~'a list -> bool\\
 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
@@ -356,10 +361,12 @@
 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun null [] = true\\
 \hspace*{0pt} ~| null (x ::~xs) = false;\\
@@ -387,28 +394,23 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent From this example, it can be glimpsed that using own
-  constructor sets is a little delicate since it changes the set of
-  valid patterns for values of that type.  Without going into much
-  detail, here some practical hints:
-
-  \begin{itemize}
-
-    \item When changing the constructor set for datatypes, take care
-      to provide alternative equations for the \isa{case} combinator.
+The same techniques can also be applied to types which are not
+  specified as datatypes, e.g.~type \isa{int} is originally specified
+  as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+  generation constants allowing construction of binary numeral values
+  are used as constructors for \isa{int}.
 
-    \item Values in the target language need not to be normalised --
-      different values in the target language may represent the same
-      value in the logic.
-
-    \item Usually, a good methodology to deal with the subtleties of
-      pattern matching is to see the type as an abstract type: provide
-      a set of operations which operate on the concrete representation
-      of the type, and derive further operations by combinations of
-      these primitive ones, without relying on a particular
-      representation.
-
-  \end{itemize}%
+  This approach however fails if the representation of a type demands
+  invariants; this issue is discussed in the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatype refinement involving invariants%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/Codegen/Thy/examples/example.ML
--- a/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -1,5 +1,6 @@
 structure Example : sig
-  val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+  val id : 'a -> 'a
+  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val rev : 'a list -> 'a list
   datatype 'a queue = AQueue of 'a list * 'a list
   val empty : 'a queue
@@ -7,10 +8,12 @@
   val enqueue : 'a -> 'a queue -> 'a queue
 end = struct
 
-fun foldl f a [] = a
-  | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
 
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+  | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
 
 datatype 'a queue = AQueue of 'a list * 'a list;
 
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 17:01:31 2010 +0200
@@ -1018,7 +1018,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code' ( 'del' ) ?
+    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
     'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
   declaration.
 
   \item @{attribute (HOL) code} explicitly selects (or with option
-  ``@{text "del"}'' deselects) a code equation for code
-  generation.  Usually packages introducing code equations provide
-  a reasonable default setup for selection.
+  ``@{text "del"}'' deselects) a code equation for code generation.
+  Usually packages introducing code equations provide a reasonable
+  default setup for selection.  Variants @{text "code abstype"} and
+  @{text "code abstract"} declare abstract datatype certificates or
+  code equations on abstract datatype representations respectively.
 
   \item @{command (HOL) "code_abort"} declares constants which are not
   required to have a definition by means of code equations; if
diff -r f7e51d981a9f -r 8a7ff1c25773 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 16:49:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 17:01:31 2010 +0200
@@ -1034,7 +1034,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code' ( 'del' ) ?
+    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
     'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
   declaration.
 
   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
-  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
-  generation.  Usually packages introducing code equations provide
-  a reasonable default setup for selection.
+  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+  Usually packages introducing code equations provide a reasonable
+  default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+  \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+  code equations on abstract datatype representations respectively.
 
   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
   required to have a definition by means of code equations; if
diff -r f7e51d981a9f -r 8a7ff1c25773 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -8,7 +8,9 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+    OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+    MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/General/linear_set.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -0,0 +1,142 @@
+(*  Title:      Pure/General/linear_set.ML
+    Author:     Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*)
+
+signature LINEAR_SET =
+sig
+  type key
+  type 'a T
+  exception DUPLICATE of key
+  exception UNDEFINED of key
+  exception NEXT_UNDEFINED of key option
+  val empty: 'a T
+  val is_empty: 'a T -> bool
+  val defined: 'a T -> key -> bool
+  val lookup: 'a T -> key -> 'a option
+  val update: key * 'a -> 'a T -> 'a T
+  val fold: key option ->
+    ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
+  val get_first: key option ->
+    ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+  val get_after: 'a T -> key option -> key option
+  val insert_after: key option -> key * 'a -> 'a T -> 'a T
+  val delete_after: key option -> 'a T -> 'a T
+end;
+
+functor Linear_Set(Key: KEY): LINEAR_SET =
+struct
+
+(* type key *)
+
+type key = Key.key;
+structure Table = Table(Key);
+
+exception DUPLICATE of key;
+exception UNDEFINED of key;
+exception NEXT_UNDEFINED of key option;
+
+
+(* raw entries *)
+
+fun the_entry entries key =
+  (case Table.lookup entries key of
+    NONE => raise UNDEFINED key
+  | SOME entry => entry);
+
+fun next_entry entries key = snd (the_entry entries key);
+
+fun put_entry entry entries = Table.update entry entries;
+
+fun new_entry entry entries = Table.update_new entry entries
+  handle Table.DUP key => raise DUPLICATE key;
+
+fun del_entry key entries = Table.delete_safe key entries;
+
+
+(* set representation and basic operations *)
+
+datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table};
+
+fun make_set (start, entries) = Set {start = start, entries = entries};
+fun map_set f (Set {start, entries}) = make_set (f (start, entries));
+
+fun start_of (Set {start, ...}) = start;
+fun entries_of (Set {entries, ...}) = entries;
+
+val empty = Set {start = NONE, entries = Table.empty};
+fun is_empty set = is_none (start_of set);
+
+fun defined set key = Table.defined (entries_of set) key;
+
+fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+
+fun update (key, x) = map_set (fn (start, entries) =>
+  (start, put_entry (key, (x, next_entry entries key)) entries));
+
+
+(* iterate entries *)
+
+fun optional_start set NONE = start_of set
+  | optional_start _ some = some;
+
+fun fold opt_start f set =
+  let
+    val entries = entries_of set;
+    fun apply _ NONE y = y
+      | apply prev (SOME key) y =
+          let
+            val (x, next) = the_entry entries key;
+            val item = ((prev, key), x);
+          in apply (SOME key) next (f item y) end;
+  in apply NONE (optional_start set opt_start) end;
+
+fun get_first opt_start P set =
+  let
+    val entries = entries_of set;
+    fun first _ NONE = NONE
+      | first prev (SOME key) =
+          let
+            val (x, next) = the_entry entries key;
+            val item = ((prev, key), x);
+          in if P item then SOME item else first (SOME key) next end;
+  in first NONE (optional_start set opt_start) end;
+
+
+(* relative addressing *)
+
+fun get_after set hook =
+  (case hook of
+    NONE => start_of set
+  | SOME key => next_entry (entries_of set) key);
+
+fun insert_after hook (key, x) = map_set (fn (start, entries) =>
+  (case hook of
+    NONE => (SOME key, new_entry (key, (x, start)) entries)
+  | SOME key1 =>
+      let
+        val (x1, next) = the_entry entries key1;
+        val entries' = entries
+          |> put_entry (key1, (x1, SOME key))
+          |> new_entry (key, (x, next));
+      in (start, entries') end));
+
+fun delete_after hook set = set |> map_set (fn (start, entries) =>
+  (case hook of
+    NONE =>
+      (case start of
+        NONE => raise NEXT_UNDEFINED NONE
+      | SOME key1 => (next_entry entries key1, del_entry key1 entries))
+  | SOME key1 =>
+      (case the_entry entries key1 of
+        (_, NONE) => raise NEXT_UNDEFINED (SOME key1)
+      | (x1, SOME key2) =>
+          let
+            val entries' = entries
+              |> put_entry (key1, (x1, next_entry entries key2))
+              |> del_entry key2;
+          in (start, entries') end)));
+
+end;
+
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Tue Aug 17 17:01:31 2010 +0200
@@ -25,8 +25,9 @@
   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
   override def empty[A] = new Linear_Set[A]
 
-  class Duplicate(s: String) extends Exception(s)
-  class Undefined(s: String) extends Exception(s)
+  class Duplicate[A](x: A) extends Exception
+  class Undefined[A](x: A) extends Exception
+  class Next_Undefined[A](x: Option[A]) extends Exception
 }
 
 
@@ -43,19 +44,22 @@
   protected val rep = Linear_Set.empty_rep[A]
 
 
-  /* auxiliary operations */
+  /* relative addressing */
 
+  // FIXME check definedness??
   def next(elem: A): Option[A] = rep.nexts.get(elem)
   def prev(elem: A): Option[A] = rep.prevs.get(elem)
 
   def get_after(hook: Option[A]): Option[A] =
     hook match {
       case None => rep.start
-      case Some(elem) => next(elem)
+      case Some(elem) =>
+        if (!contains(elem)) throw new Linear_Set.Undefined(elem)
+        next(elem)
     }
 
   def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
-    if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
+    if (contains(elem)) throw new Linear_Set.Duplicate(elem)
     else
       hook match {
         case None =>
@@ -66,7 +70,7 @@
                 rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
-          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
           else
             rep.nexts.get(elem1) match {
               case None =>
@@ -83,7 +87,7 @@
     hook match {
       case None =>
         rep.start match {
-          case None => throw new Linear_Set.Undefined("")
+          case None => throw new Linear_Set.Next_Undefined[A](None)
           case Some(elem1) =>
             rep.nexts.get(elem1) match {
               case None => empty
@@ -92,10 +96,10 @@
             }
         }
       case Some(elem1) =>
-        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
         else
           rep.nexts.get(elem1) match {
-            case None => throw new Linear_Set.Undefined("")
+            case None => throw new Linear_Set.Next_Undefined(Some(elem1))
             case Some(elem2) =>
               rep.nexts.get(elem2) match {
                 case None =>
@@ -153,15 +157,15 @@
 
   def iterator(elem: A): Iterator[A] =
     if (contains(elem)) make_iterator(Some(elem), rep.nexts)
-    else throw new Linear_Set.Undefined(elem.toString)
+    else throw new Linear_Set.Undefined(elem)
 
   def reverse_iterator(elem: A): Iterator[A] =
     if (contains(elem)) make_iterator(Some(elem), rep.prevs)
-    else throw new Linear_Set.Undefined(elem.toString)
+    else throw new Linear_Set.Undefined(elem)
 
   def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
 
   def - (elem: A): Linear_Set[A] =
-    if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+    if (!contains(elem)) throw new Linear_Set.Undefined(elem)
     else delete_after(prev(elem))
 }
\ No newline at end of file
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/IsaMakefile	Tue Aug 17 17:01:31 2010 +0200
@@ -80,6 +80,7 @@
   General/graph.ML					\
   General/heap.ML					\
   General/integer.ML					\
+  General/linear_set.ML					\
   General/long_name.ML					\
   General/markup.ML					\
   General/name_space.ML					\
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -15,7 +15,7 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  type edit = string * ((command_id * command_id option) list) option
+  type edit = string * ((command_id option * command_id option) list) option
   type state
   val init_state: state
   val define_command: command_id -> string -> state -> state
@@ -55,82 +55,43 @@
 
 (** document structure **)
 
-abstype entry = Entry of {next: command_id option, exec: exec_id option}
-  and node = Node of entry Inttab.table  (*unique entries indexed by command_id, start with no_id*)
+structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+
+abstype node = Node of exec_id option Entries.T  (*command entries with excecutions*)
   and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-
-(* command entries *)
-
-fun make_entry next exec = Entry {next = next, exec = exec};
-
-fun the_entry (Node entries) (id: command_id) =
-  (case Inttab.lookup entries id of
-    NONE => err_undef "command entry" id
-  | SOME (Entry entry) => entry);
+val empty_node = Node Entries.empty;
+val empty_version = Version Graph.empty;
 
-fun put_entry (id: command_id, entry: entry) (Node entries) =
-  Node (Inttab.update (id, entry) entries);
-
-fun put_entry_exec (id: command_id) exec node =
-  let val {next, ...} = the_entry node id
-  in put_entry (id, make_entry next exec) node end;
-
-fun reset_entry_exec id = put_entry_exec id NONE;
-fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
+fun fold_entries start f (Node entries) = Entries.fold start f entries;
+fun first_entry start P (Node entries) = Entries.get_first start P entries;
 
 
-(* iterate entries *)
-
-fun fold_entries id0 f (node as Node entries) =
-  let
-    fun apply NONE x = x
-      | apply (SOME id) x =
-          let val entry = the_entry node id
-          in apply (#next entry) (f (id, entry) x) end;
-  in if Inttab.defined entries id0 then apply (SOME id0) else I end;
-
-fun first_entry P node =
-  let
-    fun first _ NONE = NONE
-      | first prev (SOME id) =
-          let val entry = the_entry node id
-          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
-  in first NONE (SOME no_id) end;
-
-
-(* modify entries *)
-
-fun insert_after (id: command_id) (id2: command_id) node =
-  let val {next, exec} = the_entry node id in
-    node
-    |> put_entry (id, make_entry (SOME id2) exec)
-    |> put_entry (id2, make_entry next NONE)
-  end;
-
-fun delete_after (id: command_id) node =
-  let val {next, exec} = the_entry node id in
-    (case next of
-      NONE => error ("No next entry to delete: " ^ print_id id)
-    | SOME id2 =>
-        node |>
-          (case #next (the_entry node id2) of
-            NONE => put_entry (id, make_entry NONE exec)
-          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
-  end;
-
-
-(* node edits *)
+(* node edits and associated executions *)
 
 type edit =
-  string *  (*node name*)
-  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
+  string *
+  (*NONE: remove node, SOME: insert/remove commands*)
+  ((command_id option * command_id option) list) option;
+
+fun the_entry (Node entries) id =
+  (case Entries.lookup entries id of
+    NONE => err_undef "command entry" id
+  | SOME entry => entry);
 
-val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
+fun update_entry (id, exec_id) (Node entries) =
+  Node (Entries.update (id, SOME exec_id) entries);
 
-fun edit_node (id, SOME id2) = insert_after id id2
-  | edit_node (id, NONE) = delete_after id;
+fun reset_after id entries =
+  (case Entries.get_after entries id of
+    NONE => entries
+  | SOME next => Entries.update (next, NONE) entries);
+
+fun edit_node (hook, SOME id2) (Node entries) =
+      Node (Entries.insert_after hook (id2, NONE) entries)
+  | edit_node (hook, NONE) (Node entries) =
+      Node (entries |> Entries.delete_after hook |> reset_after hook);
 
 
 (* version operations *)
@@ -138,19 +99,18 @@
 fun nodes_of (Version nodes) = nodes;
 val node_names_of = Graph.keys o nodes_of;
 
+fun get_node version name = Graph.get_node (nodes_of version) name
+  handle Graph.UNDEF _ => empty_node;
+
 fun edit_nodes (name, SOME edits) (Version nodes) =
       Version (nodes
         |> Graph.default_node (name, empty_node)
         |> Graph.map_node name (fold edit_node edits))
-  | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
-
-val empty_version = Version Graph.empty;
-
-fun the_node version name =
-  Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
+  | edit_nodes (name, NONE) (Version nodes) =
+      Version (Graph.del_node name nodes);
 
 fun put_node name node (Version nodes) =
-  Version (Graph.map_node name (K node) nodes);  (* FIXME Graph.UNDEF !? *)
+  Version (Graph.map_node name (K node) nodes);
 
 end;
 
@@ -238,22 +198,22 @@
 
 local
 
-fun is_changed node' (id, {next = _, exec}) =
+fun is_changed node' ((_, id), exec) =
   (case try (the_entry node') id of
     NONE => true
-  | SOME {next = _, exec = exec'} => exec' <> exec);
+  | SOME exec' => exec' <> exec);
 
 fun new_exec name (id: command_id) (exec_id, updates, state) =
   let
     val exec = the_exec state exec_id;
     val exec_id' = new_id ();
-    val tr = the_command state id;
+    val future_tr = the_command state id;
     val exec' =
       Lazy.lazy (fn () =>
         (case Lazy.force exec of
           NONE => NONE
         | SOME st =>
-            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
+            let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
             in Toplevel.run_command name exec_tr st end));
     val state' = define_exec exec_id' exec' state;
   in (exec_id', (id, exec_id') :: updates, state') end;
@@ -266,15 +226,18 @@
     val new_version = fold edit_nodes edits old_version;
 
     fun update_node name (rev_updates, version, st) =
-      let val node = the_node version name in
-        (case first_entry (is_changed (the_node old_version name)) node of
+      let val node = get_node version name in
+        (case first_entry NONE (is_changed (get_node old_version name)) node of
           NONE => (rev_updates, version, st)
-        | SOME (prev, id, _) =>
+        | SOME ((prev, id), _) =>
             let
-              val prev_exec = the (#exec (the_entry node (the prev)));
+              val prev_exec =
+                (case prev of
+                  NONE => no_id
+                | SOME prev_id => the_default no_id (the_entry node prev_id));
               val (_, rev_upds, st') =
-                fold_entries id (new_exec name o #1) node (prev_exec, [], st);
-              val node' = fold set_entry_exec rev_upds node;
+                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
+              val node' = fold update_entry rev_upds node;
             in (rev_upds @ rev_updates, put_node name node' version, st') end)
       end;
 
@@ -306,8 +269,8 @@
         node_names_of version |> map (fn name =>
           Future.fork_pri 1 (fn () =>
             (await_cancellation ();
-              fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
-                (the_node version name) ())));
+              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+                (get_node version name) ())));
     in (versions, commands, execs, execution') end);
 
 end;
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -42,6 +42,7 @@
 use "General/ord_list.ML";
 use "General/balanced_tree.ML";
 use "General/graph.ML";
+use "General/linear_set.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/name_space.ML";
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/System/isar_document.ML
--- a/src/Pure/System/isar_document.ML	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/System/isar_document.ML	Tue Aug 17 17:01:31 2010 +0200
@@ -21,10 +21,14 @@
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;
         val edits =
-          XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
-            (XML_Data.dest_option (XML_Data.dest_list
-                (XML_Data.dest_pair XML_Data.dest_int
-                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+          XML_Data.dest_list
+            (XML_Data.dest_pair
+              XML_Data.dest_string
+              (XML_Data.dest_option
+                (XML_Data.dest_list
+                  (XML_Data.dest_pair
+                    (XML_Data.dest_option XML_Data.dest_int)
+                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
 
       val (updates, state') = Document.edit old_id new_id edits state;
       val _ =
diff -r f7e51d981a9f -r 8a7ff1c25773 src/Pure/System/isar_document.scala
--- a/src/Pure/System/isar_document.scala	Tue Aug 17 16:49:51 2010 +0200
+++ b/src/Pure/System/isar_document.scala	Tue Aug 17 17:01:31 2010 +0200
@@ -51,14 +51,13 @@
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
       edits: List[Document.Edit[Document.Command_ID]])
   {
-    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
-      XML_Data.make_long(id1 getOrElse Document.NO_ID)
-
     val arg =
       XML_Data.make_list(
         XML_Data.make_pair(XML_Data.make_string)(
           XML_Data.make_option(XML_Data.make_list(
-              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
+              XML_Data.make_pair(
+                XML_Data.make_option(XML_Data.make_long))(
+                XML_Data.make_option(XML_Data.make_long))))))(edits)
 
     input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))