improved exn_message;
authorwenzelm
Thu Apr 07 09:27:09 2005 +0200 (2005-04-07 ago)
changeset 1566853c049a365cf
parent 15667 b7bdc1651198
child 15669 2b1f1902505d
improved exn_message;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Apr 07 09:26:55 2005 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Apr 07 09:27:09 2005 +0200
     1.3 @@ -176,6 +176,7 @@
     1.4  val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
     1.5  
     1.6  
     1.7 +
     1.8  (** toplevel transitions **)
     1.9  
    1.10  exception TERMINATE;
    1.11 @@ -366,36 +367,45 @@
    1.12      (fn Theory thy => exit thy | _ => raise UNDEF)
    1.13      (fn Theory thy => kill thy | _ => raise UNDEF);
    1.14  
    1.15 -(*
    1.16 -The skip_proofs flag allows proof scripts to be skipped during interactive
    1.17 -proof in order to speed up processing of large theories. While in skipping
    1.18 -mode, states are represented as SkipProof (h, thy), where h contains a
    1.19 -counter for the number of open proof blocks.
    1.20 -*)
    1.21 +
    1.22 +(* typed transitions *)
    1.23 +
    1.24 +(*The skip_proofs flag allows proof scripts to be skipped during
    1.25 +  interactive proof in order to speed up processing of large
    1.26 +  theories. While in skipping mode, states are represented as
    1.27 +  SkipProof (h, thy), where h contains a counter for the number of
    1.28 +  open proof blocks.*)
    1.29  
    1.30  val skip_proofs = ref false;
    1.31  
    1.32  fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
    1.33  fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
    1.34 +
    1.35  fun theory_to_proof f = app_current (fn int =>
    1.36    (fn Theory thy =>
    1.37 -        if !skip_proofs then SkipProof (History.init (undo_limit int) 0,
    1.38 +        if ! skip_proofs then SkipProof (History.init (undo_limit int) 0,
    1.39            fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy))))
    1.40          else Proof (f int thy)
    1.41      | _ => raise UNDEF));
    1.42 +
    1.43  fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
    1.44    | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
    1.45    | _ => raise UNDEF));
    1.46 +
    1.47  val proof' = proof''' true;
    1.48  val proof = proof' o K;
    1.49  val proof'' = proof''' false o K;
    1.50 +
    1.51  fun proof_to_theory' f =
    1.52    map_current (fn int => (fn Proof prf => Theory (f int prf)
    1.53      | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF
    1.54      | _ => raise UNDEF));
    1.55 +
    1.56  val proof_to_theory = proof_to_theory' o K;
    1.57 +
    1.58  fun skip_proof f = map_current (fn int =>
    1.59    (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
    1.60 +
    1.61  fun skip_proof_to_theory p = map_current (fn int =>
    1.62    (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
    1.63  
    1.64 @@ -408,81 +418,73 @@
    1.65  (** toplevel transactions **)
    1.66  
    1.67  val quiet = ref false;
    1.68 -val debug = ref false;  (* Verbose messages for core exceptions. *)
    1.69 +val debug = ref false;
    1.70 +
    1.71  
    1.72  (* print exceptions *)
    1.73  
    1.74 -fun raised name = "exception " ^ name ^ " raised";
    1.75 -fun raised_msg name msg = raised name ^ ": " ^ msg;
    1.76 +local
    1.77 +
    1.78 +fun with_context f xs =
    1.79 +  (case Context.get_context () of NONE => []
    1.80 +  | SOME thy => map (f (Theory.sign_of thy)) xs);
    1.81 +
    1.82 +fun raised name [] = "exception " ^ name ^ " raised"
    1.83 +  | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
    1.84 +  | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
    1.85  
    1.86 -fun msg_on_debug (THM (msg, i, thms)) =
    1.87 -     if !debug
    1.88 -     then raised_msg ("THM " ^ string_of_int i)
    1.89 -       (cat_lines ("" :: msg :: map Display.string_of_thm thms))
    1.90 -     else raised_msg "THM" msg
    1.91 -  | msg_on_debug (THEORY (msg, thys)) =
    1.92 -     if !debug
    1.93 -     then raised_msg "THEORY" (cat_lines ("" :: msg ::
    1.94 -       map (Pretty.string_of o Display.pretty_theory) thys))
    1.95 -     else msg
    1.96 -  | msg_on_debug (AST (msg, asts)) =
    1.97 -     if !debug
    1.98 -     then raised_msg "AST" (cat_lines ("" :: msg ::
    1.99 -       map (Pretty.string_of o Syntax.pretty_ast) asts))
   1.100 -     else msg
   1.101 -  | msg_on_debug (TERM (msg, ts)) =
   1.102 -     (case (!debug, Context.get_context ()) of
   1.103 -         (true, SOME thy) =>
   1.104 -           let val sg = Theory.sign_of thy in
   1.105 -             raised_msg "TERM"
   1.106 -               (cat_lines
   1.107 -                 ("" :: msg :: map (Sign.string_of_term sg) ts))
   1.108 -           end
   1.109 -       | _ => raised_msg "TERM" msg)
   1.110 -  | msg_on_debug (TYPE (msg, Ts, ts)) =
   1.111 -     (case (!debug, Context.get_context ()) of
   1.112 -         (true, SOME thy) =>
   1.113 -           let val sg = Theory.sign_of thy in
   1.114 -             raised_msg "TYPE"
   1.115 -               (cat_lines
   1.116 -                 ("" :: msg :: map (Sign.string_of_typ sg) Ts @
   1.117 -                  map (Sign.string_of_term sg) ts))
   1.118 -           end
   1.119 -       | _ => raised_msg "TYPE" msg)
   1.120 +fun exn_msg _ TERMINATE = "Exit."
   1.121 +  | exn_msg _ RESTART = "Restart."
   1.122 +  | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   1.123 +  | exn_msg _ Interrupt = "Interrupt."
   1.124 +  | exn_msg _ ERROR = "ERROR."
   1.125 +  | exn_msg _ (ERROR_MESSAGE msg) = msg
   1.126 +  | exn_msg false (THEORY (msg, _)) = msg
   1.127 +  | exn_msg true (THEORY (msg, thys)) =
   1.128 +     raised "THEORY" (msg :: map (Pretty.string_of o Display.pretty_theory) thys)
   1.129 +  | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg
   1.130 +  | exn_msg _ (Proof.STATE (msg, _)) = msg
   1.131 +  | exn_msg _ (ProofHistory.FAIL msg) = msg
   1.132 +  | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
   1.133 +      fail_msg detailed "simproc" ((name, Position.none), exn)
   1.134 +  | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
   1.135 +  | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
   1.136 +  | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
   1.137 +  | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
   1.138 +  | exn_msg true (Syntax.AST (msg, asts)) =
   1.139 +      raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   1.140 +  | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   1.141 +  | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
   1.142 +        with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
   1.143 +  | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
   1.144 +  | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
   1.145 +  | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   1.146 +  | exn_msg true (THM (msg, i, thms)) =
   1.147 +      raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
   1.148 +  | exn_msg _ Option = raised "Option" []
   1.149 +  | exn_msg _ UnequalLengths = raised "UnequalLengths" []
   1.150 +  | exn_msg _ Empty = raised "Empty" []
   1.151 +  | exn_msg _ Subscript = raised "Subscript" []
   1.152 +  | exn_msg _ exn = General.exnMessage exn
   1.153 +and fail_msg detailed kind ((name, pos), exn) =
   1.154 +  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
   1.155  
   1.156 -fun exn_message TERMINATE = "Exit."
   1.157 -  | exn_message RESTART = "Restart."
   1.158 -  | exn_message (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   1.159 -  | exn_message Interrupt = "Interrupt."
   1.160 -  | exn_message ERROR = "ERROR."
   1.161 -  | exn_message (ERROR_MESSAGE msg) = msg
   1.162 -  | exn_message (THEORY (msg, thys)) = msg_on_debug (THEORY (msg, thys))
   1.163 -  | exn_message (ProofContext.CONTEXT (msg, _)) = msg
   1.164 -  | exn_message (Proof.STATE (msg, _)) = msg
   1.165 -  | exn_message (ProofHistory.FAIL msg) = msg
   1.166 -  | exn_message (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
   1.167 -      fail_message "simproc" ((name, Position.none), exn)
   1.168 -  | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
   1.169 -  | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
   1.170 -  | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info
   1.171 -  | exn_message (Syntax.AST (msg, asts)) = msg_on_debug (AST (msg, asts))
   1.172 -  | exn_message (TYPE (msg, Ts, ts)) = msg_on_debug (TYPE (msg, Ts, ts))
   1.173 -  | exn_message (TERM (msg, ts)) = msg_on_debug (TERM (msg, ts))
   1.174 -  | exn_message (THM (msg, i, thms)) = msg_on_debug (THM (msg, i, thms))
   1.175 -  | exn_message Option = raised "Option"
   1.176 -  | exn_message UnequalLengths = raised "UnequalLengths"
   1.177 -  | exn_message Empty = raised "Empty"
   1.178 -  | exn_message Subscript = raised "Subscript"
   1.179 -  | exn_message exn = General.exnMessage exn
   1.180 -and fail_message kind ((name, pos), exn) =
   1.181 -  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;
   1.182 +in
   1.183 +
   1.184 +val debug = ref false;
   1.185 +
   1.186 +fun exn_message exn = exn_msg (! debug) exn;
   1.187  
   1.188  fun print_exn NONE = ()
   1.189    | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
   1.190  
   1.191 +end;
   1.192 +
   1.193  
   1.194  (* apply transitions *)
   1.195  
   1.196 +val quiet = ref false;
   1.197 +
   1.198  local
   1.199  
   1.200  fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =