Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 14 May 1993 23:26:14 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA22668; Fri, 14 May 93 15:08:05 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA22663; Fri, 14 May 93 15:08:01 -0700 Received: from localhost by panther.cs.uidaho.edu with SMTP id AA00702 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu); Fri, 14 May 1993 15:08:14 -0700 Message-Id: <199305142208.AA00702@panther.cs.uidaho.edu> To: info-hol@ted.cs.uidaho.edu Subject: Re: Emacs/HOL interface In-Reply-To: Your message of Fri, 14 May 93 15:31:20 -0400. <9305141931.AA07490@nestor.oracorp.com> Date: Fri, 14 May 93 15:08:14 -0700 From: Phil Windley X-Mts: smtp On Fri, 14 May 93 15:31:20 EDT, geoffrey@oracorp.com wrote: +------------ | I'm using the Emacs/HOL interface written by Phillip Windley. I | often want to send a region from my .ml file to the HOL interpreter, | using the command ESC C-z. When I send a large enough region (say 25 | lines/commands), it stops processing the commands after about 13, and | gives the cryptic message: | | writing to process: no more processes, hol | | Does anyone know what is going on, or better, how I can successfully | send arbitrarily large regions? This is a problem people have on occasion that I've never been able to duplicate. Try setting the variable *interpreter-max-string-length* to a smaller number. I'm not sure that this will help with your problem since I've never heard of the error message you got, but it has helped in similar situations in the past. --phil--