diff options
| author | Makarius Wenzel | 2005-09-01 14:18:10 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2005-09-01 14:18:10 +0000 |
| commit | 73375b71d50c9be41127d424b4868a5d0ccdba80 (patch) | |
| tree | 0f8904db9c051169d2ab4b250b6cc87ec2380d4e | |
| parent | 2b2dab487ffa46b7ddaf930071a0e6fa70b1bbc9 (diff) | |
tuned ML code for manipulating print_mode;
| -rw-r--r-- | isa/x-symbol-isa.el | 4 | ||||
| -rw-r--r-- | isar/x-symbol-isar.el | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el index d1ff4cb7..71dcb41e 100644 --- a/isa/x-symbol-isa.el +++ b/isa/x-symbol-isa.el @@ -12,9 +12,9 @@ (setq proof-xsym-extra-modes '(thy-mode) proof-xsym-activate-command - "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);" + "change print_mode (insert (op =) \"xsymbols\")" proof-xsym-deactivate-command - "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);") + "change print_mode (remove (op =) \"xsymbols\")") diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el index 42752ebe..684a2a21 100644 --- a/isar/x-symbol-isar.el +++ b/isar/x-symbol-isar.el @@ -13,10 +13,10 @@ (setq proof-xsym-activate-command (isar-markup-ml - "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode)") + "change print_mode (insert (op =) \"xsymbols\")") proof-xsym-deactivate-command (isar-markup-ml - "print_mode := (Library.gen_rems (op =) (! print_mode, [\"xsymbols\", \"symbols\"]))")) + "change print_mode (remove (op =) \"xsymbols\")")) (provide 'x-symbol-isar) |