# HG changeset patch # User berghofe # Date 1109168340 -3600 # Node ID 14d1672598126114d09f5f19db53509d96d66ca1 # Parent aea2f1706fdfc02751f74bf751735107cfbc541f Modified node_trans to avoid duplication of signature stamps when undoing. diff -r aea2f1706fdf -r 14d167259812 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Feb 23 15:00:03 2005 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Feb 23 15:19:00 2005 +0100 @@ -214,15 +214,14 @@ let fun mk_state nd = State (SOME (nd, term)); - val cont_node = History.map (checkpoint_node int) node; - val back_node = History.map (copy_node int) cont_node; + val f' = checkpoint_node int o f int o copy_node int; - val trans = if hist then History.apply_copy (copy_node int) else History.map; + val trans = if hist then History.apply else History.map; val (result, opt_exn) = - (mk_state (transform_error (interruptible (trans (f int))) cont_node), NONE) - handle exn => (mk_state cont_node, SOME exn); + (mk_state (transform_error (interruptible (trans f')) node), NONE) + handle exn => (mk_state node, SOME exn); in - if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback)) + if is_stale result then return (mk_state node, SOME (if_none opt_exn rollback)) else return (result, opt_exn) end;