Ralf Jung writes:
> Ah, that's a good point. I should try that one time. Thanks for the hints!
And if you define that procedure (changing to the import all
file, doing C-c C-b there) as an emacs macro, then you can start
the whole recompilation with just one key stroke.
Hendrik
__
>> OK, how about creating a emacs macro that does C-c C-b in the
>> file that imports everything? You can easily bind this to F9 or
>> or any other key - then you get everything with just one
>> keystroke!
>
> That wouldn't be in background though, right? It'd stop interactive
> mode in the file
Ralf Jung writes:
>> - you start scripting in file A (for instance to fix a proof)
>> while compile-everything is still in progress? Have 2
>> compilations in parallel or abort compile-everything?
>
> Aborting when the active file is changed sounds fine. I guess that's
> what vio2vo also does
Ralf Jung writes:
> To follow-up on this: I guess what I am asking for is some command in PG
> to say "now please compile everything", that command should be as smart
> about compilation as the compilation on import. It should behave just as
> if I would step over a file that "Require"s everythin
Ralf Jung writes:
> (and from what I see it do), "Keep Going" is about compiling more of the
> dependencies of the current file even if other dependencies failed.
Right.
> What I am looking for is something that compiles more of the current
> *project* (i.e., things listed in the _CoqProject),
Ralf,
your first email got through and thanks for you positive
feedback!
I have the impression that you have not read any documentation
about the quick compilation feature. The CHANGES file is
unfortunately not the place to describe a complex feature
completely, but it contains a pointer: "See th
Hi,
I opend a PR for comments with a first version of -quick support,
see the quick branch on g...@github.com:hendriktews/PG.git. The
solution has advantages over using make because the quick options
accept an up-to-date .vo file for prerequisites (make insists on
producing .vio files for all file
Pierre Courtieu writes:
> I think there are people using it but I suspect it is only by lack of _
> CoqProject file.
I don't quite understand, how is a missing _CoqProject file
connected with using sequential compilation?
> Do we support vio compilation?
No, see the other thread.
> If we do
Hi,
Pierre Courtieu writes:
> Do we support vio compilation?
No. I started to think about it and I would like to hear about
your opinion here.
I've only done a few experiments so far with -quick,
-schedule-vio2vo and -schedule-vio-checking. Therefore, if you
made different observations, please
Hi,
how long do we want to keep the sequential and blocking
compilation implemented in coq-seq-compile.el? Is anybody
actually using it?
I am asking because I am not really motivated to maintain this
code. If you look at the 8.5 changes, many things had to be done
twice, in coq-seq-compile and in
Hi,
"Paul A. Steckler" writes:
> Well, the current goal should always be shown, unless there's a bug.
What if the user deletes the emacs window containing the current
goal because he temporarily wants to use that screen space for
something else? I used to do this quite often when I needed to
lo
Hi,
>> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler :
>>> The code in generic/proof-tree appears to rely on proof shell modes.
>>>
>>> Is the `prooftree' tool in common use among Coq users?
I used it all the time ;-)
For coq, prooftree needs the following:
1) a unique proof goal identifier
2) t
Hi,
I don't have the knowledge to join the discussion about the
relative benefits of different emacs package distribution
systems.
I once made significant contributions on PG and will join
whatever the active majority here decides.
At some stage I also prepared a PG debian packages - this was
si
Hi,
thanks a lot for taking the initiative!
Clément Pit--Claudel writes:
> changes (we would need to migrate once and for all).
I haven't contributed for a while and I am unsure if I will find
time in the future, therefore I don't know if I am eligible to
take part in the discussion. However,
Hi,
I fixed #467 now such that the menu entries (including "Time
commands") do work. If you type "Time" on your own, you have to
use customize yourself, see ticket #467. I hope this is
sufficient for closing the bug.
Bye,
Hendrik
___
ProofGeneral-devel
Hendrik Tews writes:
I don't think using defpacustom for project-filename is a good
idea. This way it appears in the menu and when you enable it,
coq-project-filename is set to t.
I fixed the t setting with fixing the :type of
coq-project-filename. Now it can stay in the
Hi Pierre,
I don't think using defpacustom for project-filename is a good
idea. This way it appears in the menu and when you enable it,
coq-project-filename is set to t.
Can defpacustom handle string options, such that the user is
queried for a string, when he enables the menu entry?
Bye,
Hend
Pierre Courtieu writes:
> - similarly for the coq/faq: wouldn't it be better to integrate
> this in the user manual and have then a "coq faq" link on the
> web page?
>
I don't understand this one. Do you mean in the coq user manual?
No, my suggestion was to integrate coq/faq
Pierre Courtieu writes:
Date: Fri, 5 Jul 2013 16:04:43 +0200
Subject: Re: [PG-devel] Move to Github
I don't mind changing the name of coq.el into pg-coq.el. Will it break
something?
You mean in the Proof General distribution, not in the Coq
distribution, right?
> Hend
Hendrik Tews writes:
Regarding the 4.3 release: ...
I have another issue that I would like to see resolved in 4.3:
The feature name conflict with Coq, see
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2012/000241.html
Both Proof General and Coq install coq.el (and some other files
Hi,
I am happy to see Pierre you back on this list and back
committing to Proof General.
Regarding the 4.3 release: There are some indentation bugs in the
tracker. Pierre, could you spend some time for them?
I intend to fix #467 and have a look at #460.
Does anybody else use the new parallel c
David Aspinall writes:
This fix was helpful but unfortunately means that developers are more
likely to introduce bugs unless they run
make clean; make check
I agree. But even before the change we had now and then
compilation errors in the repository.
>From my point of view the com
Hi,
the Proof General releases do always contain a symlink
ProofGeneral --> ProofGeneral-X.Y, which, ahem, is a bit in the
way when creating debian packages.
What is the reason for having this symlink in the tar archive?
Bye,
Hendrik
___
ProofGeneral-
Hi,
I spend some time to find a fix for tickets #458. The problem is
that special-display-regexps is obsolete in 24.3, while its
replacement, display-buffer-alist was only introduced in 24.1 and
not fully functional before 24.3. Writing compatible code for
emacs 23 and 24 without obsolete warning
I believe all Proof General versions (including the latest trunk)
show the timing in the *goals* buffer when you use them with Coq
8.3pl4 or earlier. If you have more than one subgoal the timing
is shown only when coq-hide-additional-subgoals is off. Then the
*goals* buffer looks like
###
I remember how PG used to behave, but I do not recall which version it was.
I started using Coq at version 8.3pl2, or there-abouts, so I can try to
8.3pl3 was released in December 2011, so it was probably Proof
General 4-2pre111207 or earlier.
Hendrik
__
Hi,
somebody wrote in the bug tracker:
Btw, is it possible to get me added to the cc list for this bug?
(jasongross9+PG AT gmail DOT com)
I don't know how. I therefore suggest to continue the discussion
here at ProofGeneral-devel.
I have some suspicions, what caused the timings to disa
Hi,
currently, proof-shell-filter looks for urgent messages before
looking for errors. Moreover, if an urgent message is found, it
searches for errors only in the output that follows the urgent
message.
This behavior is responsible for issue #463, where Coq outputs an
error before a warning and
Hi,
do we have a support problem for Proof General?
I am asking because we have issues in the tracker that are quite
old and nobody seems to care... for instance #460 or #463 to
which I gave partial answers today.
Do we have a lack of developers or do the developers not like to
comment on issues
Hi,
is anybody actually using prooftree with the cvs head of Proof
General?
For supporting bullets, braces and "Grab Existential Variables" I
would like to make several commits that break compatibility with
the current release of prooftree. A suitable prooftree release
will follow within a month
Hi,
currently editor backup files are deleted by make clean. I find
this unfortunate, because I have to use make clean quite often to
remove elc files. If nobody disagrees, I move the removal of *~
to the distclean target.
Bye,
Hendrik
___
ProofGeneral
I wrote:
here is a patch that solves the problem for me. Any comments?
I committed now. I deleted the argument of proof-shell-filter, to
make sure, nobody will use it. Reasons are described in the doc
comments.
Hendrik
___
ProofGeneral-devel mailing
David Aspinall writes:
At a quick glance this looks like a reasonable way to fix without
messing with the current filter code. Luckily, I don't think the str
argument is used.
I'm not completely clear on the error case, is the
idea just to give up if we hit an error in some cal
Stefan Monnier writes:
I think this deserves an Emacs bug report.
see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400
There are definitely some documentation problems.
process-send-string is not mentioned as function that might
trigger a filter call.
I think many packages are vulnerab
Hi,
here is a patch that solves the problem for me. Any comments?
Bye,
Hendrik
Index: generic/proof-shell.el
===
RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v
retrieving revision 12.15
diff -u -r12.15 proof-she
David Aspinall writes:
Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?
I don't use the debugger, I let certain functions insert st
Hi,
sometimes I see prooftree crashes with a cold disk cache (eg
after reboot or after "sync; sudo sh -c 'echo 3 >
/proc/sys/vm/drop_caches'").
What apparently happens is that at some stage process-send-string
blocks because the pipe to prooftree is full. This happens inside
proof-shell-filter,
David Aspinall writes:
> I just committed the first version of parallel background
> compilation for Coq.
It sounds very useful! Are there some Coq users who are testing for you?
Not that I know.
H.
___
ProofGeneral-devel mailing list
Proo
Pierre Courtieu writes:
Since double hit terminator is more or less an alternative to electric
terminator, I have put them side by side in coq menu, to see if people
OK, I thought "double hit" would modify the behavior of electric
terminator.
like it, but I did not make it geenric yet
Hi,
I just committed the first version of parallel background
compilation for Coq. It is disabled by default in favor of the
old synchronous compilation method.
Parallel compilation required one fundamental and one minor
change in the general proof shell treatment, see below.
If you want to try
Hi,
I just noticed that there are a view boolean settings in the Coq
menu which are not done via defpacustom and which are therefore
not in the Settings submenu. Is there a reason, why "Toggle
tooltips", "Electric Terminator" and "Double Hit Electric
Terminator" are not in the Settings submenu?
I
Hi,
I just came across proof-shell-pre-interrupt-hook. I can't find
any location where this hook is run. Am I missing something?
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo
Hi,
I am missing the documentation comment for
pg-finish-tracing-display. What is it used for?
(As you may have noticed I am implementing parallel background
compilation for Coq. It is working already if there is no error
in the compilation itself. I am now trying to keep the queue
region alive w
Hi,
David, is there anything left to do before you can do "make
release"? Maybe I or somebody else could help?
(My Coq project is now so large that the sequential blocking
compilation really sucks. I would really like to start now with
rewriting the compilation with parallel background jobs.)
By
Hi,
there are no issues left with milestone 4.2. Nobody has committed
changes for one week. David, I believe, you can release now.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listin
Hi,
how can I add my email address (which is different from coquser)
to an existing bug report? Having to click all issues, only for
checking if somebody has answered, is really not acceptable.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGen
Hendrik Tews writes:
- support for braces and bullets
This requires more work than I thought. I have to postpone this
to October. Given that only few people use braces/bullets
(because they are new) and even fewer use Prooftree, it doesn't
make sense to delay the release of Proof Ge
In addition to Davids list we should fix the conflict between
proof-electric-terminator and coq-colon-self-insert, that I
reported yesterday on this list.
issue #449
- Proof appears as command in the proof tree
issue #450
- support for braces and bullets
issue #451
H.
David Aspinall writes:
I'd like to push the button on this soon, so I think we should stop
adding new features/hacks to the CVS head for a while...
How about Hol light? Would you release 4.2 with the current
partial hol light support enabled? Or would you put hol-light
into comments in gen
Pierre Courtieu writes:
(define-key coq-mode-map (kbd ".") 'self-insert-command)
(define-key coq-mode-map (kbd ";") 'self-insert-command)
No, I want the default Proof General electric terminator thing,
where one "." asserts up to the last phrase. Sorry for being not
clear enough about this
Hi,
coming back from holiday, I got the new double hit terminator
feature on checkout. Being not open-minded about new things, I
wanted to disable it. But how to do that?
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
The main problem with your solution is that for the moment pg coq needs to
see the informations that were present in the prompt before a command was
issued to know how to back just before this command. Therefore if we want
to be able to backtrack inside the chunks we need to read al
Hi,
I was recently a bit annoyed by the time Proof General needs to
process my Coq files. A simple measurement showed that Proof
General has only one third or less of the speed of coqc.
I therefore tested the following idea: When Proof General
processes larger chunks, it can send proof scripts a
Ulrich Mueller writes:
Byte-compilation of ProofGeneral fails if Emacs was configured with
option --without-x, because image-load-path is not defined in this
case:
Which emacs version are you using?
Could anybody explain me, why I cannot reproduce the problem? I
tried with emacs23-nox
Pierre Courtieu writes:
2012/6/6 Stefan Monnier :
>
> Another take on it is that the two teams should join their efforts.
I already asked why this old file is still in coq distribution. The
answer was: some people just want to open coq file for syntax
highlighting. For them sta
Stefan Monnier writes:
> Or by those who designed Emacs with a flat namespace for features and
> library files...
Ahem!
Please don't put .../ProofGeneral/coq in the load-path, and then simply
do (require 'coq/coq).
Where is this documented? I would even say that the Elisp manual
Hendrik Tews writes:
This is going to be a problem for those that want to use a
manually installed Coq 8.4 with a Debian installation of Proof
General. In Debian, manually installed stuff has precedence, so
when proof-site requires 'coq, Emacs will actually load coq.el
fro
Hi,
both Proof General and Coq install and provide Emacs files and
features for 'coq, 'coq-db and 'coq-syntax (the latter two are
actually old versions from Proof General).
This is going to be a problem for those that want to use a
manually installed Coq 8.4 with a Debian installation of Proof
Ge
I wrote:
> I believe setting cursor-in-non-selected-windows to nil (and
> leaving cursor-type unchanged) in *goals* and *response* would be
> more appropriate.
I've committed this change yesterday.
David, quite some changes accumulated since Release-4-2pre120430.
Do you think you can
Hi,
what is the rationale for overriding the user preference for
cursor-type in *goals* and *response* ?
I would expect that people who really want different cursors
within one frame, set the cursor appearance in their personal
configuration, eg via proof-shell-init-hook.
I believe setting curs
Hi,
I still don't like the fact that Proof General moves point to the
beginning of the buffer, when the buffer is automatically
retracted, because I change the current scripting buffer. See
also the old discussion at
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html
I have n
Hi,
my last commit fixes the problem that Proof General was screwing
up the displayed buffers when switching the active scripting
buffer with Coq. Let me explain:
I use the 2-windows mode of Proof General, usually one frame
showing the current scripting buffer and either *goals* or
*response*. L
Hi,
if nobody disagrees I am going to remove coq/coqtags because the
Coq distribution contains its own coqtags.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-dev
Hi,
I just merged the ProofTreeBranch into the main trunk. Hopefully
I didn't break anything.
If you want to try it you have to install Coq 8.4 beta (from
http://coq.inria.fr/coq-84) or a recent development version of
Coq and Prooftree (from http://askra.de/software/prooftree/). The
Prooftree web
Hi,
for Coq I implemented a setting that dynamically changes
proof-shell-end-goals-regexp and thereby either hides or shows
additional subgoals (see my commit this morning). If other proof
assistants do also want this, we could generalize the change and
move the setting into the Proof General menu
Hi,
if you would like the virtual cursor of the vcursor package being
visible also inside the locked region you can put the following
as fix into your .emacs:
(defadvice vcursor-move (after vcursor-overlay-set-priority activate)
"Set a high priority for the vcursor overlay to make the vcursor v
David Aspinall writes:
I plan to announce a little bit more widely later this week, please
let me know asap if there are any hiccups.
I haven't seen an announcement of Proof General 4.1 on coq-club.
If nobody else wants to do this I'll post something this
afternoon.
Bye,
Hendrik
Tom Prince writes:
>Some developments don't fully qualify their imports, and so coqdep gives
>warning about ambiguous imports. Allow these developments to use
>auto-compilation mode anyway.
Sorry about the delay, I somehow forgot about the issue. It's now
fixed in the reposi
That sounds OK, except there shouldn't be quotes in there:
Sure, I've committed the change now, please test.
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> If nobody objects, I'll adopt solution 1 (see #421 for solution 2):
Fixed now in cvs, please test.
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Tom Prince writes:
>> Does anybody use -I ... -as ... ?? Does anybody has an opinion
>> about whether Coq Proof General should support -I ... -as ... ??
If somebody needs it later, we can
always add it.
Of course, but I don't want to make an incompatible change, when
we add -I .
Pierre Courtieu writes:
2011/9/10 Erik Martin-Dorel :
> 3. Finally, it seems the function `proof-shell-exit' raises
> systematically an unexpected error.
>
> To reproduce it, run the (Coq) prover, then try:
> [M-: (setq debug-on-error t) RET]
> [C-c C-x]
I have noticed t
Tom Prince writes:
Some developments don't fully qualify their imports, and so coqdep gives
warning about ambiguous imports. Allow these developments to use
auto-compilation mode anyway.
Could you describe an example? What is coqdep printing in these
cases?
-(if (string-match "^
Tom Prince writes:
On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews
wrote:
> * With the patch, coq-load-path covers the options -I and
> -R ... -as ... With a minor change we will also get -R ...
> However, -I ... -as ... would still be unsupported.
-R only ac
I am also in favor of releasing this patch, as it doeas not seem ro
break the users old configuration settings using coq-prog-args (does
it?).
No, as long as coq-compile-before-require is nil.
What do you think about -I ... -as ... ? Do people use it?
Bye,
Hendrik
__
Tom Prince writes:
Make coq-load-path accept either strings (which are passed "-I" options)
or conses of strings (which are passed as "-R" options).
Thanks a lot for your patch. This has been on my todo list,
however, I never looked at this point, because I don't use -R (yet).
Before I co
Hi,
the mercurial view of the Proof General cvs repository at
http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/
seems to be dead. Is there any alternative?
If not I would volunteer to set up viewvc and cvshistory, but for
that I would need access to the raw *,v rcs files. Of course a
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional
last column (not currently used but was in the past).
Just committed.
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailm
Stefan Monnier writes:
But admittedly, it also means that it's mostly useless as well: if your
Coq file is called ".v" the completion will stop at ".v" in any case,
No, it won't, because Coq does also generate ".glob" files.
Additionally completion-ignored-extensions are hidden by defaul
David Aspinall writes:
Hendrik, do you want to add this for Coq?
Yes, as soon as we agree on how to it best.
I don't think it needs to
be added to generic mechanisms since Coq is the only supported prover
that compiles files at the moment.
You are right. However, completion-ignor
David Aspinall writes:
> Yes, but this will not be easy. The problem is the
> following: I temporarily have to stop the proof-shell main
> loop if the next item in proof-action-list is a Require and
> if the corresponding compile job has not been finished.
>
> Simply calling ac
Pierre Courtieu writes:
> Emacs is locked because I avoided all synchronization trouble and
> call coqdep and coqc synchronously. All this happens before the
> asserted items are put into proof-action-list.
>
> This is not optimal, but for a first version it is hopefully ok.
David Aspinall writes:
> In order to do some changes in A the user unlocks A, thereby
> retracting B. If B is not visible, then the point in B will
> be moved to the beginning of the buffer.
[ is there a difference between what happens with B invisible
and visible? ]
Yes, if B is
David Aspinall writes:
> why does proof-retract-until-point make the current buffer
> the active scripting buffer? It seems that Proof General
> anticipates that the user starts asserting immediately
> afterward.
Not particularly, this is to enforce the simplifying invariant
th
Hi,
Pierre Courtieu writes:
Is there a reason why emacs completely hangs when auto compilation is
working?
You mean emacs is locked until compilation is finished and all
asserted items are in the queue region? Or do you mean something
else?
Emacs is locked because I avoided all synchr
Hi,
in its default setting (which is locked) proof-follow-mode
ensures that point is at the end of the locked region. Consider
the following case: The user switches to buffer A, which is a
locked ancestor of the current scripting buffer B. In order to do
some changes in A the user unlocks A, there
Hi,
why does proof-retract-until-point make the current buffer the
active scripting buffer? It seems that Proof General anticipates
that the user starts asserting immediately afterward.
However, it might also be the case that the user does only make
some very small change and then goes to the pre
the branch point of ProofTreeBranch,
you have to append them manually. To do this, generate the
ChangeLog for the main trunk and copy everything starting with
the entry ``2011-04-15 Hendrik Tews''.
Alternatively you can use the rcs2log option ``-v''. This
generates a ChangeLog containin
Hi,
I prepared the first release of prooftree, please have a look at
http://askra.de/software/prooftree/
Installation is a bit tedious, because you have to manually
compile and install Proof General, Coq and prooftree itself. The
prooftree-bundle that I am releasing contains a snapshot from the
P
Hi,
inspired by PVS, I started to work on an external visualization
of the proof tree. I have now a basic version running, see below.
It is implemented in GTK and Ocaml, integrated with Proof General
and works with a patched version of Coq.
I believe it's time now to share the code with others a
Pierre Courtieu writes:
I agree with the idea, but should we really modify
completion-ignored-extensions by ourselves?
That's the usual practice. Here emacs -q -no-site-file gives
completion-ignored-extensions is a variable defined in `C source code'.
Its value is
(".o" "~"
Hi,
AFAICT there is no support for completion-ignored-extensions in
Proof General. For coq, setting completion-ignored-extensions
would be nice, because the coq compiler clutters the directory
with .vo and .glob files.
My suggestion would be to extend proof-assistant-table with one
row for a list
Hi,
proof-done-advancing-require-function and
proof-shell-require-command-regexp seem to have only been used
for coq and they are no longer needed. IMHO it makes sense to
delete them. If this is general consensus I would develop a patch
and post it here for review.
Bye,
Hendrik
_
Hi,
because nobody answered to my poll on the coq mailing list
(https://sympa-roc.inria.fr/wws/arc/coq-club/2011-02/msg00059.html),
I suggest to not further support coq-auto-compile-vos.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-dev
Hi,
if nobody disagrees I am going to delete the old multiple file
handling code for coq. There was one worthwhile thing in it: the
coq-auto-compile-vos option. I'll check how I can keep its
functionality.
Bye,
Hendrik
___
ProofGeneral-devel mailing li
Hi,
is it really intended to add defpacustom variables to two
customization groups, to proof-assistant-internals-cusgrp and to
proof-assistant-setting?
Is there a reason why the group proof-assistant-setting is not
defined?
Bye,
Hendrik
___
ProofGene
Hi,
for coq there is currently a problem when you switch the active
scripting buffer: The first assert command in the new scripting
buffer does not assert anything.
This happens, because coq mode kills the proof assistant in the
deactivation hooks and proof-activate-scripting runs those hooks
_a
David Aspinall writes:
OK, I committed a patch now (not quite the one I sent you off list)
which ensures that the hook function is run.
Thanks, we can now close the killing-fully-asserted-active-buffer
issue.
And I don't get an error!
You don't see the error any more, because we have
Hi,
I looked around, but I could not find the inverse of
proof-register-possibly-new-processed-file. This inverse should
delete a file from proof-included-files-list and unlock its
buffer, if it exists.
There is proof-unregister-buffer-file-name, but
- it only works on buffers
- it does not unl
David Aspinall writes:
So I agree that your approach 1 is best.
Implemented and seems to work, but see my next post on "Reverse
of proof-register-possibly-new-processed-file".
> BTW, what is the relation of 'remove-action and
> 'span-delete-action? If there is a hook, the remove action
1 - 100 of 135 matches
Mail list logo
