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.

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.