# HG changeset patch
# User wenzelm
# Date 1181685726 -7200
# Node ID 9981199bf86552c1ce6b6504d8e00630cf52dc83
# Parent  de1476695aa6f0809222771a63e22d3157f176d8
transaction: context_position (non-destructive only);

diff -r de1476695aa6 -r 9981199bf865 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jun 13 00:02:05 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Jun 13 00:02:06 2007 +0200
@@ -358,16 +358,23 @@
 
 val stale_theory = ERROR "Stale theory encountered after succesful execution!";
 
-fun map_theory f = History.map
+fun map_theory f = History.map_current
   (fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE)
     | node => node);
 
+fun context_position pos = History.map_current
+  (fn Theory (Context.Proof lthy, ctxt) =>
+        Theory (Context.Proof (ContextPosition.put pos lthy), ctxt)
+    | Proof (prf, x) =>
+        Proof (ProofHistory.map_current (Proof.map_context (ContextPosition.put pos)) prf, x)
+    | node => node);
+
 fun return (result, NONE) = result
   | return (result, SOME exn) = raise FAILURE (result, exn);
 
 in
 
-fun transaction hist f (node, term) =
+fun transaction hist pos f (node, term) =
   let
     val cont_node = map_theory Theory.checkpoint node;
     val back_node = map_theory Theory.copy cont_node;
@@ -377,9 +384,11 @@
 
     val (result, err) =
       cont_node
+      |> context_position pos
       |> (f
-          |> (if hist then History.apply' (History.current back_node) else History.map)
+          |> (if hist then History.apply' (History.current back_node) else History.map_current)
           |> controlled_execution)
+      |> context_position Position.none
       |> normal_state
       handle exn => error_state cont_node exn;
   in
@@ -421,33 +430,33 @@
 
 fun keep_state int f = controlled_execution (fn x => tap (f int) x);
 
-fun apply_tr int (Init (f, term)) (state as Toplevel _) =
+fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
       let val node = Theory (Context.Theory (f int), NONE)
       in safe_exit state; State (History.init (undo_limit int) node, term) end
-  | apply_tr int (InitEmpty f) state =
+  | apply_tr int _ (InitEmpty f) state =
       (keep_state int (K f) state; safe_exit state; toplevel)
-  | apply_tr _ Exit (State (node, term)) =
+  | apply_tr _ _ Exit (State (node, term)) =
       (the_global_theory (History.current node); Toplevel (SOME (node, term)))
-  | apply_tr _ UndoExit (Toplevel (SOME state_info)) = State state_info
-  | apply_tr _ Kill (State (node, (_, kill))) =
+  | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
+  | apply_tr _ _ Kill (State (node, (_, kill))) =
       (kill (the_global_theory (History.current node)); toplevel)
-  | apply_tr _ (History f) (State (node, term)) = State (f node, term)
-  | apply_tr int (Keep f) state = keep_state int f state
-  | apply_tr int (Transaction (hist, f)) (State state) =
-      transaction hist (fn x => f int x) state
-  | apply_tr _ _ _ = raise UNDEF;
+  | apply_tr _ _ (History f) (State (node, term)) = State (f node, term)
+  | apply_tr int _ (Keep f) state = keep_state int f state
+  | apply_tr int pos (Transaction (hist, f)) (State state) =
+      transaction hist pos (fn x => f int x) state
+  | apply_tr _ _ _ _ = raise UNDEF;
 
-fun apply_union _ [] state = raise FAILURE (state, UNDEF)
-  | apply_union int (tr :: trs) state =
-      apply_tr int tr state
-        handle UNDEF => apply_union int trs state
-          | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
+fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
+  | apply_union int pos (tr :: trs) state =
+      apply_tr int pos tr state
+        handle UNDEF => apply_union int pos trs state
+          | FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
 in
 
-fun apply_trans int trs state = (apply_union int trs state, NONE)
+fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
 
 end;
@@ -660,7 +669,7 @@
 
 local
 
-fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
+fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) state =
   let
     val _ =
       if not int andalso int_only then warning (command_msg "Interactive-only " tr)
@@ -670,7 +679,7 @@
     fun do_profiling f x = profile (! profiling) f x;
 
     val (result, opt_exn) =
-       state |> (apply_trans int trans
+       state |> (apply_trans int pos trans
         |> (if ! profiling > 0 then do_profiling else I)
         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
     val _ =