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<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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.
------------------------------------------------------------------------------
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
