diff options
| -rw-r--r-- | CHANGES | 26 | ||||
| -rw-r--r-- | generic/proof-config.el | 15 | ||||
| -rw-r--r-- | generic/proof-shell.el | 11 |
3 files changed, 36 insertions, 16 deletions
@@ -42,13 +42,25 @@ Emacs would freeze when starting proof assistant due to character matching problem. -*** Fix for infamous Solaris ^G problem, now PG uses pipes +*** Fix for infamous Solaris ^G problem: proof-shell-process-connection-type - We now set process-connection-type=nil to force piped communication - instead of ptys. However, ptys are to be prefered over pipes - because pipes can become full or lose data. Please report any - problems of this nature you may suspect; if any are found we - will only use pipes for Solaris. + A user (or proof assistant configuration) can now specify whether + to use pty or piped communication. This is to fix the problem that + Solaris users have (because of a Solaris bug), when lots of ^G's + appear. + + The default setting for proof-shell-process-connection-type is made + by examining the ARCH environment variable. If this contains "sun" + then proof-shell-process-connection-type is set to nil for using + pipes. Otherwise we use ptys which are to be prefered over pipes + because pipes can become full or lose data, and pipes don't work + which some proof assistants. + + If necessary, you can override this by customization, as usual. + +*** Added new configuration hook: proof-shell-pre-interrupt-hook + + This is ** Coq Changes @@ -60,6 +72,8 @@ ** Isabelle Changes +*** + ** Isar Changes 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 |