# HG changeset patch # User wenzelm # Date 1112858829 -7200 # Node ID 53c049a365cf73c0b511b490d2eb65a0a898c18d # Parent b7bdc1651198071dc6271957c84c4728e7cc0bcb improved exn_message; diff -r b7bdc1651198 -r 53c049a365cf src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Apr 07 09:26:55 2005 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Apr 07 09:27:09 2005 +0200 @@ -176,6 +176,7 @@ val enter_forward_proof = node_case Proof.init_state Proof.enter_forward; + (** toplevel transitions **) exception TERMINATE; @@ -366,36 +367,45 @@ (fn Theory thy => exit thy | _ => raise UNDEF) (fn Theory thy => kill thy | _ => raise UNDEF); -(* -The skip_proofs flag allows proof scripts to be skipped during interactive -proof in order to speed up processing of large theories. While in skipping -mode, states are represented as SkipProof (h, thy), where h contains a -counter for the number of open proof blocks. -*) + +(* typed transitions *) + +(*The skip_proofs flag allows proof scripts to be skipped during + interactive proof in order to speed up processing of large + theories. While in skipping mode, states are represented as + SkipProof (h, thy), where h contains a counter for the number of + open proof blocks.*) val skip_proofs = ref false; fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF)); fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF)); + fun theory_to_proof f = app_current (fn int => (fn Theory thy => - if !skip_proofs then SkipProof (History.init (undo_limit int) 0, + if ! skip_proofs then SkipProof (History.init (undo_limit int) 0, fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy)))) else Proof (f int thy) | _ => raise UNDEF)); + fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf) | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF | _ => raise UNDEF)); + val proof' = proof''' true; val proof = proof' o K; val proof'' = proof''' false o K; + fun proof_to_theory' f = map_current (fn int => (fn Proof prf => Theory (f int prf) | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF | _ => raise UNDEF)); + val proof_to_theory = proof_to_theory' o K; + fun skip_proof f = map_current (fn int => (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF)); + fun skip_proof_to_theory p = map_current (fn int => (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF)); @@ -408,81 +418,73 @@ (** toplevel transactions **) val quiet = ref false; -val debug = ref false; (* Verbose messages for core exceptions. *) +val debug = ref false; + (* print exceptions *) -fun raised name = "exception " ^ name ^ " raised"; -fun raised_msg name msg = raised name ^ ": " ^ msg; +local + +fun with_context f xs = + (case Context.get_context () of NONE => [] + | SOME thy => map (f (Theory.sign_of thy)) xs); + +fun raised name [] = "exception " ^ name ^ " raised" + | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg + | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); -fun msg_on_debug (THM (msg, i, thms)) = - if !debug - then raised_msg ("THM " ^ string_of_int i) - (cat_lines ("" :: msg :: map Display.string_of_thm thms)) - else raised_msg "THM" msg - | msg_on_debug (THEORY (msg, thys)) = - if !debug - then raised_msg "THEORY" (cat_lines ("" :: msg :: - map (Pretty.string_of o Display.pretty_theory) thys)) - else msg - | msg_on_debug (AST (msg, asts)) = - if !debug - then raised_msg "AST" (cat_lines ("" :: msg :: - map (Pretty.string_of o Syntax.pretty_ast) asts)) - else msg - | msg_on_debug (TERM (msg, ts)) = - (case (!debug, Context.get_context ()) of - (true, SOME thy) => - let val sg = Theory.sign_of thy in - raised_msg "TERM" - (cat_lines - ("" :: msg :: map (Sign.string_of_term sg) ts)) - end - | _ => raised_msg "TERM" msg) - | msg_on_debug (TYPE (msg, Ts, ts)) = - (case (!debug, Context.get_context ()) of - (true, SOME thy) => - let val sg = Theory.sign_of thy in - raised_msg "TYPE" - (cat_lines - ("" :: msg :: map (Sign.string_of_typ sg) Ts @ - map (Sign.string_of_term sg) ts)) - end - | _ => raised_msg "TYPE" msg) +fun exn_msg _ TERMINATE = "Exit." + | exn_msg _ RESTART = "Restart." + | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] + | exn_msg _ Interrupt = "Interrupt." + | exn_msg _ ERROR = "ERROR." + | exn_msg _ (ERROR_MESSAGE msg) = msg + | exn_msg false (THEORY (msg, _)) = msg + | exn_msg true (THEORY (msg, thys)) = + raised "THEORY" (msg :: map (Pretty.string_of o Display.pretty_theory) thys) + | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg + | exn_msg _ (Proof.STATE (msg, _)) = msg + | exn_msg _ (ProofHistory.FAIL msg) = msg + | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) = + fail_msg detailed "simproc" ((name, Position.none), exn) + | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info + | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info + | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info + | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] + | exn_msg true (Syntax.AST (msg, asts)) = + raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts) + | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg] + | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: + with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts) + | exn_msg false (TERM (msg, _)) = raised "TERM" [msg] + | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts) + | exn_msg false (THM (msg, _, _)) = raised "THM" [msg] + | exn_msg true (THM (msg, i, thms)) = + raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms) + | exn_msg _ Option = raised "Option" [] + | exn_msg _ UnequalLengths = raised "UnequalLengths" [] + | exn_msg _ Empty = raised "Empty" [] + | exn_msg _ Subscript = raised "Subscript" [] + | exn_msg _ exn = General.exnMessage exn +and fail_msg detailed kind ((name, pos), exn) = + "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; -fun exn_message TERMINATE = "Exit." - | exn_message RESTART = "Restart." - | exn_message (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_message exn, msg] - | exn_message Interrupt = "Interrupt." - | exn_message ERROR = "ERROR." - | exn_message (ERROR_MESSAGE msg) = msg - | exn_message (THEORY (msg, thys)) = msg_on_debug (THEORY (msg, thys)) - | exn_message (ProofContext.CONTEXT (msg, _)) = msg - | exn_message (Proof.STATE (msg, _)) = msg - | exn_message (ProofHistory.FAIL msg) = msg - | exn_message (MetaSimplifier.SIMPROC_FAIL (name, exn)) = - fail_message "simproc" ((name, Position.none), exn) - | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info - | exn_message (Method.METHOD_FAIL info) = fail_message "method" info - | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info - | exn_message (Syntax.AST (msg, asts)) = msg_on_debug (AST (msg, asts)) - | exn_message (TYPE (msg, Ts, ts)) = msg_on_debug (TYPE (msg, Ts, ts)) - | exn_message (TERM (msg, ts)) = msg_on_debug (TERM (msg, ts)) - | exn_message (THM (msg, i, thms)) = msg_on_debug (THM (msg, i, thms)) - | exn_message Option = raised "Option" - | exn_message UnequalLengths = raised "UnequalLengths" - | exn_message Empty = raised "Empty" - | exn_message Subscript = raised "Subscript" - | exn_message exn = General.exnMessage exn -and fail_message kind ((name, pos), exn) = - "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_message exn; +in + +val debug = ref false; + +fun exn_message exn = exn_msg (! debug) exn; fun print_exn NONE = () | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]); +end; + (* apply transitions *) +val quiet = ref false; + local fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =