Mark, thank you very much! You gave me a good idea, to try to use the top of
update_database.ml directly:
(* Execute any OCaml expression given as a string. *)
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
And you've explained it:
Roughly speaking it takes a string, turns it into lexical tokens, turns
this into abstract syntax and then executes it.
I'll look at your HOL Zero source code for extra info.
HOL Light and HOL Zero don't use OCaml's lexing facilities, but
implement their own from scratch.
Wow, I didn't know that! Where can I learn about HOL Light lexing facilities?
'failwith' is part of OCaml itself, but 'fail' is a just a HOL Light thing.
Thanks!
All exceptions are pretty printed in OCaml,
I don't think that's right. Before I wrote my
let PrintErrorFail s =
open_box 0; print_string s; close_box (); print_newline (); fail();;
I was always getting strings with double-quotes and \n instead of newlines when
I used failwith.
and I thought the whole point of your post was that you weren't
happy with this pretty printing for Failure exceptions, and so I
explained how to override it just for Failure exceptions and keep
the pretty printer for all other exceptions exactly the same.
I wasn't happy with how failwith printed any error message, and the main
exception for me is Not_found. Now my only problem is the minor one of seeing
Exception "".
at the end. On to a minor point.
Yes, the use of the "Format" prefix in HOL Light's make.ml is
unnecessary because it's already included as a result of printer.ml
in hol.ml. But it does no harm being there.
Regarding what the OCaml reference manual says: OCaml's Pervasives
module is initially opened, but not its Format module.
Ah, but I think section 20.2 Module Pervasives (p 318) says that print_string
and print_newline are pervasive anyway, even though, as you say, the entire
Format module is not opened.
--
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
