diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-06-04 12:38:33 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-06-04 12:38:33 +0000 |
| commit | d7c3a28384d55f4daf7bb207bc5914225d4917a0 (patch) | |
| tree | 18d60989e05645fbce427b88aa84bcf7944132cb /isar/isar.el | |
| parent | 682a9b0aa3373a4ab65011c1547529404b264827 (diff) | |
replaced isar-verbatim by isabelle-verbatim;
added isar-strip-terminators;
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/isar/isar.el b/isar/isar.el index 0f23aad1..83c601a3 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -186,6 +186,17 @@ (and cont (forward-char forward-amount))) found-header))) + +(defun isar-strip-terminators () + "Remove explicit Isabelle/Isar command terminators `;' from buffer" + (interactive) + (save-excursion + (goto-char (point-min)) + (while (search-forward ";" (point-max) t) + (if (not (buffer-syntactic-context)) + (delete-backward-char 1))))) + + (defun isar-mode-config-set-variables () "Configure generic proof scripting mode variables for Isabelle/Isar." (setq @@ -272,12 +283,12 @@ ;; initial command configures Isabelle/Isar by modifying print ;; functions, restoring settings saved by Proof General, etc. - proof-shell-pre-sync-init-cmd (isar-verbatim + proof-shell-pre-sync-init-cmd (isabelle-verbatim "ProofGeneral.init true;") proof-assistant-setting-format 'isar-markup-ml proof-shell-init-cmd (proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.restart;" - proof-shell-quit-cmd (isar-verbatim "quit();") + proof-shell-quit-cmd (isabelle-verbatim "quit();") proof-shell-eager-annotation-start-length 1 proof-shell-eager-annotation-start "\360\\|\362" @@ -520,7 +531,7 @@ proof-shell-retract-files-regexp." (defun isar-preprocessing () ;dynamic scoping of `string' "Insert sync markers - acts on variable STRING by dynamic scoping" - (if (string-match isar-verbatim-regexp string) + (if (string-match isabelle-verbatim-regexp string) (setq string (match-string 1 string)) (unless (string-match ";[ \t]$" string) ; da: added this (setq string (concat string ";"))) ; da: added this |