# HG changeset patch # User wenzelm # Date 1244315482 -7200 # Node ID c5d2899b6de96326115aef7dfa16de1a377b72b8 # Parent 85e864045497acb811e2fdcd30b9774cfe919743 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML); diff -r 85e864045497 -r c5d2899b6de9 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jun 06 19:58:11 2009 +0200 +++ b/src/Pure/IsaMakefile Sat Jun 06 21:11:22 2009 +0200 @@ -62,12 +62,12 @@ Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ - Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \ - Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \ - Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \ - ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \ - ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ - ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ + Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \ + Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \ + Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \ + ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \ + ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \ + ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \ Proof/extraction.ML Proof/proof_rewrite_rules.ML \ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ diff -r 85e864045497 -r c5d2899b6de9 src/Pure/Isar/runtime.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/runtime.ML Sat Jun 06 21:11:22 2009 +0200 @@ -0,0 +1,107 @@ +(* Title: Pure/Isar/runtime.ML + Author: Makarius + +Isar toplevel runtime support. +*) + +signature RUNTIME = +sig + exception UNDEF + exception TERMINATE + exception EXCURSION_FAIL of exn * string + exception TOPLEVEL_ERROR + val exn_context: Proof.context option -> exn -> exn + val exn_message: (exn -> Position.T) -> exn -> string + val debugging: ('a -> 'b) -> 'a -> 'b + val controlled_execution: ('a -> 'b) -> 'a -> 'b + val toplevel_error: (exn -> string) -> ('a -> 'b) -> 'a -> 'b +end; + +structure Runtime: RUNTIME = +struct + +(** exceptions **) + +exception UNDEF; +exception TERMINATE; +exception EXCURSION_FAIL of exn * string; +exception TOPLEVEL_ERROR; + + +(* exn_context *) + +exception CONTEXT of Proof.context * exn; + +fun exn_context NONE exn = exn + | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn); + + +(* exn_message *) + +fun if_context NONE _ _ = [] + | if_context (SOME ctxt) f xs = map (f ctxt) xs; + +fun exn_message exn_position e = + let + fun raised exn name msgs = + let val pos = Position.str_of (exn_position exn) in + (case msgs of + [] => "exception " ^ name ^ " raised" ^ pos + | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg + | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) + end; + + val detailed = ! Output.debugging; + + fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn + | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) + | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = + exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) + | exn_msg _ TERMINATE = "Exit." + | exn_msg _ Exn.Interrupt = "Interrupt." + | exn_msg _ TimeLimit.TimeOut = "Timeout." + | exn_msg _ TOPLEVEL_ERROR = "Error." + | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg + | exn_msg _ (ERROR msg) = msg + | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg] + | exn_msg _ (exn as THEORY (msg, thys)) = + raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) + | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg :: + (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else [])) + | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg :: + (if detailed then + if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts + else [])) + | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg :: + (if detailed then if_context ctxt Syntax.string_of_term ts else [])) + | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg :: + (if detailed then if_context ctxt ProofContext.string_of_thm thms else [])) + | exn_msg _ exn = raised exn (General.exnMessage exn) []; + in exn_msg NONE e end; + + + +(** controlled execution **) + +fun debugging f x = + if ! Output.debugging then + Exn.release (exception_trace (fn () => + Exn.Result (f x) handle + exn as UNDEF => Exn.Exn exn + | exn as EXCURSION_FAIL _ => Exn.Exn exn)) + else f x; + +fun controlled_execution f = + f + |> debugging + |> Future.interruptible_task; + +fun toplevel_error exn_message f x = + let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in + f x handle exn => + (Output.error_msg (exn_message (exn_context ctxt exn)); + raise TOPLEVEL_ERROR) + end; + +end; + diff -r 85e864045497 -r c5d2899b6de9 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Jun 06 19:58:11 2009 +0200 +++ b/src/Pure/Isar/toplevel.ML Sat Jun 06 21:11:22 2009 +0200 @@ -32,8 +32,6 @@ val skip_proofs: bool ref exception TERMINATE exception TOPLEVEL_ERROR - exception CONTEXT of Proof.context * exn - val exn_message: exn -> string val program: (unit -> 'a) -> 'a type transition val empty: transition @@ -98,7 +96,7 @@ (** toplevel state **) -exception UNDEF; +exception UNDEF = Runtime.UNDEF; (* local theory wrappers *) @@ -225,102 +223,20 @@ val profiling = ref 0; val skip_proofs = ref false; -exception TERMINATE; -exception EXCURSION_FAIL of exn * string; -exception FAILURE of state * exn; -exception TOPLEVEL_ERROR; - - -(* print exceptions *) - -exception CONTEXT of Proof.context * exn; - -fun exn_context NONE exn = exn - | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn); - -local - -fun if_context NONE _ _ = [] - | if_context (SOME ctxt) f xs = map (f ctxt) xs; - -fun raised exn name msgs = - let val pos = Position.str_of (ML_Compiler.exception_position exn) in - (case msgs of - [] => "exception " ^ name ^ " raised" ^ pos - | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg - | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) - end; - -in - -fun exn_message e = - let - val detailed = ! debug; - - fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn - | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) - | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = - exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) - | exn_msg _ TERMINATE = "Exit." - | exn_msg _ Exn.Interrupt = "Interrupt." - | exn_msg _ TimeLimit.TimeOut = "Timeout." - | exn_msg _ TOPLEVEL_ERROR = "Error." - | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg - | exn_msg _ (ERROR msg) = msg - | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg] - | exn_msg _ (exn as THEORY (msg, thys)) = - raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) - | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg :: - (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else [])) - | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg :: - (if detailed then - if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts - else [])) - | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg :: - (if detailed then if_context ctxt Syntax.string_of_term ts else [])) - | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg :: - (if detailed then if_context ctxt ProofContext.string_of_thm thms else [])) - | exn_msg _ exn = raised exn (General.exnMessage exn) [] - in exn_msg NONE e end; - -end; - - -(* controlled execution *) - -local - -fun debugging f x = - if ! debug then - Exn.release (exception_trace (fn () => - Exn.Result (f x) handle - exn as UNDEF => Exn.Exn exn - | exn as EXCURSION_FAIL _ => Exn.Exn exn)) - else f x; - -fun toplevel_error f x = - let val ctxt = try ML_Context.the_local_context () in - f x handle exn => - (Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR) - end; - -in - -fun controlled_execution f = - f - |> debugging - |> Future.interruptible_task; +exception TERMINATE = Runtime.TERMINATE; +exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL; +exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR; fun program f = (f - |> controlled_execution - |> toplevel_error) (); - -end; + |> Runtime.controlled_execution + |> Runtime.toplevel_error ML_Compiler.exn_message) (); (* node transactions -- maintaining stable checkpoints *) +exception FAILURE of state * exn; + local fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) @@ -329,7 +245,7 @@ fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy) | is_draft_theory _ = false; -fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false; +fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false; fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") | stale_error some = some; @@ -349,7 +265,7 @@ val (result, err) = cont_node - |> controlled_execution f + |> Runtime.controlled_execution f |> map_theory Theory.checkpoint |> state_error NONE handle exn => state_error (SOME exn) cont_node; @@ -382,9 +298,9 @@ | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) = State (NONE, prev) | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) = - (controlled_execution exit thy; toplevel) + (Runtime.controlled_execution exit thy; toplevel) | apply_tr int _ (Keep f) state = - controlled_execution (fn x => tap (f int) x) state + Runtime.controlled_execution (fn x => tap (f int) x) state | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) = apply_transaction pos (fn x => f int x) g state | apply_tr _ _ _ _ = raise UNDEF; @@ -392,7 +308,7 @@ fun apply_union _ _ [] state = raise FAILURE (state, UNDEF) | apply_union int pos (tr :: trs) state = apply_union int pos trs state - handle UNDEF => apply_tr int pos tr state + handle Runtime.UNDEF => apply_tr int pos tr state | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); @@ -628,7 +544,8 @@ setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) (); fun error_msg tr exn_info = - setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) (); + setmp_thread_position tr (fn () => + Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) (); (* post-transition hooks *) @@ -671,7 +588,7 @@ (case app int tr st of (_, SOME TERMINATE) => NONE | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info) - | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr)) + | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr)) | (st', NONE) => SOME (st', NONE)); val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ()); in res end; diff -r 85e864045497 -r c5d2899b6de9 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jun 06 19:58:11 2009 +0200 +++ b/src/Pure/ROOT.ML Sat Jun 06 21:11:22 2009 +0200 @@ -155,6 +155,7 @@ (*ML support*) use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; +use "Isar/runtime.ML"; if ml_system = "polyml-experimental" then use "ML/ml_compiler_polyml-5.3.ML" else use "ML/ml_compiler.ML";