Add hooks for unicode tokens within proof shell

3 files changed, 75 insertions, 11 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 55594aa0..cf3b02ca 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -2015,8 +2015,9 @@ processing."
 		  (if proof-assistant-settings
 		      (proof-shell-invisible-command (proof-assistant-settings-cmd) t)))
 
-	      ;; Configure for x-symbol [even if the init cmd caused some error]
-	      (proof-x-symbol-shell-config)))))))
+	      ;; Configure for x-symbol or unicode input
+	      (proof-x-symbol-shell-config)
+	      (proof-unicode-tokens-shell-config)))))))
 
 
 (provide 'proof-shell)
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 95c4b691..2c5bf723 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -55,7 +55,8 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit."
       (remove-hook hook 'unicode-tokens-mode))
     (proof-map-buffers 
       (proof-buffers-in-mode proof-mode-for-script)
-      (unicode-tokens-mode (if flag 1 0)))))
+      (unicode-tokens-mode (if flag 1 0)))
+    (proof-unicode-tokens-shell-config)))
 
   
   
@@ -72,6 +73,49 @@ in future if we have just activated it for this buffer."
       (proof-unicode-tokens-init))
     (proof-unicode-tokens-set-global (not unicode-tokens-mode))))
 
+
+;;;
+;;; Interface to shell
+;;;
+
+(defun proof-unicode-tokens-activate-prover ()
+  (when (and proof-xsym-activate-command 
+	     (proof-shell-live-buffer)
+	     (proof-shell-available-p))
+    (proof-shell-invisible-command-invisible-result
+     proof-xsym-activate-command)))
+
+(defun proof-unicode-tokens-deactivate-prover ()
+  (when (and proof-xsym-deactivate-command 
+	     (proof-shell-live-buffer)
+	     (proof-shell-available-p))
+    (proof-shell-invisible-command-invisible-result
+     proof-xsym-deactivate-command)))
+
+(defun proof-unicode-tokens-shell-config ()
+  (when (proof-ass unicode-tokens-enable)
+    (add-hook 'proof-shell-insert-hook
+	      'proof-x-symbol-encode-shell-input)
+    (proof-unicode-tokens-activate-prover))
+  (unless (proof-ass unicode-tokens-enable)
+    (remove-hook 'proof-shell-insert-hook
+		 'proof-x-symbol-encode-shell-input)
+    (proof-unicode-tokens-deactivate-prover)))
+
+(defun proof-unicode-tokens-encode-shell-input ()
+  "Encode shell input in the variable STRING.
+A value for proof-shell-insert-hook."
+  (if (proof-ass unicode-tokens-enable)
+      (with-temp-buffer ;; TODO: better to do directly in *prover*
+	(insert string)
+	(unicode-tokens-unicode-to-tokens)
+	(setq string (buffer-substring-no-properties
+		      (point-min) (point-max))))))
+
+	
+	    
+
+
 ;;
 ;; On start up, adjust automode according to user setting
 ;;
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 414b926a..ada9f804 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -221,6 +221,7 @@
 ;;;    ("longleftrightarrow" . "←→")
 ;;;    ("Longleftrightarrow" . "⇐⇒")
 ;;;    ("longmapsto" . "❘→")
+    ("DodgyLongleftrightarrow" . "⇐woo⇒")
    ("hookrightarrow" . "↪")
    ("rightharpoonup" . "⇀")
    ("rightharpoondown" . "⇁")
@@ -305,6 +306,9 @@
    ("ffl" . "ffl")
    ))
 
+;; FIXME: not all of these shortcuts work, for some reason
+;; e.g. /0 although appears in input method prompts
+;; long arrows --> ==> don't appear in prompts
 (defvar isar-shortcut-alist
   '(; short cut, unicode string
     ("<>" . "⋄")
@@ -366,15 +370,30 @@
     ("''" . "″")
     ("'''" . "‴")
     ("''''" . "⁗")
-    ("nat" . "ℕ")
-    ("int" . "ℤ")
-    ("rat" . "ℚ")
-    ("real" . "ℝ")
-    ("complex" . "ℂ")
     (":=" . "≔")
-    ("euro" . "€")
-    ("yen" . "¥")
-    ("cent" . "¢")))
+    ;; some word shortcuts, started with backslash otherwise
+    ;; too annoying.
+    ("\nat" . "ℕ")
+    ("\int" . "ℤ")
+    ("\rat" . "ℚ")
+    ("\real" . "ℝ")
+    ("\complex" . "ℂ")
+    ("\euro" . "€")
+    ("\yen" . "¥")
+    ("\cent" . "¢")))
+
+
+;;
+;; prover symbol support 
+;;
+
+(eval-after-load "isar" 
+  '(setq 
+    proof-xsym-activate-command
+    (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
+    proof-xsym-deactivate-command
+    (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
+
 
 
 (provide 'isar-unicode-tokens)