Mark, I now understand your HOLZero/print_exn idea, and it works pretty well:
exception Readable_fail of string;; let PrintErrorFail s = raise(Readable_fail s);; let print_exn e = match e with | Readable_fail s -> print_string s | _ -> print_string (Printexc.to_string e);; #install_printer print_exn;; Now PrintErrorFail gives me nice error messages, without double-quotes and with real newlines, e.g. # Exception: no matching right bracket operator \] to left bracket operator \[ in xyz . # Exception: missing initial "proof" or final "qed;" in !m n. ~(n = 0) ==> ((m MOD n) MOD n = m MOD n) prooof intro_TAC !m n, H1; mp_TAC_specl [m; n; 1] MOD_MOD; fol H1 MULT_CLAUSES MULT_EQ_0 ONE NOT_SUC; qed; . So you were mostly right earlier: > and I thought the whole point of your post was that you weren't > happy with this pretty printing for Failure exceptions, Yes! But I thought not, because I didn't understand that failwith just raises the exception Failure. > and so I explained how to override it just for Failure exceptions Yes, and that works great! Thanks. > and keep the pretty printer for all other exceptions exactly the > same. But it's not exactly the same. Run the eval code from http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html#toc9 and you can then get eval [("x", 1.0); ("y", 3.14)] (Prod(Sum(Var "z", Const 2.0), Var "y"));; Exception: Unbound_variable("z"). But normally this exception would be printed Exception: Unbound_variable "z". That's not a big difference, right? But it's some change. What really excites me is this: maybe you can generalize your print_exn to improve the pretty-printing of all HOL Light exception string error message. I looked through all your Tactician sources for uses of Toploop, Obj.magic and Lexing. Can you explain if this is a problem for Freek and I, from holzero-0.6.1/Bounty.txt: - circumventing the ML language proper or its type system (e.g. 'Obj.magic'); Carl Witty [16-09-2010] - for exposing how 'Obj.magic' can be used to create arbitrary theorems It all looked interesting, such as this from termparser.ml, which looks like something that Freek posted he was interested in: (* This file overwrites the existing HOL Light term parser with a version *) (* that stores the inputted quotation string in a dynamic lookup tree. The *) (* idea is that this string can be looked up when the term gets pretty *) (* printed, so that it has all the type annotations of its original input. *) (* This gets around the fact that the HOL Light term pretty printer never *) (* annotates terms with their types, and so will often output ambiguous term *) (* quotations that do not get parsed back in correctly. *) I saw you borrowed the update_database.ml `exec' in mlconcrete.ml, but I couldn't understand what you did with it. Just take the first time you used `exec': exec ("type env_t = { values: (path_t * value_description) tbl;\n" ^ (if (let v = String.sub Sys.ocaml_version 0 4 in v = "3.09" or v = "3.10") then "" else " annotations: dummy;\n") ^ " constrs: dummy; labels: dummy; types: dummy; modules: (path_t * module_type) tbl; modtypes: dummy; components: dummy; classes: dummy; cltypes: dummy; summary: dummy};;");; Can't you just evaluate this command yourself without `exec'? At other times, it looked like you needed it, especially in autopromote.ml, where I think cmd is a string that you're getting from somewhere else: let rec promote_value0 verbose (name,t,vd) = match (promotion_command "" (name,vd)) with Some cmd -> if (t > !bulkpromoted_value_tstamp) && not (dltree_mem t !handpromoted_values) then ((if verbose then (print_string "Promoting value \""; print_string name; print_string "\"\n")); exec cmd; last_promoted_value := name) | _ -> ();; -- Best, Bill ------------------------------------------------------------------------------ Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info