For some reason, the prefix C-u C-u to M-h M-r never seems to work for me. I'm using Emacs 24.5 (the latest version) and have an up-to-date HOL version.
My solution is to manually toggle quietness with M-h C-q. In other words, to avoid output I press M-h C-q then M-h M-r then M-h C-q. Cheers, Magnus On 2 June 2016 at 05:17, Michael Norrish <michael.norr...@nicta.com.au> wrote: > This behaviour is documented at > > https://hol-theorem-prover.org/hol-mode.html > > Michael > > On 1 Jun 2016, at 23:10, Peter Vincent Homeier > <palan...@trustworthytools.com> wrote: > > Dear Michael, > > I tried using your suggestion > > and it does work as you describe. Thank you! That is very convenient. > > Seeing I've gone so many years without knowing this, perhaps it might be a > good thing to add some mention to the Tutorial or to the Description > manuals? This feature has such an immediately practical value, that I'd like > save others from working without knowing about it. > > Peter > > On Tue, May 31, 2016 at 7:57 PM, Michael Norrish > <michael.norr...@nicta.com.au> wrote: >> >> Dear Peter, >> >> If you use the Emacs mode to select regions and paste them into a *HOL* >> buffer (with M-h M-r), then if you precede that command with two C-u >> "prefixes", you get the toggling of quiet-declarations before and after. >> >> So, when I'm opening many theories all at once, I select the relevant >> block with the usual emacs commands, and then do >> >> C-u C-u M-h M-r >> >> to get "silent" (and quick!) opening. >> >> best wishes, >> Michael >> >> On 1 Jun 2016, at 03:59, Peter Vincent Homeier >> <palan...@trustworthytools.com> wrote: >> >> Dear Mike and Anthony, >> >> Thank you so much for your quick responses! >> >> Mike, it turns out I am using Poly/ML, so your solution using >> PolyML.print_depth does work very well for me. >> >> Anthony, I have checked and your solution using >> HOL_Interactive.toggle_quietdec also works fine. >> >> Since the toggle_quietdec function seems a little simpler (taking just a >> unit argument) and is part of HOL itself, rather than being specific to an >> SML implementation, I think I'll go with that method for now. >> >> Here's an example of its use in the HOLFOOT project: >> http://holfoot.heap-of-problems.org/EXAMPLES/interactive/filter.hol >> >> Mike, congratulations on your retirement! I hope you are finding time to >> do all the things you always wanted to. But I am very glad you're still in >> touch and interested in HOL. >> >> Many thanks to you both, Mike and Anthony! You've saved me literally hours >> of my life. >> >> Peter >> >> >> On Tue, May 31, 2016 at 12:22 PM, Anthony Fox <ac...@cam.ac.uk> wrote: >>> >>> 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 >>> >> >> >> >> -- >> >> >> "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 >> >> >> >> ________________________________ >> >> The information in this e-mail may be confidential and subject to legal >> professional privilege and/or copyright. National ICT Australia Limited >> accepts no liability for any damage caused by this email or its attachments. > > > > > -- > > > "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
