I use Ramana’s HOL mode for Vim, shortcut “hl”. That makes use of HOL_Interactive.toggle_quietdec
For example, you can do > HOL_Interactive.toggle_quietdec(); > open prim_recTheory pairTheory listTheory rich_listTheory; > open ... > HOL_Interactive.toggle_quietdec(); The advantage of the Vim shortcut is that it also loads all of the theories beforehand. I believe there is something similar for the Emacs mode. Anthony > On 31 May 2016, at 16:39, Peter Vincent Homeier > <palan...@trustworthytools.com> wrote: > > Very often I wish to work in an existing theory script file which begins with > a number of files being opened, e.g., > > open prim_recTheory pairTheory listTheory rich_listTheory; > open combinTheory; > open listLib; > open pred_setTheory pred_setLib; > open numTheory; > open numLib; > open arithmeticTheory; > . . . > > But for theories that contain hundreds or thousands of theorems, this prints > out each theorem in full, which can take tens of minutes of my time while I > am waiting to begin work, and theorems that I already know are just spilling > by. > > Clearly this is not practical. What do other people do to speed this up, so > you can get into your theory and start work? Is there any way to enter the > defined names of an existing theory, like arithmeticTheory, to the current ML > session without printing all of them, which is what takes such a long time? > I'd like to use something like > > open_silently arithmeticTheory; > > which would be functionally equivalent to "open", but would print none of the > values it is introducing. > > What do people do to get around this problem? Or do they just live with it? > Would "open_silently" have to be added to the Standard ML implementation? > > Peter > > > "In Your majesty ride prosperously > because of truth, humility, and righteousness; > and Your right hand shall teach You awesome things." (Psalm 45:4) > ------------------------------------------------------------------------------ > What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic > patterns at an interface-level. Reveals which users, apps, and protocols are > consuming the most bandwidth. Provides multi-vendor support for NetFlow, > J-Flow, sFlow and other flows. Make informed decisions using capacity > planning reports. > https://ad.doubleclick.net/ddm/clk/305295220;132659582;e_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interface-level. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multi-vendor support for NetFlow, J-Flow, sFlow and other flows. Make informed decisions using capacity planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
