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;
. . .
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
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_quiet
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
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 imme
This behaviour is documented at
https://hol-theorem-prover.org/hol-mode.html
Michael
On 1 Jun 2016, at 23:10, Peter Vincent Homeier
mailto:palan...@trustworthytools.com>> wrote:
Dear Michael,
I tried using your suggestion
and it does work as you describe. Thank you! That is very convenient.
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,
Mag
