added functor Linear_Set, based on former adhoc structures in document.ML;
authorwenzelm
Tue Aug 17 15:10:49 2010 +0200 (2010-08-17 ago)
changeset 3844862d16c415019
parent 38447 f55e77f623ab
child 38449 2eb6bad282b1
added functor Linear_Set, based on former adhoc structures in document.ML;
Linear_Set.delete_after (ML): actually delete table entries;
Scala Linear_Set: clarified exceptions, according to ML version;
simplified Document.node using Linear_Set;
ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
src/Pure/General/linear_set.ML
src/Pure/General/linear_set.scala
src/Pure/IsaMakefile
src/Pure/PIDE/document.ML
src/Pure/ROOT.ML
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/linear_set.ML	Tue Aug 17 15:10:49 2010 +0200
     1.3 @@ -0,0 +1,142 @@
     1.4 +(*  Title:      Pure/General/linear_set.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Sets with canonical linear order, or immutable linked-lists.
     1.8 +*)
     1.9 +
    1.10 +signature LINEAR_SET =
    1.11 +sig
    1.12 +  type key
    1.13 +  type 'a T
    1.14 +  exception DUPLICATE of key
    1.15 +  exception UNDEFINED of key
    1.16 +  exception NEXT_UNDEFINED of key option
    1.17 +  val empty: 'a T
    1.18 +  val is_empty: 'a T -> bool
    1.19 +  val defined: 'a T -> key -> bool
    1.20 +  val lookup: 'a T -> key -> 'a option
    1.21 +  val update: key * 'a -> 'a T -> 'a T
    1.22 +  val fold: key option ->
    1.23 +    ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
    1.24 +  val get_first: key option ->
    1.25 +    ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
    1.26 +  val get_after: 'a T -> key option -> key option
    1.27 +  val insert_after: key option -> key * 'a -> 'a T -> 'a T
    1.28 +  val delete_after: key option -> 'a T -> 'a T
    1.29 +end;
    1.30 +
    1.31 +functor Linear_Set(Key: KEY): LINEAR_SET =
    1.32 +struct
    1.33 +
    1.34 +(* type key *)
    1.35 +
    1.36 +type key = Key.key;
    1.37 +structure Table = Table(Key);
    1.38 +
    1.39 +exception DUPLICATE of key;
    1.40 +exception UNDEFINED of key;
    1.41 +exception NEXT_UNDEFINED of key option;
    1.42 +
    1.43 +
    1.44 +(* raw entries *)
    1.45 +
    1.46 +fun the_entry entries key =
    1.47 +  (case Table.lookup entries key of
    1.48 +    NONE => raise UNDEFINED key
    1.49 +  | SOME entry => entry);
    1.50 +
    1.51 +fun next_entry entries key = snd (the_entry entries key);
    1.52 +
    1.53 +fun put_entry entry entries = Table.update entry entries;
    1.54 +
    1.55 +fun new_entry entry entries = Table.update_new entry entries
    1.56 +  handle Table.DUP key => raise DUPLICATE key;
    1.57 +
    1.58 +fun del_entry key entries = Table.delete_safe key entries;
    1.59 +
    1.60 +
    1.61 +(* set representation and basic operations *)
    1.62 +
    1.63 +datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table};
    1.64 +
    1.65 +fun make_set (start, entries) = Set {start = start, entries = entries};
    1.66 +fun map_set f (Set {start, entries}) = make_set (f (start, entries));
    1.67 +
    1.68 +fun start_of (Set {start, ...}) = start;
    1.69 +fun entries_of (Set {entries, ...}) = entries;
    1.70 +
    1.71 +val empty = Set {start = NONE, entries = Table.empty};
    1.72 +fun is_empty set = is_none (start_of set);
    1.73 +
    1.74 +fun defined set key = Table.defined (entries_of set) key;
    1.75 +
    1.76 +fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
    1.77 +
    1.78 +fun update (key, x) = map_set (fn (start, entries) =>
    1.79 +  (start, put_entry (key, (x, next_entry entries key)) entries));
    1.80 +
    1.81 +
    1.82 +(* iterate entries *)
    1.83 +
    1.84 +fun optional_start set NONE = start_of set
    1.85 +  | optional_start _ some = some;
    1.86 +
    1.87 +fun fold opt_start f set =
    1.88 +  let
    1.89 +    val entries = entries_of set;
    1.90 +    fun apply _ NONE y = y
    1.91 +      | apply prev (SOME key) y =
    1.92 +          let
    1.93 +            val (x, next) = the_entry entries key;
    1.94 +            val item = ((prev, key), x);
    1.95 +          in apply (SOME key) next (f item y) end;
    1.96 +  in apply NONE (optional_start set opt_start) end;
    1.97 +
    1.98 +fun get_first opt_start P set =
    1.99 +  let
   1.100 +    val entries = entries_of set;
   1.101 +    fun first _ NONE = NONE
   1.102 +      | first prev (SOME key) =
   1.103 +          let
   1.104 +            val (x, next) = the_entry entries key;
   1.105 +            val item = ((prev, key), x);
   1.106 +          in if P item then SOME item else first (SOME key) next end;
   1.107 +  in first NONE (optional_start set opt_start) end;
   1.108 +
   1.109 +
   1.110 +(* relative addressing *)
   1.111 +
   1.112 +fun get_after set hook =
   1.113 +  (case hook of
   1.114 +    NONE => start_of set
   1.115 +  | SOME key => next_entry (entries_of set) key);
   1.116 +
   1.117 +fun insert_after hook (key, x) = map_set (fn (start, entries) =>
   1.118 +  (case hook of
   1.119 +    NONE => (SOME key, new_entry (key, (x, start)) entries)
   1.120 +  | SOME key1 =>
   1.121 +      let
   1.122 +        val (x1, next) = the_entry entries key1;
   1.123 +        val entries' = entries
   1.124 +          |> put_entry (key1, (x1, SOME key))
   1.125 +          |> new_entry (key, (x, next));
   1.126 +      in (start, entries') end));
   1.127 +
   1.128 +fun delete_after hook set = set |> map_set (fn (start, entries) =>
   1.129 +  (case hook of
   1.130 +    NONE =>
   1.131 +      (case start of
   1.132 +        NONE => raise NEXT_UNDEFINED NONE
   1.133 +      | SOME key1 => (next_entry entries key1, del_entry key1 entries))
   1.134 +  | SOME key1 =>
   1.135 +      (case the_entry entries key1 of
   1.136 +        (_, NONE) => raise NEXT_UNDEFINED (SOME key1)
   1.137 +      | (x1, SOME key2) =>
   1.138 +          let
   1.139 +            val entries' = entries
   1.140 +              |> put_entry (key1, (x1, next_entry entries key2))
   1.141 +              |> del_entry key2;
   1.142 +          in (start, entries') end)));
   1.143 +
   1.144 +end;
   1.145 +
     2.1 --- a/src/Pure/General/linear_set.scala	Mon Aug 16 22:56:28 2010 +0200
     2.2 +++ b/src/Pure/General/linear_set.scala	Tue Aug 17 15:10:49 2010 +0200
     2.3 @@ -25,8 +25,9 @@
     2.4    implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
     2.5    override def empty[A] = new Linear_Set[A]
     2.6  
     2.7 -  class Duplicate(s: String) extends Exception(s)
     2.8 -  class Undefined(s: String) extends Exception(s)
     2.9 +  class Duplicate[A](x: A) extends Exception
    2.10 +  class Undefined[A](x: A) extends Exception
    2.11 +  class Next_Undefined[A](x: Option[A]) extends Exception
    2.12  }
    2.13  
    2.14  
    2.15 @@ -43,19 +44,22 @@
    2.16    protected val rep = Linear_Set.empty_rep[A]
    2.17  
    2.18  
    2.19 -  /* auxiliary operations */
    2.20 +  /* relative addressing */
    2.21  
    2.22 +  // FIXME check definedness??
    2.23    def next(elem: A): Option[A] = rep.nexts.get(elem)
    2.24    def prev(elem: A): Option[A] = rep.prevs.get(elem)
    2.25  
    2.26    def get_after(hook: Option[A]): Option[A] =
    2.27      hook match {
    2.28        case None => rep.start
    2.29 -      case Some(elem) => next(elem)
    2.30 +      case Some(elem) =>
    2.31 +        if (!contains(elem)) throw new Linear_Set.Undefined(elem)
    2.32 +        next(elem)
    2.33      }
    2.34  
    2.35    def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
    2.36 -    if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
    2.37 +    if (contains(elem)) throw new Linear_Set.Duplicate(elem)
    2.38      else
    2.39        hook match {
    2.40          case None =>
    2.41 @@ -66,7 +70,7 @@
    2.42                  rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
    2.43            }
    2.44          case Some(elem1) =>
    2.45 -          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
    2.46 +          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
    2.47            else
    2.48              rep.nexts.get(elem1) match {
    2.49                case None =>
    2.50 @@ -83,7 +87,7 @@
    2.51      hook match {
    2.52        case None =>
    2.53          rep.start match {
    2.54 -          case None => throw new Linear_Set.Undefined("")
    2.55 +          case None => throw new Linear_Set.Next_Undefined[A](None)
    2.56            case Some(elem1) =>
    2.57              rep.nexts.get(elem1) match {
    2.58                case None => empty
    2.59 @@ -92,10 +96,10 @@
    2.60              }
    2.61          }
    2.62        case Some(elem1) =>
    2.63 -        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
    2.64 +        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
    2.65          else
    2.66            rep.nexts.get(elem1) match {
    2.67 -            case None => throw new Linear_Set.Undefined("")
    2.68 +            case None => throw new Linear_Set.Next_Undefined(Some(elem1))
    2.69              case Some(elem2) =>
    2.70                rep.nexts.get(elem2) match {
    2.71                  case None =>
    2.72 @@ -153,15 +157,15 @@
    2.73  
    2.74    def iterator(elem: A): Iterator[A] =
    2.75      if (contains(elem)) make_iterator(Some(elem), rep.nexts)
    2.76 -    else throw new Linear_Set.Undefined(elem.toString)
    2.77 +    else throw new Linear_Set.Undefined(elem)
    2.78  
    2.79    def reverse_iterator(elem: A): Iterator[A] =
    2.80      if (contains(elem)) make_iterator(Some(elem), rep.prevs)
    2.81 -    else throw new Linear_Set.Undefined(elem.toString)
    2.82 +    else throw new Linear_Set.Undefined(elem)
    2.83  
    2.84    def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
    2.85  
    2.86    def - (elem: A): Linear_Set[A] =
    2.87 -    if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
    2.88 +    if (!contains(elem)) throw new Linear_Set.Undefined(elem)
    2.89      else delete_after(prev(elem))
    2.90  }
    2.91 \ No newline at end of file
     3.1 --- a/src/Pure/IsaMakefile	Mon Aug 16 22:56:28 2010 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Tue Aug 17 15:10:49 2010 +0200
     3.3 @@ -80,6 +80,7 @@
     3.4    General/graph.ML					\
     3.5    General/heap.ML					\
     3.6    General/integer.ML					\
     3.7 +  General/linear_set.ML					\
     3.8    General/long_name.ML					\
     3.9    General/markup.ML					\
    3.10    General/name_space.ML					\
     4.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 16 22:56:28 2010 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 17 15:10:49 2010 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4    val new_id: unit -> id
     4.5    val parse_id: string -> id
     4.6    val print_id: id -> string
     4.7 -  type edit = string * ((command_id * command_id option) list) option
     4.8 +  type edit = string * ((command_id option * command_id option) list) option
     4.9    type state
    4.10    val init_state: state
    4.11    val define_command: command_id -> string -> state -> state
    4.12 @@ -55,82 +55,43 @@
    4.13  
    4.14  (** document structure **)
    4.15  
    4.16 -abstype entry = Entry of {next: command_id option, exec: exec_id option}
    4.17 -  and node = Node of entry Inttab.table  (*unique entries indexed by command_id, start with no_id*)
    4.18 +structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    4.19 +
    4.20 +abstype node = Node of exec_id option Entries.T  (*command entries with excecutions*)
    4.21    and version = Version of node Graph.T  (*development graph wrt. static imports*)
    4.22  with
    4.23  
    4.24 -
    4.25 -(* command entries *)
    4.26 -
    4.27 -fun make_entry next exec = Entry {next = next, exec = exec};
    4.28 -
    4.29 -fun the_entry (Node entries) (id: command_id) =
    4.30 -  (case Inttab.lookup entries id of
    4.31 -    NONE => err_undef "command entry" id
    4.32 -  | SOME (Entry entry) => entry);
    4.33 +val empty_node = Node Entries.empty;
    4.34 +val empty_version = Version Graph.empty;
    4.35  
    4.36 -fun put_entry (id: command_id, entry: entry) (Node entries) =
    4.37 -  Node (Inttab.update (id, entry) entries);
    4.38 -
    4.39 -fun put_entry_exec (id: command_id) exec node =
    4.40 -  let val {next, ...} = the_entry node id
    4.41 -  in put_entry (id, make_entry next exec) node end;
    4.42 -
    4.43 -fun reset_entry_exec id = put_entry_exec id NONE;
    4.44 -fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    4.45 +fun fold_entries start f (Node entries) = Entries.fold start f entries;
    4.46 +fun first_entry start P (Node entries) = Entries.get_first start P entries;
    4.47  
    4.48  
    4.49 -(* iterate entries *)
    4.50 -
    4.51 -fun fold_entries id0 f (node as Node entries) =
    4.52 -  let
    4.53 -    fun apply NONE x = x
    4.54 -      | apply (SOME id) x =
    4.55 -          let val entry = the_entry node id
    4.56 -          in apply (#next entry) (f (id, entry) x) end;
    4.57 -  in if Inttab.defined entries id0 then apply (SOME id0) else I end;
    4.58 -
    4.59 -fun first_entry P node =
    4.60 -  let
    4.61 -    fun first _ NONE = NONE
    4.62 -      | first prev (SOME id) =
    4.63 -          let val entry = the_entry node id
    4.64 -          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    4.65 -  in first NONE (SOME no_id) end;
    4.66 -
    4.67 -
    4.68 -(* modify entries *)
    4.69 -
    4.70 -fun insert_after (id: command_id) (id2: command_id) node =
    4.71 -  let val {next, exec} = the_entry node id in
    4.72 -    node
    4.73 -    |> put_entry (id, make_entry (SOME id2) exec)
    4.74 -    |> put_entry (id2, make_entry next NONE)
    4.75 -  end;
    4.76 -
    4.77 -fun delete_after (id: command_id) node =
    4.78 -  let val {next, exec} = the_entry node id in
    4.79 -    (case next of
    4.80 -      NONE => error ("No next entry to delete: " ^ print_id id)
    4.81 -    | SOME id2 =>
    4.82 -        node |>
    4.83 -          (case #next (the_entry node id2) of
    4.84 -            NONE => put_entry (id, make_entry NONE exec)
    4.85 -          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    4.86 -  end;
    4.87 -
    4.88 -
    4.89 -(* node edits *)
    4.90 +(* node edits and associated executions *)
    4.91  
    4.92  type edit =
    4.93 -  string *  (*node name*)
    4.94 -  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
    4.95 +  string *
    4.96 +  (*NONE: remove node, SOME: insert/remove commands*)
    4.97 +  ((command_id option * command_id option) list) option;
    4.98 +
    4.99 +fun the_entry (Node entries) id =
   4.100 +  (case Entries.lookup entries id of
   4.101 +    NONE => err_undef "command entry" id
   4.102 +  | SOME entry => entry);
   4.103  
   4.104 -val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
   4.105 +fun update_entry (id, exec_id) (Node entries) =
   4.106 +  Node (Entries.update (id, SOME exec_id) entries);
   4.107  
   4.108 -fun edit_node (id, SOME id2) = insert_after id id2
   4.109 -  | edit_node (id, NONE) = delete_after id;
   4.110 +fun reset_after id entries =
   4.111 +  (case Entries.get_after entries id of
   4.112 +    NONE => entries
   4.113 +  | SOME next => Entries.update (next, NONE) entries);
   4.114 +
   4.115 +fun edit_node (hook, SOME id2) (Node entries) =
   4.116 +      Node (Entries.insert_after hook (id2, NONE) entries)
   4.117 +  | edit_node (hook, NONE) (Node entries) =
   4.118 +      Node (entries |> Entries.delete_after hook |> reset_after hook);
   4.119  
   4.120  
   4.121  (* version operations *)
   4.122 @@ -138,16 +99,15 @@
   4.123  fun nodes_of (Version nodes) = nodes;
   4.124  val node_names_of = Graph.keys o nodes_of;
   4.125  
   4.126 +fun get_node version name = Graph.get_node (nodes_of version) name
   4.127 +  handle Graph.UNDEF _ => empty_node;
   4.128 +
   4.129  fun edit_nodes (name, SOME edits) (Version nodes) =
   4.130        Version (nodes
   4.131          |> Graph.default_node (name, empty_node)
   4.132          |> Graph.map_node name (fold edit_node edits))
   4.133 -  | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
   4.134 -
   4.135 -val empty_version = Version Graph.empty;
   4.136 -
   4.137 -fun the_node version name =
   4.138 -  Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
   4.139 +  | edit_nodes (name, NONE) (Version nodes) =
   4.140 +      Version (Graph.del_node name nodes);  (* FIXME Graph.UNDEF !? *)
   4.141  
   4.142  fun put_node name node (Version nodes) =
   4.143    Version (Graph.map_node name (K node) nodes);  (* FIXME Graph.UNDEF !? *)
   4.144 @@ -173,8 +133,8 @@
   4.145  
   4.146  val init_state =
   4.147    make_state (Inttab.make [(no_id, empty_version)],
   4.148 -    Inttab.make [(no_id, Future.value Toplevel.empty)],
   4.149 -    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],
   4.150 +    Inttab.make [(no_id, Future.value Toplevel.empty)],          (* FIXME no_id !?? *)
   4.151 +    Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))],  (* FIXME no_id !?? *)
   4.152      []);
   4.153  
   4.154  
   4.155 @@ -238,10 +198,10 @@
   4.156  
   4.157  local
   4.158  
   4.159 -fun is_changed node' (id, {next = _, exec}) =
   4.160 +fun is_changed node' ((_, id), exec) =
   4.161    (case try (the_entry node') id of
   4.162      NONE => true
   4.163 -  | SOME {next = _, exec = exec'} => exec' <> exec);
   4.164 +  | SOME exec' => exec' <> exec);
   4.165  
   4.166  fun new_exec name (id: command_id) (exec_id, updates, state) =
   4.167    let
   4.168 @@ -266,15 +226,18 @@
   4.169      val new_version = fold edit_nodes edits old_version;
   4.170  
   4.171      fun update_node name (rev_updates, version, st) =
   4.172 -      let val node = the_node version name in
   4.173 -        (case first_entry (is_changed (the_node old_version name)) node of
   4.174 +      let val node = get_node version name in
   4.175 +        (case first_entry NONE (is_changed (get_node old_version name)) node of
   4.176            NONE => (rev_updates, version, st)
   4.177 -        | SOME (prev, id, _) =>
   4.178 +        | SOME ((prev, id), _) =>
   4.179              let
   4.180 -              val prev_exec = the (#exec (the_entry node (the prev)));
   4.181 +              val prev_exec =
   4.182 +                (case prev of
   4.183 +                  NONE => no_id
   4.184 +                | SOME prev_id => the_default no_id (the_entry node prev_id));
   4.185                val (_, rev_upds, st') =
   4.186 -                fold_entries id (new_exec name o #1) node (prev_exec, [], st);
   4.187 -              val node' = fold set_entry_exec rev_upds node;
   4.188 +                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   4.189 +              val node' = fold update_entry rev_upds node;
   4.190              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   4.191        end;
   4.192  
   4.193 @@ -306,8 +269,8 @@
   4.194          node_names_of version |> map (fn name =>
   4.195            Future.fork_pri 1 (fn () =>
   4.196              (await_cancellation ();
   4.197 -              fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   4.198 -                (the_node version name) ())));
   4.199 +              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   4.200 +                (get_node version name) ())));
   4.201      in (versions, commands, execs, execution') end);
   4.202  
   4.203  end;
     5.1 --- a/src/Pure/ROOT.ML	Mon Aug 16 22:56:28 2010 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Tue Aug 17 15:10:49 2010 +0200
     5.3 @@ -42,6 +42,7 @@
     5.4  use "General/ord_list.ML";
     5.5  use "General/balanced_tree.ML";
     5.6  use "General/graph.ML";
     5.7 +use "General/linear_set.ML";
     5.8  use "General/long_name.ML";
     5.9  use "General/binding.ML";
    5.10  use "General/name_space.ML";
     6.1 --- a/src/Pure/System/isar_document.ML	Mon Aug 16 22:56:28 2010 +0200
     6.2 +++ b/src/Pure/System/isar_document.ML	Tue Aug 17 15:10:49 2010 +0200
     6.3 @@ -21,10 +21,14 @@
     6.4          val old_id = Document.parse_id old_id_string;
     6.5          val new_id = Document.parse_id new_id_string;
     6.6          val edits =
     6.7 -          XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
     6.8 -            (XML_Data.dest_option (XML_Data.dest_list
     6.9 -                (XML_Data.dest_pair XML_Data.dest_int
    6.10 -                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    6.11 +          XML_Data.dest_list
    6.12 +            (XML_Data.dest_pair
    6.13 +              XML_Data.dest_string
    6.14 +              (XML_Data.dest_option
    6.15 +                (XML_Data.dest_list
    6.16 +                  (XML_Data.dest_pair
    6.17 +                    (XML_Data.dest_option XML_Data.dest_int)
    6.18 +                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    6.19  
    6.20        val (updates, state') = Document.edit old_id new_id edits state;
    6.21        val _ =
     7.1 --- a/src/Pure/System/isar_document.scala	Mon Aug 16 22:56:28 2010 +0200
     7.2 +++ b/src/Pure/System/isar_document.scala	Tue Aug 17 15:10:49 2010 +0200
     7.3 @@ -51,14 +51,13 @@
     7.4    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     7.5        edits: List[Document.Edit[Document.Command_ID]])
     7.6    {
     7.7 -    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
     7.8 -      XML_Data.make_long(id1 getOrElse Document.NO_ID)
     7.9 -
    7.10      val arg =
    7.11        XML_Data.make_list(
    7.12          XML_Data.make_pair(XML_Data.make_string)(
    7.13            XML_Data.make_option(XML_Data.make_list(
    7.14 -              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    7.15 +              XML_Data.make_pair(
    7.16 +                XML_Data.make_option(XML_Data.make_long))(
    7.17 +                XML_Data.make_option(XML_Data.make_long))))))(edits)
    7.18  
    7.19      input("Isar_Document.edit_version",
    7.20        Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))