Add hooks for unicode tokens within proof shell

2 files changed, 48 insertions, 3 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
 ;;