1.1 --- a/src/Pure/Isar/toplevel.ML Sat Jun 06 19:58:11 2009 +0200
1.2 +++ b/src/Pure/Isar/toplevel.ML Sat Jun 06 21:11:22 2009 +0200
1.3 @@ -32,8 +32,6 @@
1.4 val skip_proofs: bool ref
1.5 exception TERMINATE
1.6 exception TOPLEVEL_ERROR
1.7 - exception CONTEXT of Proof.context * exn
1.8 - val exn_message: exn -> string
1.9 val program: (unit -> 'a) -> 'a
1.10 type transition
1.11 val empty: transition
1.12 @@ -98,7 +96,7 @@
1.13
1.14 (** toplevel state **)
1.15
1.16 -exception UNDEF;
1.17 +exception UNDEF = Runtime.UNDEF;
1.18
1.19
1.20 (* local theory wrappers *)
1.21 @@ -225,102 +223,20 @@
1.22 val profiling = ref 0;
1.23 val skip_proofs = ref false;
1.24
1.25 -exception TERMINATE;
1.26 -exception EXCURSION_FAIL of exn * string;
1.27 -exception FAILURE of state * exn;
1.28 -exception TOPLEVEL_ERROR;
1.29 -
1.30 -
1.31 -(* print exceptions *)
1.32 -
1.33 -exception CONTEXT of Proof.context * exn;
1.34 -
1.35 -fun exn_context NONE exn = exn
1.36 - | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
1.37 -
1.38 -local
1.39 -
1.40 -fun if_context NONE _ _ = []
1.41 - | if_context (SOME ctxt) f xs = map (f ctxt) xs;
1.42 -
1.43 -fun raised exn name msgs =
1.44 - let val pos = Position.str_of (ML_Compiler.exception_position exn) in
1.45 - (case msgs of
1.46 - [] => "exception " ^ name ^ " raised" ^ pos
1.47 - | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
1.48 - | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
1.49 - end;
1.50 -
1.51 -in
1.52 -
1.53 -fun exn_message e =
1.54 - let
1.55 - val detailed = ! debug;
1.56 -
1.57 - fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
1.58 - | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
1.59 - | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
1.60 - exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
1.61 - | exn_msg _ TERMINATE = "Exit."
1.62 - | exn_msg _ Exn.Interrupt = "Interrupt."
1.63 - | exn_msg _ TimeLimit.TimeOut = "Timeout."
1.64 - | exn_msg _ TOPLEVEL_ERROR = "Error."
1.65 - | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
1.66 - | exn_msg _ (ERROR msg) = msg
1.67 - | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
1.68 - | exn_msg _ (exn as THEORY (msg, thys)) =
1.69 - raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
1.70 - | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
1.71 - (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
1.72 - | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
1.73 - (if detailed then
1.74 - if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
1.75 - else []))
1.76 - | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
1.77 - (if detailed then if_context ctxt Syntax.string_of_term ts else []))
1.78 - | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
1.79 - (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
1.80 - | exn_msg _ exn = raised exn (General.exnMessage exn) []
1.81 - in exn_msg NONE e end;
1.82 -
1.83 -end;
1.84 -
1.85 -
1.86 -(* controlled execution *)
1.87 -
1.88 -local
1.89 -
1.90 -fun debugging f x =
1.91 - if ! debug then
1.92 - Exn.release (exception_trace (fn () =>
1.93 - Exn.Result (f x) handle
1.94 - exn as UNDEF => Exn.Exn exn
1.95 - | exn as EXCURSION_FAIL _ => Exn.Exn exn))
1.96 - else f x;
1.97 -
1.98 -fun toplevel_error f x =
1.99 - let val ctxt = try ML_Context.the_local_context () in
1.100 - f x handle exn =>
1.101 - (Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR)
1.102 - end;
1.103 -
1.104 -in
1.105 -
1.106 -fun controlled_execution f =
1.107 - f
1.108 - |> debugging
1.109 - |> Future.interruptible_task;
1.110 +exception TERMINATE = Runtime.TERMINATE;
1.111 +exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
1.112 +exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
1.113
1.114 fun program f =
1.115 (f
1.116 - |> controlled_execution
1.117 - |> toplevel_error) ();
1.118 -
1.119 -end;
1.120 + |> Runtime.controlled_execution
1.121 + |> Runtime.toplevel_error ML_Compiler.exn_message) ();
1.122
1.123
1.124 (* node transactions -- maintaining stable checkpoints *)
1.125
1.126 +exception FAILURE of state * exn;
1.127 +
1.128 local
1.129
1.130 fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
1.131 @@ -329,7 +245,7 @@
1.132 fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
1.133 | is_draft_theory _ = false;
1.134
1.135 -fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
1.136 +fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false;
1.137
1.138 fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
1.139 | stale_error some = some;
1.140 @@ -349,7 +265,7 @@
1.141
1.142 val (result, err) =
1.143 cont_node
1.144 - |> controlled_execution f
1.145 + |> Runtime.controlled_execution f
1.146 |> map_theory Theory.checkpoint
1.147 |> state_error NONE
1.148 handle exn => state_error (SOME exn) cont_node;
1.149 @@ -382,9 +298,9 @@
1.150 | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
1.151 State (NONE, prev)
1.152 | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
1.153 - (controlled_execution exit thy; toplevel)
1.154 + (Runtime.controlled_execution exit thy; toplevel)
1.155 | apply_tr int _ (Keep f) state =
1.156 - controlled_execution (fn x => tap (f int) x) state
1.157 + Runtime.controlled_execution (fn x => tap (f int) x) state
1.158 | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
1.159 apply_transaction pos (fn x => f int x) g state
1.160 | apply_tr _ _ _ _ = raise UNDEF;
1.161 @@ -392,7 +308,7 @@
1.162 fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
1.163 | apply_union int pos (tr :: trs) state =
1.164 apply_union int pos trs state
1.165 - handle UNDEF => apply_tr int pos tr state
1.166 + handle Runtime.UNDEF => apply_tr int pos tr state
1.167 | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
1.168 | exn as FAILURE _ => raise exn
1.169 | exn => raise FAILURE (state, exn);
1.170 @@ -628,7 +544,8 @@
1.171 setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
1.172
1.173 fun error_msg tr exn_info =
1.174 - setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();
1.175 + setmp_thread_position tr (fn () =>
1.176 + Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
1.177
1.178
1.179 (* post-transition hooks *)
1.180 @@ -671,7 +588,7 @@
1.181 (case app int tr st of
1.182 (_, SOME TERMINATE) => NONE
1.183 | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
1.184 - | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr))
1.185 + | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
1.186 | (st', NONE) => SOME (st', NONE));
1.187 val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
1.188 in res end;