>> 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?
HOL Light's nice, simple and compact, but is a bit light on source code comments. It's got a snappy little lexer, implemented towards the start of parser.ml. If you can't understand this, then take a look at HOL Zero's. Part of the point of HOL Zero is to have more explanation in the source code, so that non-experts stand a chance of understanding what's going on. Another is that quotation syntax is carefully designed to avoid issues related to parser/printer completeness/soundness, so that any valid HOL name can be parsed in and unambiguously pretty printed. So the lexer, implemented in lexer.ml, is more lengthy but is well commented. >> 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. Well, it's very simple pretty printing. It's still pretty printing though. > 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 "". What about instead of printing out your failure message followed by using fail(), just using failwith applied to a string argument that is your failure message? >> 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. Yes, but 'print_string' and 'print_newline' are in *both* modules: Pervasives and Format. All the other formatting stuff is not in Pervasives. Mark. ------------------------------------------------------------------------------ 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
