Custom Query (361 matches)

displaying this customization group gives an error and a lot of options are invisible

Hello,

I have just noticed the ProofGeneral function proof-undo-and-delete-last-successful-command does not really meet the specification that is described in its documentation, namely:

... the deleted command is put into the Emacs kill ring, so
you can use the usual `yank' and similar commands to retrieve the
deleted text.

I have performed a few tests and it seems sufficient to replace

(proof-undo-last-successful-command-1 'delete-region)

with

(proof-undo-last-successful-command-1 'kill-region)

in generic/pg-user.el to provide the missing feature.

Kind regards,

Erik Martin-Dorel

proof-shell-trace-output-regexp appears visually in the *trace* buffer.

For example (in Isabelle):

ML_command {* tracing "foo" *}

Results in

\^AVfoo

Another example with extra term markup, which is displayed properly after the initial garbage:

ML_command {* tracing (Syntax.string_of_term_global @{theory} @{term "x == y"}) *}