transaction: context_position (non-destructive only);
authorwenzelm
Wed Jun 13 00:02:06 2007 +0200 (2007-06-13)
changeset 233639981199bf865
parent 23362 de1476695aa6
child 23364 1f3b832c90c1
transaction: context_position (non-destructive only);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jun 13 00:02:05 2007 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jun 13 00:02:06 2007 +0200
     1.3 @@ -358,16 +358,23 @@
     1.4  
     1.5  val stale_theory = ERROR "Stale theory encountered after succesful execution!";
     1.6  
     1.7 -fun map_theory f = History.map
     1.8 +fun map_theory f = History.map_current
     1.9    (fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE)
    1.10      | node => node);
    1.11  
    1.12 +fun context_position pos = History.map_current
    1.13 +  (fn Theory (Context.Proof lthy, ctxt) =>
    1.14 +        Theory (Context.Proof (ContextPosition.put pos lthy), ctxt)
    1.15 +    | Proof (prf, x) =>
    1.16 +        Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put pos)) prf, x)
    1.17 +    | node => node);
    1.18 +
    1.19  fun return (result, NONE) = result
    1.20    | return (result, SOME exn) = raise FAILURE (result, exn);
    1.21  
    1.22  in
    1.23  
    1.24 -fun transaction hist f (node, term) =
    1.25 +fun transaction hist pos f (node, term) =
    1.26    let
    1.27      val cont_node = map_theory Theory.checkpoint node;
    1.28      val back_node = map_theory Theory.copy cont_node;
    1.29 @@ -377,9 +384,11 @@
    1.30  
    1.31      val (result, err) =
    1.32        cont_node
    1.33 +      |> context_position pos
    1.34        |> (f
    1.35 -          |> (if hist then History.apply' (History.current back_node) else History.map)
    1.36 +          |> (if hist then History.apply' (History.current back_node) else History.map_current)
    1.37            |> controlled_execution)
    1.38 +      |> context_position Position.none
    1.39        |> normal_state
    1.40        handle exn => error_state cont_node exn;
    1.41    in
    1.42 @@ -421,33 +430,33 @@
    1.43  
    1.44  fun keep_state int f = controlled_execution (fn x => tap (f int) x);
    1.45  
    1.46 -fun apply_tr int (Init (f, term)) (state as Toplevel _) =
    1.47 +fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
    1.48        let val node = Theory (Context.Theory (f int), NONE)
    1.49        in safe_exit state; State (History.init (undo_limit int) node, term) end
    1.50 -  | apply_tr int (InitEmpty f) state =
    1.51 +  | apply_tr int _ (InitEmpty f) state =
    1.52        (keep_state int (K f) state; safe_exit state; toplevel)
    1.53 -  | apply_tr _ Exit (State (node, term)) =
    1.54 +  | apply_tr _ _ Exit (State (node, term)) =
    1.55        (the_global_theory (History.current node); Toplevel (SOME (node, term)))
    1.56 -  | apply_tr _ UndoExit (Toplevel (SOME state_info)) = State state_info
    1.57 -  | apply_tr _ Kill (State (node, (_, kill))) =
    1.58 +  | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
    1.59 +  | apply_tr _ _ Kill (State (node, (_, kill))) =
    1.60        (kill (the_global_theory (History.current node)); toplevel)
    1.61 -  | apply_tr _ (History f) (State (node, term)) = State (f node, term)
    1.62 -  | apply_tr int (Keep f) state = keep_state int f state
    1.63 -  | apply_tr int (Transaction (hist, f)) (State state) =
    1.64 -      transaction hist (fn x => f int x) state
    1.65 -  | apply_tr _ _ _ = raise UNDEF;
    1.66 +  | apply_tr _ _ (History f) (State (node, term)) = State (f node, term)
    1.67 +  | apply_tr int _ (Keep f) state = keep_state int f state
    1.68 +  | apply_tr int pos (Transaction (hist, f)) (State state) =
    1.69 +      transaction hist pos (fn x => f int x) state
    1.70 +  | apply_tr _ _ _ _ = raise UNDEF;
    1.71  
    1.72 -fun apply_union _ [] state = raise FAILURE (state, UNDEF)
    1.73 -  | apply_union int (tr :: trs) state =
    1.74 -      apply_tr int tr state
    1.75 -        handle UNDEF => apply_union int trs state
    1.76 -          | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
    1.77 +fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
    1.78 +  | apply_union int pos (tr :: trs) state =
    1.79 +      apply_tr int pos tr state
    1.80 +        handle UNDEF => apply_union int pos trs state
    1.81 +          | FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state
    1.82            | exn as FAILURE _ => raise exn
    1.83            | exn => raise FAILURE (state, exn);
    1.84  
    1.85  in
    1.86  
    1.87 -fun apply_trans int trs state = (apply_union int trs state, NONE)
    1.88 +fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
    1.89    handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
    1.90  
    1.91  end;
    1.92 @@ -660,7 +669,7 @@
    1.93  
    1.94  local
    1.95  
    1.96 -fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
    1.97 +fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) state =
    1.98    let
    1.99      val _ =
   1.100        if not int andalso int_only then warning (command_msg "Interactive-only " tr)
   1.101 @@ -670,7 +679,7 @@
   1.102      fun do_profiling f x = profile (! profiling) f x;
   1.103  
   1.104      val (result, opt_exn) =
   1.105 -       state |> (apply_trans int trans
   1.106 +       state |> (apply_trans int pos trans
   1.107          |> (if ! profiling > 0 then do_profiling else I)
   1.108          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
   1.109      val _ =