| 1 | Debugger entered--Lisp error: (wrong-type-argument stringp nil) |
|---|
| 2 | set-buffer(nil) |
|---|
| 3 | (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 ... ... ...))) |
|---|
| 4 | (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 ... ... ...))) |
|---|
| 5 | proof-trace-buffer-display("IVtestJ") |
|---|
| 6 | (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 ... ... ...))) |
|---|
| 7 | proof-shell-process-urgent-message("IVtestJ") |
|---|
| 8 | (save-excursion (setq lastend end) (proof-shell-process-urgent-message (buffer-substring start end))) |
|---|
| 9 | (if (setq end (re-search-forward proof-shell-eager-annotation-end nil t)) (save-excursion (setq lastend end) (proof-shell-process-urgent-message ...))) |
|---|
| 10 | (while (and end (re-search-forward proof-shell-eager-annotation-start nil ...)) (setq start (match-beginning 0)) (if (setq end ...) (save-excursion ... ...))) |
|---|
| 11 | (let ((pt ...) (end t) lastend (start ...)) (goto-char start) (while (and end ...) (setq start ...) (if ... ...)) (if lastend (set-marker proof-shell-urgent-message-marker ...)) (if end (set-marker proof-shell-urgent-message-scanner ...) (set-marker proof-shell-urgent-message-scanner ...)) (goto-char pt)) |
|---|
| 12 | proof-shell-process-urgent-messages() |
|---|
| 13 | (and proof-shell-eager-annotation-start (proof-shell-process-urgent-messages)) |
|---|
| 14 | (save-excursion (if proof-shell-strip-crs-from-output (progn ... ...)) (and proof-shell-eager-annotation-start (proof-shell-process-urgent-messages)) (if (if proof-shell-wakeup-char ... t) (if ... ... ...))) |
|---|
| 15 | proof-shell-filter("IVtestJ\nIVTrue\n 1. TrueJ\nO\nproof (prove): step 1\n\ngoal (1 subgoal):\n 1. True\nP\n> S") |
|---|
| 16 | run-hook-with-args(proof-shell-filter "IVtestJ\nIVTrue\n 1. TrueJ\nO\nproof (prove): step 1\n\ngoal (1 subgoal):\n 1. True\nP\n> S") |
|---|
| 17 | comint-output-filter(#<process "isabelle" pid 11285 state:run> "IVtestJ\nIVTrue\n 1. TrueJ\nO\nproof (prove): step 1\n\ngoal (1 subgoal):\n 1. True\nP\n> S") |
|---|
