Custom Query (361 matches)

if you're undoing a command, "undo" will undo the largest container which ends with the command; this is not always correct behaviour, for example if our document ends halfway through a proof, or if we've made an edit which has reset the parsed container regions, then undo will try to undo the lemma, which is incorrect (and can cause prover state to become inconsistent).

one option is to look at the proof state and only undo the largest container which has been closed (processed to the point where it is discharged, e.g. lemma .... sorry).

alternatively when we do a parse we could record whether the container is closed. if we have to change the length of that container (e.g. because of an edit) then we reset the container to be open, and we don't undo it until a parse tells us its correct end location.

it is possible that i broke this (if this used to work, then it is very likely!), by adjusting the end location of containers when edits are done. however i think the changes i made were necessary. but i think what i did to break it was approximately correct.

(were we using empty children or whitespace to indicate that a container is parsed to closure? that would explain how i broke it. if so, i suggest we refactor to use a boolean "containerParsedToClosure" on a container to indicate that it is parsed to closure, rather than sticking empty containers or whitespace into the tree.)

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.