summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Thu, 18 Aug 1994 17:53:28 +0200 | |

changeset 545 | fc4ff96bb0e9 |

parent 544 | c53386a5bcf1 |

child 546 | 36e40454e03e |

Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
from prove_goalw

src/Pure/goals.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/goals.ML Thu Aug 18 17:50:22 1994 +0200 +++ b/src/Pure/goals.ML Thu Aug 18 17:53:28 1994 +0200 @@ -194,18 +194,19 @@ (case Sequence.pull (tapply(tac,st0)) of Some(st,_) => st | _ => error ("prove_goal: tactic failed")) - in mkresult (true, cond_timeit (!proof_timing) statef) end; + in mkresult (true, cond_timeit (!proof_timing) statef) end + handle e => (print_sign_exn (#sign (rep_cterm chorn)) e; + error ("The exception above was raised for\n" ^ + string_of_cterm chorn)); + (*Version taking the goal as a string*) fun prove_goalw thy rths agoal tacsf = let val sign = sign_of thy val chorn = read_cterm sign (agoal,propT) - in prove_goalw_cterm rths chorn tacsf - handle ERROR => error (*from type_assign, etc via prepare_proof*) - ("The error above occurred for " ^ quote agoal) - | e => (print_sign_exn sign e; (*other exceptions*) - error ("The exception above was raised for " ^ quote agoal)) - end; + in prove_goalw_cterm rths chorn tacsf end + handle ERROR => error (*from read_cterm?*) + ("The error above occurred for " ^ quote agoal); (*String version with no meta-rewrite-rules*) fun prove_goal thy = prove_goalw thy [];