diff options
Diffstat (limited to 'isar')
-rw-r--r-- | isar/isar-syntax.el | 9 | ||||
-rw-r--r-- | isar/isar.el | 14 |
2 files changed, 16 insertions, 7 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 74d5cb3e..22ab0a14 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -143,8 +143,15 @@ (concat "\\(" (proof-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":") "Regexp matching goal commands in Isabelle/Isar which name a theorem") +(defconst isar-verbatim-regexp "^\^VERBATIM: \\(.*\\)" + "Regexp matching internal marker for verbatim command output") -;; ----- Isabelle term / type hiliting +(defun isar-verbatim (str) + "Mark internal command for verbatim output" + (concat "\^VERBATIM: " str)) + + +;; ----- Isabelle inner syntax hilite (defface isabelle-class-name-face '((((type x) (class color) (background light)) diff --git a/isar/isar.el b/isar/isar.el index 059020f0..fc971fa2 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -71,6 +71,7 @@ ;;; ======== Configuration of generic modes ======== ;;; + ;; ===== outline mode (defcustom isar-outline-regexp @@ -188,7 +189,7 @@ proof-shell-prompt-pattern "^\\w*[>#] " ;; for issuing command, not used to track cwd in any way. - proof-shell-cd "cd \"%s\";" + proof-shell-cd (isar-verbatim "cd \"%s\";") proof-shell-proof-completed-regexp nil ; n.a. proof-shell-interrupt-regexp "\364\\*\\*\\* Interrupt\\|\360Interrupt" @@ -207,9 +208,9 @@ proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 ;; initial command configures Isabelle/Isar by modifying print functions etc. - proof-shell-init-cmd "ProofGeneral.init true;" + proof-shell-init-cmd (isar-verbatim "ProofGeneral.init true;") proof-shell-restart-cmd "init_toplevel; touch_all_thys; welcome;" - proof-shell-quit-cmd "quit();" + proof-shell-quit-cmd (isar-verbatim "quit();") proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-end "\361\\|\363" @@ -488,10 +489,11 @@ proof-shell-retract-files-regexp." ;; Configuring proof and pbp mode and setting up various utilities ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun isar-preprocessing () +(defun isar-preprocessing () ;dynamic scoping of `string' "insert sync markers - acts on variable string by dynamic scoping" - (if (not (string-match "^cd \\|^ProofGeneral\\.init " string)) ;; FIXME hack to detect initial ML stuff - (setq string (concat "\\<^sync>" (isar-shell-adjust-line-width) string "\\<^sync>;")))) + (if (string-match isar-verbatim-regexp string) + (setq string (match-string 1 string)) + (setq string (concat "\\<^sync>" (isar-shell-adjust-line-width) string "\\<^sync>;")))) (defun isar-mode-config () (isar-mode-config-set-variables) |