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
