# HG changeset patch # User haftmann # Date 1282060495 -7200 # Node ID 3b898102963f8ed270a3bd7070c0cf06d2ad6cb5 # Parent 8a7ff1c257737fdbebfe0e3873c95e432559307b# Parent 95a41e6ef5a864f1f5bc9b96038d531b33b2247b merged diff -r 95a41e6ef5a8 -r 3b898102963f src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 17 17:54:55 2010 +0200 @@ -63,12 +63,12 @@ | string_for_connective AIff = "<=>" | string_for_connective ANotIff = "<~>" fun string_for_formula (AQuant (q, xs, phi)) = - string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ - string_for_formula phi + "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ + string_for_formula phi ^ ")" | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) = space_implode " != " (map string_for_term ts) | string_for_formula (AConn (c, [phi])) = - string_for_connective c ^ " " ^ string_for_formula phi + "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")" | string_for_formula (AConn (c, phis)) = "(" ^ space_implode (" " ^ string_for_connective c ^ " ") (map string_for_formula phis) ^ ")" diff -r 95a41e6ef5a8 -r 3b898102963f src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 17:54:55 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, @@ -183,7 +185,7 @@ required_execs = [], arguments = fn _ => fn timeout => "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ - " --input_file ", + " --input_file", proof_delims = [("=========== Refutation ==========", "======= End of refutation ======="), @@ -195,7 +197,7 @@ (TimedOut, "SZS status Timeout"), (Unprovable, "Satisfiability detected"), (OutOfResources, "Refutation not found"), - (OldVampire, "input_file")], + (OldVampire, "not a valid option")], max_new_relevant_facts_per_iter = 50 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} diff -r 95a41e6ef5a8 -r 3b898102963f src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 17 17:54:55 2010 +0200 @@ -85,8 +85,7 @@ fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = case test (xs @ seen) of - result as {outcome = NONE, proof, used_thm_names, ...} - : prover_result => + result as {outcome = NONE, proof, used_thm_names, ...} : prover_result => sublinear_minimize test (filter_used_facts used_thm_names xs) (filter_used_facts used_thm_names seen, result) | _ => sublinear_minimize test xs (x :: seen, result) diff -r 95a41e6ef5a8 -r 3b898102963f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 17 17:54:55 2010 +0200 @@ -279,10 +279,10 @@ | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) | add_type_constraint _ = I -fun fix_atp_variable_name s = +fun repair_atp_variable_name f s = let fun subscript_name s n = s ^ nat_subscript n - val s = String.map Char.toLower s + val s = String.map f s in case space_explode "_" s of [_] => (case take_suffix Char.isDigit (String.explode s) of @@ -349,9 +349,10 @@ SOME b => Var ((b, 0), T) | NONE => if is_tptp_variable a then - Var ((fix_atp_variable_name a, 0), T) + Var ((repair_atp_variable_name Char.toLower a, 0), T) else - raise Fail ("Unexpected constant: " ^ quote a) + (* Skolem constants? *) + Var ((repair_atp_variable_name Char.toUpper a, 0), T) in list_comb (t, ts) end in aux (SOME HOLogic.boolT) [] end @@ -410,7 +411,8 @@ do_formula pos (AQuant (q, xs, phi')) #>> quantify_over_free (case q of AForall => @{const_name All} - | AExists => @{const_name Ex}) x + | AExists => @{const_name Ex}) + (repair_atp_variable_name Char.toLower x) | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 @@ -834,6 +836,7 @@ second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst in proof_top @ proof_bottom end +(* FIXME: Still needed? Probably not. *) val kill_duplicate_assumptions_in_proof = let fun relabel_facts subst = diff -r 95a41e6ef5a8 -r 3b898102963f src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 17 17:54:55 2010 +0200 @@ -102,41 +102,41 @@ (0 upto length Ts - 1 ~~ Ts)) fun introduce_combinators_in_term ctxt kind t = - let - val thy = ProofContext.theory_of ctxt - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - let - val t = t |> conceal_bounds Ts - |> Envir.eta_contract - val ([t], ctxt') = Variable.import_terms true [t] ctxt - in - t |> cterm_of thy - |> Clausifier.introduce_combinators_in_cterm - |> singleton (Variable.export ctxt' ctxt) - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - end - in t |> not (Meson.is_fol_term thy t) ? aux [] end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - case kind of - Axiom => HOLogic.true_const - | Conjecture => HOLogic.false_const + let val thy = ProofContext.theory_of ctxt in + if Meson.is_fol_term thy t then + t + else + let + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + t |> conceal_bounds Ts + |> Envir.eta_contract + |> cterm_of thy + |> Clausifier.introduce_combinators_in_cterm + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + val ([t], ctxt') = Variable.import_terms true [t] ctxt + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + case kind of + Axiom => HOLogic.true_const + | Conjecture => HOLogic.false_const + end (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the same in Sledgehammer to prevent the discovery of unreplable proofs. *) diff -r 95a41e6ef5a8 -r 3b898102963f 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:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/General/linear_set.scala Tue Aug 17 17:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/IsaMakefile Tue Aug 17 17:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/PIDE/document.ML Tue Aug 17 17:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/ROOT.ML Tue Aug 17 17:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/System/isar_document.ML --- a/src/Pure/System/isar_document.ML Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/System/isar_document.ML Tue Aug 17 17:54:55 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 95a41e6ef5a8 -r 3b898102963f src/Pure/System/isar_document.scala --- a/src/Pure/System/isar_document.scala Tue Aug 17 17:54:46 2010 +0200 +++ b/src/Pure/System/isar_document.scala Tue Aug 17 17:54:55 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))