diff options
author | 2000-06-16 11:50:12 +0000 | |
---|---|---|
committer | 2000-06-16 11:50:12 +0000 | |
commit | fefe0c59d3a3ca46f26d2c7bb52c20234e3dcd9b (patch) | |
tree | aec07ca83a7dd9d725be55e18af26fb56cdca095 | |
parent | 6470c02c16ad15cbab8f18b0fa09bfebe9b92743 (diff) |
Tuned x-symbol config, moved settings to isabelle-system.el
-rw-r--r-- | isa/isa.el | 16 | ||||
-rw-r--r-- | isa/isabelle-system.el | 25 | ||||
-rw-r--r-- | isar/isar.el | 24 |
3 files changed, 31 insertions, 34 deletions
@@ -612,9 +612,6 @@ you will be asked to retract the file or process the remainder of it." ;; (setq proof-xsym-extra-modes '(thy-mode) - proof-xsym-font-lock-keywords - ;; fontification for tokens themselves (FIXME: broken) - '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))) proof-xsym-activate-command "print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode);" proof-xsym-deactivate-command @@ -724,19 +721,6 @@ you will be asked to retract the file or process the remainder of it." ;; that's it for now! )) -(eval-after-load "x-symbol-isa" - ;; Add x-symbol tokens to isa-completion-table and rebuild - ;; internal completion table if completion is already active -'(progn -(defpgdefault completion-table - (append (proof-ass completion-table) - (mapcar (lambda (xsym) (nth 2 xsym)) - x-symbol-isa-table))) -(if (featurep 'completion) - (proof-add-completions)))) - - - diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el index 2e6aa775..ef2e4c79 100644 --- a/isa/isabelle-system.el +++ b/isa/isabelle-system.el @@ -288,5 +288,30 @@ until Proof General is restarted." (defpgdefault help-menu-entries isabelle-docs-menu) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; X-Symbol language configuration, and adding to completion table +;; + +(defpgdefault x-symbol-language 'isabelle) + +(setq proof-xsym-font-lock-keywords + ;; fontification for tokens themselves (FIXME: broken) + '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face)))) + +(eval-after-load "x-symbol-isabelle" + ;; Add x-symbol tokens to isa-completion-table and rebuild + ;; internal completion table if completion is already active +'(progn + (defpgdefault completion-table + (append (proof-ass completion-table) + (mapcar (lambda (xsym) (nth 2 xsym)) + x-symbol-isabelle-table))) + (if (featurep 'completion) + (proof-add-completions)))) + + + + (provide 'isabelle-system) ;; End of isabelle-system.el diff --git a/isar/isar.el b/isar/isar.el index a412e6d1..f69eaa53 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -567,15 +567,14 @@ proof-shell-retract-files-regexp." ;; x-symbol support for Isabelle PG, provided by David von Oheimb. ;; ;; The following settings configure the generic PG package. -;; The token language "Isabelle Symbols" is in file x-symbol-isar.el +;; The token language "Isabelle Symbols" is in file x-symbol-isabelle.el ;; -(setq proof-xsym-font-lock-keywords - '(("\\\\<[A-Za-z][A-Za-z0-9_']*>" (0 font-lock-type-face))) - proof-xsym-activate-command - "ML_command {* print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode) *};" - proof-xsym-deactivate-command - "ML_command {* print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]) *};") +(setq + proof-xsym-activate-command + "ML_command {* print_mode := ([\"xsymbols\",\"symbols\"] @ ! print_mode) *};" + proof-xsym-deactivate-command + "ML_command {* print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"]) *};") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -587,16 +586,5 @@ proof-shell-retract-files-regexp." (defpgdefault completion-table isar-keywords-major) -(eval-after-load "x-symbol-isar" - ;; Add x-symbol tokens to isar-completion-table and rebuild - ;; internal completion table if completion is already active -'(progn -(defpgdefault completion-table - (append (proof-ass completion-table) - (mapcar (lambda (xsym) (nth 2 xsym)) - x-symbol-isar-table))) -(if (featurep 'completion) - (proof-add-completions)))) - (provide 'isar) |