Hello Bill, The Tuareg mode I mentioned in my earlier email takes care of OCaml indentation, OCaml syntax highlighting (not for HOL Light syntax), and provides key bindings to send commands to the OCaml toplevel (essentially HOL Light).
Regards, Petros On 24/01/2013 03:19, Bill Richter wrote: > Marko, Petros & Ramana, I use Emacs & miz3, with a minimal interface > hol_light/RichterHilbertAxiomGeometry/hol-light-fonts.el > which mostly allows writing HOL Light code with math characters. The > Isabelle folks are phasing out ProofGeneral in favor of jedit. I would like > to have automatic indentation, so TAB would move you where in the correctly > indented place. I've seen this for Scheme code. I imagine that's only a few > lines of Emacs code, but I haven't written it. Another Emacs point is that > evaluating code in an Emacs shell is a good idea, because you can then look > at thousands of lines of output: there's no scroll limit. Freek's paper > arxiv.org/pdf/1201.3601 sorta gives the impression that you need an interface > to use miz3, but you can just paste code from your editor into the window > running ocaml. I don't know what the HOL4 Emacs support does. > -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: [email protected] --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnnow-d2d _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
