more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
authorwenzelm
Mon Aug 30 15:09:20 2010 +0200 (2010-08-30)
changeset 388744a4d34d2f97b
parent 38873 278f552b2e97
child 38875 c7a66b584147
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Mon Aug 30 14:56:27 2010 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Mon Aug 30 15:09:20 2010 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    exception EXCURSION_FAIL of exn * string
     1.5    exception TOPLEVEL_ERROR
     1.6    val exn_context: Proof.context option -> exn -> exn
     1.7 +  val exn_messages: (exn -> Position.T) -> exn -> string list
     1.8    val exn_message: (exn -> Position.T) -> exn -> string
     1.9    val debugging: ('a -> 'b) -> 'a -> 'b
    1.10    val controlled_execution: ('a -> 'b) -> 'a -> 'b
    1.11 @@ -41,7 +42,7 @@
    1.12  fun if_context NONE _ _ = []
    1.13    | if_context (SOME ctxt) f xs = map (f ctxt) xs;
    1.14  
    1.15 -fun exn_message exn_position e =
    1.16 +fun exn_messages exn_position e =
    1.17    let
    1.18      fun raised exn name msgs =
    1.19        let val pos = Position.str_of (exn_position exn) in
    1.20 @@ -53,32 +54,36 @@
    1.21  
    1.22      val detailed = ! Output.debugging;
    1.23  
    1.24 -    fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
    1.25 -      | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
    1.26 -      | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
    1.27 -      | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
    1.28 -          exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
    1.29 -      | exn_msg _ TERMINATE = "Exit."
    1.30 -      | exn_msg _ Exn.Interrupt = "Interrupt."
    1.31 -      | exn_msg _ TimeLimit.TimeOut = "Timeout."
    1.32 -      | exn_msg _ TOPLEVEL_ERROR = "Error."
    1.33 -      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
    1.34 -      | exn_msg _ (ERROR msg) = msg
    1.35 -      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
    1.36 -      | exn_msg _ (exn as THEORY (msg, thys)) =
    1.37 -          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
    1.38 -      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
    1.39 -            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
    1.40 -      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
    1.41 +    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
    1.42 +      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
    1.43 +      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
    1.44 +          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
    1.45 +      | exn_msgs _ TERMINATE = ["Exit."]
    1.46 +      | exn_msgs _ Exn.Interrupt = []
    1.47 +      | exn_msgs _ TimeLimit.TimeOut = ["Timeout."]
    1.48 +      | exn_msgs _ TOPLEVEL_ERROR = ["Error."]
    1.49 +      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
    1.50 +      | exn_msgs _ (ERROR msg) = [msg]
    1.51 +      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
    1.52 +      | exn_msgs _ (exn as THEORY (msg, thys)) =
    1.53 +          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    1.54 +      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
    1.55 +            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
    1.56 +      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
    1.57              (if detailed then
    1.58                if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
    1.59 -             else []))
    1.60 -      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
    1.61 -            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
    1.62 -      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
    1.63 -            (if detailed then if_context ctxt Display.string_of_thm thms else []))
    1.64 -      | exn_msg _ exn = raised exn (General.exnMessage exn) [];
    1.65 -  in exn_msg NONE e end;
    1.66 +             else []))]
    1.67 +      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
    1.68 +            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
    1.69 +      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
    1.70 +            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
    1.71 +      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
    1.72 +  in exn_msgs NONE e end;
    1.73 +
    1.74 +fun exn_message exn_position exn =
    1.75 +  (case exn_messages exn_position exn of
    1.76 +    [] => "Interrupt."
    1.77 +  | msgs => cat_lines msgs);
    1.78  
    1.79  
    1.80  
     2.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Aug 30 14:56:27 2010 +0200
     2.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 30 15:09:20 2010 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  signature ML_COMPILER =
     2.5  sig
     2.6    val exn_position: exn -> Position.T
     2.7 +  val exn_messages: exn -> string list
     2.8    val exn_message: exn -> string
     2.9    val eval: bool -> Position.T -> ML_Lex.token list -> unit
    2.10  end
    2.11 @@ -15,6 +16,7 @@
    2.12  struct
    2.13  
    2.14  fun exn_position _ = Position.none;
    2.15 +val exn_messages = Runtime.exn_messages exn_position;
    2.16  val exn_message = Runtime.exn_message exn_position;
    2.17  
    2.18  fun eval verbose pos toks =
     3.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 30 14:56:27 2010 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Aug 30 15:09:20 2010 +0200
     3.3 @@ -4,13 +4,6 @@
     3.4  Advanced runtime compilation for Poly/ML 5.3.0.
     3.5  *)
     3.6  
     3.7 -signature ML_COMPILER =
     3.8 -sig
     3.9 -  val exn_position: exn -> Position.T
    3.10 -  val exn_message: exn -> string
    3.11 -  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    3.12 -end
    3.13 -
    3.14  structure ML_Compiler: ML_COMPILER =
    3.15  struct
    3.16  
    3.17 @@ -37,6 +30,7 @@
    3.18      NONE => Position.none
    3.19    | SOME loc => position_of loc);
    3.20  
    3.21 +val exn_messages = Runtime.exn_messages exn_position;
    3.22  val exn_message = Runtime.exn_message exn_position;
    3.23  
    3.24  
     4.1 --- a/src/Pure/ROOT.ML	Mon Aug 30 14:56:27 2010 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Aug 30 15:09:20 2010 +0200
     4.3 @@ -179,9 +179,9 @@
     4.4  use "ML/ml_syntax.ML";
     4.5  use "ML/ml_env.ML";
     4.6  use "Isar/runtime.ML";
     4.7 +use "ML/ml_compiler.ML";
     4.8  if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
     4.9 -  String.isPrefix "smlnj" ml_system
    4.10 -then use "ML/ml_compiler.ML"
    4.11 +  String.isPrefix "smlnj" ml_system then ()
    4.12  else use "ML/ml_compiler_polyml-5.3.ML";
    4.13  use "ML/ml_context.ML";
    4.14