diff options
| -rw-r--r-- | isa/x-symbol-isa.el | 21 | ||||
| -rw-r--r-- | isar/x-symbol-isar.el | 22 |
2 files changed, 43 insertions, 0 deletions
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el new file mode 100644 index 00000000..d1ff4cb7 --- /dev/null +++ b/isa/x-symbol-isa.el @@ -0,0 +1,21 @@ +;; Canonical file for token language file for PG/isar. + +(require 'x-symbol-isabelle) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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-isabelle.el +;; + +(setq proof-xsym-extra-modes '(thy-mode) + proof-xsym-activate-command + "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);" + proof-xsym-deactivate-command + "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);") + + + +(provide 'x-symbol-isa) diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el new file mode 100644 index 00000000..42752ebe --- /dev/null +++ b/isar/x-symbol-isar.el @@ -0,0 +1,22 @@ +;; Canonical file for token language file for PG/isar. + +(require 'x-symbol-isabelle) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; x-symbol support +;; +;; The following settings configure the generic PG package. +;; The token language "Isabelle Symbols" is in file isa/x-symbol-isabelle.el +;; + +(setq + proof-xsym-activate-command + (isar-markup-ml + "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode)") + proof-xsym-deactivate-command + (isar-markup-ml + "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))")) + + +(provide 'x-symbol-isar) |