Hi Bill, > Thanks, Mark! That sounds like a good tip, but can you be more specific? I > produce error message with this function > > let PrintErrorFail s = > open_box 0; print_string s; close_box (); print_newline (); fail();; > > .... > But I only want to change the OCaml exception printer for my function > PrintErrorFail.
You put a call to PrintErrorFail where the "...." was in my last email, i.e. in the pretty printer for exceptions. Don't put it in each function - just raise the exception in each funciton and let the pretty printer print it out when it bubbles to the toplevel. So in each function there is no need to have "try ... with ... -> PrintErrorFail" in each function - instead you have "try ... with ... -> failwith (....the error message that you want...)". Take a look at HOL Zero if you want to see it in practice. Like I said, see 'exn.ml' and holzero.ml' (although these do it for my own HolFail exceptions, not for Failure exceptions). And take at look at other files, like 'lib.ml' to see exceptions getting raised and trapped. > BTW I do not understand why this works, why I don't have to say > Format.open_box and Format.close_box, > which would follow Freek's miz3.ml usage. I know print_string and > print_newline are pervasive, so you didn't need to write > Format.print_string. This is about modules. Things declared inside the Format module would normally need to be prefixed by their module name, but a module can be "included" or "opened" to avoid having to use the module prefix. John "includes" the 'Format' module in printer.ml, so you don't have to prefix from that point onwards. > BTW do you understand either of the undocumented Ocaml features that Freek > uses, Toploop or Object.magic? Is there an Ocaml list I ought to posting > questions on instead of hol-info? The OCaml developers want to keep these modules (by the way, it's Obj not Object) low key and don't publish any details about them. OCaml is used in the implementation of OCaml (!), and as I understand it, they exist for this purpose. The only source of info I can find is by Google searches. I only know a bit about them, but enough to use them in my Tactician utility. Grep Tactician's source code for Obj and Toploop if you want to find out more. Mark. ------------------------------------------------------------------------------ See everything from the browser to the database with AppDynamics Get end-to-end visibility with application monitoring from AppDynamics Isolate bottlenecks and diagnose root cause in seconds. Start your free trial of AppDynamics Pro today! http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
