Added proof-shell-process-connection-type.

2 files changed, 16 insertions, 10 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 37e5ad27..9860434e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1410,6 +1410,21 @@ to do syntax highlighting with font-lock."
 ;; 5c. hooks and hook-related variables
 ;;
 
+(defcustom proof-shell-process-connection-type 
+  ;; Use ptys unless it seems like we're on Solaris.
+  (not (string-match "[sS]un" (or (getenv "ARCH") "")))
+  "The value of process-connection-type for the proof shell.
+Set non-nil for ptys, nil for pipes.
+The default (and preferred) option is to use pty communication.
+However there is a long-standing backslash/long line problem with
+Solaris which gives a mess of ^G characters when some input is sent
+which has a \ in the 256th position.   We do not force pipes everywhere
+because this risks loss of data and some proof assistants do not 
+flush their output by default after each interaction, which breaks 
+pipe communication."
+  :type 'boolean
+  :group 'proof-shell)
+  
 (defcustom proof-shell-insert-hook nil 
   "Hooks run by proof-shell-insert before inserting a command.
 Can be used to configure the proof assistant to the interface in
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 91fa4398..cf116a4a 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -222,16 +222,7 @@ Does nothing if proof assistant is already running."
 	      ;; Split on spaces: FIXME: maybe should be whitespace.
 	      " "))
 
-	    ;; Experimental fix for backslash/long line problem with
-	    ;; Solaris.  Make start-process (called by make-comint)
-	    ;; use a pipe, not a pty, by setting process-connection-type=nil.
-	    ;; It seems to work, but has known disadvantages.  
-	    ;; (I've forgotten what they are, size problems?).
-	    (process-connection-type 
-	     ;; FIXME: might be good to test for Solaris here to use
-	     ;; pty's on Linux as not problematic.
-	     nil))
-
+	    (process-connection-type proof-shell-process-connection-type))
 
 	;; An improvement here might be to catch failure of
 	;; make-comint and then kill off the buffer.  Then we