🚀 go-pugleaf

GNU Emacs 19.25.1 of Fri Aug 12 1994 on craro.dcs.ed.ac.uk (sparc-sun-solaris2.3)

I'm at my wits end with this one.

Somebody reported the following problem with my comint-derived package
for using a theorem prover: submitting the input shown below between
the two lines caused the process to die, as if EOF had been sent.  At
first I didn't believe it, but I found I could repeat it, and it
doesn't seem to have anything to do with my code.

In shell mode, if I type

$ cat >foo
<text>
$ bash: syntax error near unexpected token `1)])'

where <text> is the text below, I find that `foo' contains all but the
final line of text, and the bash error is consistent with typing in
just the last line.  This doesn't happen outside Emacs; things are
fine in an xterm (and in 19.22).

I don't *think* this is a comint problem, because the same thing
appears to happen when I call process-send-string with the string
below.

Of course, I have experimented to try and find a more concise example
that will cause the same failure, but it seems difficult: there are
several factors.  The size of the input (277 chars) *alone* is not at
fault, but deleting any of the lines removes the error.  I can delete
some of the characters; others seem important to the problem.  I have
spent much time trying various permutations but haven't found a string
which suggests more than the original does.

I hope that somebody will be able to spot the problem with this input,
or already has some clue as to what causes this problem - it seems
extremely obscure from this angle.

--------------------------------------------------
val consE' = prove_goal ZF.thy
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
 (fn major::prems =>
  [(rtac (major RS consE) 1),
   (eresolve_tac prems 1),
   (rtac classical 1),
   (eresolve_tac prems 1),
   (swap_res_tac prems 1),
   (etac notnotD 1)]);
--------------------------------------------------

Any help would be greatly appreciated.


------------
David Aspinall,                 email: David.Aspinall@dcs.ed.ac.uk
Department of Computer Science,   URL: http://www.dcs.ed.ac.uk/home/da
University of Edinburgh,          Tel: +44 31 650 5898
King's Buildings,                 Fax: +44 31 667 7209
Edinburgh.  EH9 3JZ