New files.

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)