| 1 | Debugger entered--Lisp error: (wrong-type-argument char-or-string-p nil) |
|---|
| 2 | insert(nil) |
|---|
| 3 | (save-excursion (set-buffer (get-buffer-create " x-symbol string conversion")) (erase-buffer) (insert string) (x-symbol-inherit-from-buffer buffer) (x-symbol-encode-all) (buffer-string)) |
|---|
| 4 | x-symbol-encode-string(nil #<buffer "*isabelle*">) |
|---|
| 5 | (setq string (x-symbol-encode-string string (current-buffer))) |
|---|
| 6 | (and x-symbol-language (setq string (x-symbol-encode-string string ...))) |
|---|
| 7 | proof-x-symbol-encode-shell-input() |
|---|
| 8 | run-hooks(proof-x-symbol-encode-shell-input) |
|---|
| 9 | (save-current-buffer (set-buffer proof-shell-buffer) (goto-char (point-max)) (run-hooks (quote proof-shell-insert-hook)) (if proof-shell-strip-crs-from-input (setq string ...)) (insert string) (unless (null ...) (set-marker proof-marker ...)) (insert proof-shell-insert-space-fudge) (let (...) (comint-send-input))) |
|---|
| 10 | (with-current-buffer proof-shell-buffer (goto-char (point-max)) (run-hooks (quote proof-shell-insert-hook)) (if proof-shell-strip-crs-from-input (setq string ...)) (insert string) (unless (null ...) (set-marker proof-marker ...)) (insert proof-shell-insert-space-fudge) (let (...) (comint-send-input))) |
|---|
| 11 | proof-shell-insert(nil proof-done-retracting) |
|---|
| 12 | (progn (proof-grab-lock queuemode) (setq proof-shell-last-output-kind nil) (if (proof-shell-should-be-silent ...) (progn ... ...)) (setq proof-action-list (nconc proof-action-list alist)) (proof-shell-insert (nth 1 item) (nth 2 item))) |
|---|
| 13 | (if proof-action-list (progn (and proof-shell-busy queuemode ...) (if ... ...) (setq proof-action-list ...)) (progn (proof-grab-lock queuemode) (setq proof-shell-last-output-kind nil) (if ... ...) (setq proof-action-list ...) (proof-shell-insert ... ...))) |
|---|
| 14 | (if alist (if proof-action-list (progn ... ... ...) (progn ... ... ... ... ...))) |
|---|
| 15 | (let (item) (while (and alist ...) (funcall ... ...) (setq alist ...)) (if (and ... ...) (proof-detach-queue)) (if alist (if proof-action-list ... ...))) |
|---|
| 16 | proof-append-alist(((#<extent [69, 81) 0x38a1738 in buffer Scratch.thy> nil proof-done-retracting))) |
|---|
| 17 | proof-start-queue(69 81 ((#<extent [69, 81) 0x38a1738 in buffer Scratch.thy> nil proof-done-retracting))) |
|---|
| 18 | (let ((end ...) (start ...) (span ...) actions) (if (and span proof-kill-goal-command ...) (if ... ... ... ...)) (if (> end start) (setq actions ...)) (proof-start-queue (min start end) (proof-locked-end) actions)) |
|---|
| 19 | proof-retract-target(#<extent [69, 81) H keymap help-echo balloon-help cmd type 0x37321f8 in buffer Scratch.thy> nil) |
|---|
| 20 | (let ((span ...)) (unless span (proof-goto-end-of-locked) (backward-char) (setq span ...)) (proof-retract-target span delete-region)) |
|---|
| 21 | (if (proof-locked-region-empty-p) nil (let (...) (unless span ... ... ...) (proof-retract-target span delete-region))) |
|---|
| 22 | (unless (proof-locked-region-empty-p) (let (...) (unless span ... ... ...) (proof-retract-target span delete-region))) |
|---|
| 23 | (if (proof-locked-region-empty-p) (error "No locked region") (proof-activate-scripting) (unless (proof-locked-region-empty-p) (let ... ... ...))) |
|---|
| 24 | proof-retract-until-point(nil) |
|---|
| 25 | (progn (goto-char (span-start lastspan)) (proof-retract-until-point delete)) |
|---|
| 26 | (if lastspan (progn (goto-char ...) (proof-retract-until-point delete)) (error "Nothing to undo!")) |
|---|
| 27 | (let ((lastspan ...)) (if lastspan (progn ... ...) (error "Nothing to undo!"))) |
|---|
| 28 | (if (proof-locked-region-empty-p) nil (let (...) (if lastspan ... ...))) |
|---|
| 29 | (unless (proof-locked-region-empty-p) (let (...) (if lastspan ... ...))) |
|---|
| 30 | (progn (unless (proof-locked-region-empty-p) (let ... ...))) |
|---|
| 31 | (if (eq proof-follow-mode (quote locked)) (progn (unless ... ...)) (save-excursion (unless ... ...))) |
|---|
| 32 | (proof-maybe-save-point (unless (proof-locked-region-empty-p) (let ... ...))) |
|---|
| 33 | (progn (proof-maybe-save-point (unless ... ...)) (proof-maybe-follow-locked-end)) |
|---|
| 34 | (cond ((eq proof-buffer-type ...) (progn ... ...)) ((buffer-live-p proof-script-buffer) (with-current-buffer proof-script-buffer ... ...))) |
|---|
| 35 | (proof-with-script-buffer (proof-maybe-save-point (unless ... ...)) (proof-maybe-follow-locked-end)) |
|---|
| 36 | proof-undo-last-successful-command-1() |
|---|
| 37 | (lambda nil "Undo last successful command at end of locked region." (interactive) (proof-undo-last-successful-command-1))() |
|---|
| 38 | call-interactively(proof-toolbar-undo) |
|---|
| 39 | release-and-activate-toolbar-button(#<buttonup-event button1up>) |
|---|
| 40 | call-interactively(release-and-activate-toolbar-button) |
|---|
