Custom Query (361 matches)

Using xemacs-21.4.x (on Mac OS or Linux), the initial *trace* buffer setup breaks down with the following backtrace.

Reproduce this by starting a fresh PG session and issue the following command: ML {* tracing "foo" *}

(1) (error/warning) Error in process filter: (wrong-type-argument stringp nil)

The emacs debugger produces a backtrace like this:

Debugger entered--Lisp error: (wrong-type-argument stringp nil)
  set-buffer(nil)
  (save-current-buffer (set-buffer proof-trace-buffer) (goto-char (point-max)) (newline) (or proof-trace-last-fontify-pos (setq proof-trace-last-fontify-pos ...)) (insert str) (unless (bolp) (newline)) (unless pg-tracing-slow-mode (let ... ... ...)))
  (with-current-buffer proof-trace-buffer (goto-char (point-max)) (newline) (or proof-trace-last-fontify-pos (setq proof-trace-last-fontify-pos ...)) (insert str) (unless (bolp) (newline)) (unless pg-tracing-slow-mode (let ... ... ...)))
  proof-trace-buffer-display("IVfooJ")
  (cond ((and proof-shell-trace-output-regexp ...) (proof-trace-buffer-display ...) (unless ... ... ...) (if ... ...)) ((and proof-shell-process-file ...) (let ... ...)) ((and proof-shell-retract-files-regexp ...) (let ... ... ...)) ((and proof-shell-clear-response-regexp ...) (pg-response-maybe-erase nil t t)) ((and proof-shell-clear-goals-regexp ...) (proof-clean-buffer proof-goals-buffer)) ((and proof-shell-set-elisp-variable-regexp ...) (let ... ...)) ((and proof-shell-match-pgip-cmd ...) (require ...) (require ...) (unless ... ...) (let ... ...)) ((and proof-shell-theorem-dependency-list-regexp ...) (let ... ...)) (t (pg-response-maybe-erase nil nil) (let ... ... ...)))

After stopping/starting Isabelle, it somehow works, i.e. *trace* is available then.

Typical work flow is: change something, send using c-c c-return. If the command fails, it's probably due to the something I just changed, where I had the cursor in the first place. Unfortunately, proof general moves it to the end of the current command, making me have to go back manually, change things again, etc.

Being able to keep the cursor where it is if the command fails would be really nice.

The commands of type (* comment *) and -- "comment" are absorbed as part of the previous command. They hardly ever describe the previous command, instead describing the *following* one.

I would much prefer if when I pressed "previous" or performed an undo using c-c c-return, I could go up to before the comment without undoing the previous command.

This is one of the reasons I've taken to working with strict read-only turned off, but for beginners this is not such a good idea.