Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "Find Theorems" error

view this post on Zulip Email Gateway (Aug 18 2022 at 10:37):

From: John Matthews <matthews@galois.com>
I am trying to use the "Find Theorems" command with the latest
Isabelle snapshot (Isabelle_04-Jun-2007). However, all that happens
is that ProofGeneral brings up a new window called "Find Theorems",
and then the error message "No such face: :height" in the mini-buffer
at the bottom of the window.

I am using pre-release version ProofGeneral-3.7pre070511, on XEmacs
version 21.4.15. So far the rest of ProofGeneral has been working fine.

Thanks,
-john

view this post on Zulip Email Gateway (Aug 18 2022 at 10:37):

From: David Aspinall <da@inf.ed.ac.uk>
Quoting John Matthews <matthews@galois.com>:

I am trying to use the "Find Theorems" command with the latest
Isabelle snapshot (Isabelle_04-Jun-2007). However, all that happens
is that ProofGeneral brings up a new window called "Find Theorems",
and then the error message "No such face: :height" in the
mini-buffer at the bottom of the window.

This has been fixed in the Proof General CVS now. The window was
developed on GNU Emacs so an XEmacs incompatibility slipped through. I
will make a new pre-release soon.

I am using pre-release version ProofGeneral-3.7pre070511, on XEmacs
version 21.4.15. So far the rest of ProofGeneral has been working
fine.

Thanks for the report. If you find more problems which are definitely
Proof General problems, please use the trac system at
http://proofgeneral.inf.ed.ac.uk/trac

(Your problem was already there at
http://proofgeneral.inf.ed.ac.uk/trac/ticket/115)

Last updated: May 03 2024 at 08:18 UTC