Hi Bill,
You can overwrite the OCaml exception printer if you want, like I do in HOL
Zero in 'exn.ml' and the main build file 'holzero.ml', where the error
message is part of the exception and gets printed out if/when the exception
bubbles to the top. You could do something like this:
let print_exn e =
match e with
Failure msg
-> ........ (* Special printing for Failure exceptions *)
| _ -> Format.print_string (Printexc.to_string e);; (* Otherwise
revert to normal OCaml printing *)
#install_printer print_exn;;
You would get something like this printed out:
Exception: <whatever>
So this doesn't stop "Exception" getting printed out at the start, but you
have control over everything else after that. There is probably also a way
to stop "Exception" getting printed, but I just don't know enough about
OCaml to do this.
Mark.
on 26/7/13 1:48 PM, Bill Richter <[email protected]> wrote:
> Vince, I figured out how to print error messages without double-quotes and
> with actual newlines! This and a lot more is explained in the ocaml doc
in
> "Module Format", which I got the idea to use after looking at Freek's
> miz3.ml. I'd like to get rid of a trailing message Exception: Failure "".
>
> #load "str.cma";;
>
> let StringRegexpEqual r s = Str.string_match r s 0 &&
> s = Str.matched_string s;;
>
> let rec FindMatch sleft sright s =
> let test = Str.regexp ("\("^ sleft ^"\|"^ sright ^"\)") and
> left = (Str.regexp sleft) in
> let rec FindMatchPosition s count =
> if count = 1 then 0 else
> try
> ignore(Str.search_forward test s 0);
> let endpos = Str.match_end() in
> let rest = Str.string_after s endpos and
> increment =
> if StringRegexpEqual left (Str.matched_group 1 s) then -1 else 1
> in
> endpos + (FindMatchPosition rest (count + increment))
> with Not_found -> open_box 0; print_string
> ("\n no matching right bracket operator "^ sright ^
> " to left bracket operator "^ sleft ^" in "^ s ^"\n");
> close_box (); print_newline (); fail() in
> FindMatchPosition s 0;;
>
> let s = ";abc]edf" in Str.string_before s (FindMatch "\[" "\]" s);;
> let s = ";1234[abc]]xyz" in Str.string_before s (FindMatch "\[" "\]" s);;
> let s = ";12345[abc]lmnop]xyz" in Str.string_before s (FindMatch "\[" "\]"
> s);;
> let s = ";123456[abc]lmnop[abc]pqrs]xyz" in Str.string_before s (FindMatch
> "\[" "\]" s);;
> let s = ";123[45[abc]lm]nop!!!!!!!!!!]xyz" in Str.string_before s
(FindMatch
> "\[" "\]" s);;
> let s = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]xyz" in Str.string_before
s
> (FindMatch "\[" "\]" s);;
> let s = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!![]xyz" in Str.string_before
s
> (FindMatch "\[" "\]" s);;
>
> Output:
>
> val it : string = ";abc]"
> # val it : string = ";1234[abc]]"
> # val it : string = ";12345[abc]lmnop]"
> # val it : string = ";123456[abc]lmnop[abc]pqrs]"
> # val it : string = ";123[45[abc]lm]nop!!!!!!!!!!]"
> # val it : string = ";123456[abc]lmn[op[abc]pq]rs!!!!!!!!!!]"
> #
> no matching right bracket operator \] to left bracket operator \[ in xyz
>
> Exception: Failure "".
>
> I'm responding to your post on Jul 2:
>
>> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>>
>> with Not_found -> failwith("missing initial \"proof\" or final \"qed;\"
> in "^ s)
>>
>> It would be nice to at least have an actual newline before the string
> s.
>
> Not to my knowledge.
>
> Here's another example:
>
> let rec FindSemicolon s =
> try
> let rec FindMatchPosition s pos =
> let start = Str.search_forward (Str.regexp ";\|\[") s pos in
> if Str.matched_string s = ";" then start
> else
> let rest = Str.string_after s (start + 1) in
> let MatchingSquareBrace = FindMatch "\[" "\]" rest in
> let newpos = start + 1 + MatchingSquareBrace in
> FindMatchPosition s newpos in
> FindMatchPosition s 0
> with Not_found -> open_box 0; print_string
> ("\n no final semicolon in " ^ s ^"\n");
> close_box (); print_newline (); fail();;
>
> let s = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![];xyz" in
> Str.string_before s (FindSemicolon s);;
> let s = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]xyz" in
> Str.string_before s (FindSemicolon s);;
>
> Output:
>
> val it : string = "123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]"
> #
> no final semicolon in 123456[abc]lmn[op[a; b; c]pq]rs!!!!!!!!!![]xyz
>
> Exception: Failure "".
>
> Thanks for writing you ZOL tutorial. I'll read it avidly.
>
> --
> Best,
> Bill
>
>
>
----------------------------------------------------------------------------
> --
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
