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.

The above version of XEmacs (standard XEmacs on Fedora 7) has problems with matching ends of commands properly. It trips up on the standard test example.v file, as well as, e.g., examples given in #141.