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
