# HG changeset patch # User wenzelm # Date 1283173760 -7200 # Node ID 4a4d34d2f97ba2c37ebc42fecf3c85e3ca4c6f43 # Parent 278f552b2e97d982aeec15a10dd610006660cd41 more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt; diff -r 278f552b2e97 -r 4a4d34d2f97b src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Mon Aug 30 14:56:27 2010 +0200 +++ b/src/Pure/Isar/runtime.ML Mon Aug 30 15:09:20 2010 +0200 @@ -11,6 +11,7 @@ exception EXCURSION_FAIL of exn * string exception TOPLEVEL_ERROR val exn_context: Proof.context option -> exn -> exn + val exn_messages: (exn -> Position.T) -> exn -> string list val exn_message: (exn -> Position.T) -> exn -> string val debugging: ('a -> 'b) -> 'a -> 'b val controlled_execution: ('a -> 'b) -> 'a -> 'b @@ -41,7 +42,7 @@ fun if_context NONE _ _ = [] | if_context (SOME ctxt) f xs = map (f ctxt) xs; -fun exn_message exn_position e = +fun exn_messages exn_position e = let fun raised exn name msgs = let val pos = Position.str_of (exn_position exn) in @@ -53,32 +54,36 @@ val detailed = ! Output.debugging; - fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn - | exn_msg _ (Exn.EXCEPTIONS []) = "Exception." - | 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 :: + fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn + | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns + | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) = + map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn) + | exn_msgs _ TERMINATE = ["Exit."] + | exn_msgs _ Exn.Interrupt = [] + | exn_msgs _ TimeLimit.TimeOut = ["Timeout."] + | exn_msgs _ TOPLEVEL_ERROR = ["Error."] + | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg] + | exn_msgs _ (ERROR msg) = [msg] + | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]] + | exn_msgs _ (exn as THEORY (msg, thys)) = + [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))] + | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg :: + (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))] + | exn_msgs 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 Display.string_of_thm thms else [])) - | exn_msg _ exn = raised exn (General.exnMessage exn) []; - in exn_msg NONE e end; + else []))] + | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg :: + (if detailed then if_context ctxt Syntax.string_of_term ts else []))] + | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg :: + (if detailed then if_context ctxt Display.string_of_thm thms else []))] + | exn_msgs _ exn = [raised exn (General.exnMessage exn) []]; + in exn_msgs NONE e end; + +fun exn_message exn_position exn = + (case exn_messages exn_position exn of + [] => "Interrupt." + | msgs => cat_lines msgs); diff -r 278f552b2e97 -r 4a4d34d2f97b src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Mon Aug 30 14:56:27 2010 +0200 +++ b/src/Pure/ML/ml_compiler.ML Mon Aug 30 15:09:20 2010 +0200 @@ -7,6 +7,7 @@ signature ML_COMPILER = sig val exn_position: exn -> Position.T + val exn_messages: exn -> string list val exn_message: exn -> string val eval: bool -> Position.T -> ML_Lex.token list -> unit end @@ -15,6 +16,7 @@ struct fun exn_position _ = Position.none; +val exn_messages = Runtime.exn_messages exn_position; val exn_message = Runtime.exn_message exn_position; fun eval verbose pos toks = diff -r 278f552b2e97 -r 4a4d34d2f97b src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Aug 30 14:56:27 2010 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Aug 30 15:09:20 2010 +0200 @@ -4,13 +4,6 @@ Advanced runtime compilation for Poly/ML 5.3.0. *) -signature ML_COMPILER = -sig - val exn_position: exn -> Position.T - val exn_message: exn -> string - val eval: bool -> Position.T -> ML_Lex.token list -> unit -end - structure ML_Compiler: ML_COMPILER = struct @@ -37,6 +30,7 @@ NONE => Position.none | SOME loc => position_of loc); +val exn_messages = Runtime.exn_messages exn_position; val exn_message = Runtime.exn_message exn_position; diff -r 278f552b2e97 -r 4a4d34d2f97b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Aug 30 14:56:27 2010 +0200 +++ b/src/Pure/ROOT.ML Mon Aug 30 15:09:20 2010 +0200 @@ -179,9 +179,9 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "Isar/runtime.ML"; +use "ML/ml_compiler.ML"; if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse - String.isPrefix "smlnj" ml_system -then use "ML/ml_compiler.ML" + String.isPrefix "smlnj" ml_system then () else use "ML/ml_compiler_polyml-5.3.ML"; use "ML/ml_context.ML";