diff options
| -rw-r--r-- | isar/isar-syntax.el | 9 | ||||
| -rw-r--r-- | isar/isar.el | 42 |
2 files changed, 40 insertions, 11 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 0bc279f3..487a1bdc 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -13,7 +13,6 @@ (require 'proof-syntax) (require 'isar-keywords) - ;; ----- character syntax (defconst isar-script-syntax-table-entries @@ -467,6 +466,14 @@ matches contents of quotes for quoted identifiers.") (defun isar-cannot-undo (cmd) (concat "cannot_undo \"" cmd "\";")) +(defconst isar-undo-commands + (list + isar-linear-undo + isar-undo + "init_toplevel" "kill_thy" + "undos_proof" + "cannot_undo")) + (defconst isar-theory-start-regexp (proof-anchor-regexp (isar-ids-to-regexp diff --git a/isar/isar.el b/isar/isar.el index 9b40ad5b..b9381e2c 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -533,20 +533,42 @@ Checks the width in the `proof-goals-buffer'" ans)) ;; -;; Configuring proof output buffer +;; Shell mode command adjusting ;; +(defconst isar-nonwrap-regexp + ;; FIXME: approx: should only match at start or after terminator + (regexp-opt (cons "ProofGeneral.process_pgip" + isar-undo-commands))) + +(defun isar-command-wrapping (string) + (if (not (proof-string-match isar-nonwrap-regexp string)) + (concat + "Isabelle.command \"" + (proof-replace-regexp-in-string + "[\000-\037\"\\\\]" + (lambda (str) (format "\\\\%03d" (string-to-char str))) + string) + "\"") + (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string))) + + (defun isar-preprocessing () ;dynamic scoping of `string' "Insert sync markers - acts on variable STRING by dynamic scoping." - (if (proof-string-match isabelle-verbatim-regexp string) - (setq string (match-string 1 string)) - (unless (proof-string-match ";[ \t]*\\'" string) - (setq string (concat string ";"))) - (setq string (concat - "\\<^sync>" - (isar-shell-adjust-line-width) - (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string) - " \\<^sync>;")))) + (save-match-data + (if (proof-string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)) + (unless (proof-string-match ";[ \t]*\\'" string) + (setq string (concat string ";"))) + (setq string (concat + "\\<^sync>; " + (isar-shell-adjust-line-width) + (isar-command-wrapping string) + " \\<^sync>;"))))) + +;; +;; Configuring proof output buffer +;; (defun isar-mode-config () (isar-mode-config-set-variables) |