diff options
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-user.el | 38 |
1 files changed, 37 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 8f930382..4b748b81 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -647,12 +647,15 @@ last use time, to discourage saving these into the users database." ;; ;; Tags table building ;; -;; New in 3.3... or perhaps later. +;; New in 3.3... or perhaps later! ;; ;; FIXME: incomplete. Add function to build tags table from ;; + + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -911,6 +914,39 @@ If NUM is negative, move upwards. Return new span." + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Generic adjustmenth of prover's pretty-printing width +;; (adapted from Lego's mode, was also used in Isar and Plastic) +;; +;; FIXME: complete this. + +;(defvar pg-prover-current-line-width nil +; "Cache value for pg-adjust-line-width to avoid repeatedly changing width.") + +;(defun pg-adjust-line-width (buffer) +; "Adjust the prover's line width to match that of BUFFER." +; (proof-if-setting-configured proof-shell-adjust-line-width-cmd) +; proof-shell-(let* ((win (get-buffer-window buffer)) +; (curwid (if win (window-width win)))) +; (if (and curwid +; (not (equal curwid pg-prover-current-line-width))) +; (progn +; ;; Update the prover's output width +; (proof-shell-invisible-command + + +;with-current-buffer buffer +; (let ((current-width +; (window-width (get-buffer-window proof-goals-buffer))) +; (if (equal current-width lego-shell-current-line-width) () +; ; else +; (setq lego-shell-current-line-width current-width) +; (set-buffer proof-shell-buffer) +; (insert (format lego-pretty-set-width (- current-width 1))) +; ))))) + |