diff options
| author | David Aspinall | 2000-05-29 18:33:15 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-05-29 18:33:15 +0000 |
| commit | fb474f38984c9752e0ca06dbf70a176af93bedc3 (patch) | |
| tree | 25a85a17f3376dbf455b5978ec2a3bd50e093bb1 /isar | |
| parent | 90659a5779c1ddb472a19af0a8f1c9776e695d37 (diff) | |
Use generic default setting mechanism now. Add isar-markup-ml here.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/isar/isar.el b/isar/isar.el index 24d54fc2..5775f24d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -184,10 +184,6 @@ found-header))) -;;; NB! Disadvantage of *not* shadowing variables is that user -;;; cannot override them. It might be nice to override some -;;; variables, which ones? - (defun isar-mode-config-set-variables () "Configure generic proof scripting mode variables for Isabelle/Isar." (setq @@ -275,11 +271,13 @@ ;; initial command configures Isabelle/Isar by modifying print ;; functions, restoring settings saved by Proof General, etc. - proof-shell-pre-sync-init-cmd (isar-verbatim "ProofGeneral.init true;") - proof-shell-init-cmd (isabelle-set-default-cmd) + proof-shell-pre-sync-init-cmd (isar-verbatim + "ProofGeneral.init true;") + proof-shell-init-cmd (proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.restart;" proof-shell-quit-cmd (isar-verbatim "quit();") - + proof-assistant-setting-format 'isar-markup-ml + proof-shell-eager-annotation-start-length 1 proof-shell-eager-annotation-start "\360\\|\362" proof-shell-eager-annotation-end "\361\\|\363" @@ -525,6 +523,10 @@ proof-shell-retract-files-regexp." (setq string (match-string 1 string)) (setq string (concat "\\<^sync>" (isar-shell-adjust-line-width) string "\\<^sync>;")))) +(defun isar-markup-ml (string) + "Return marked up version of ML command STRING for Isar." + (format "ML_command {* %s *};" string)) + (defun isar-mode-config () (isar-mode-config-set-variables) (isar-init-syntax-table) |