Opened 14 years ago
Closed 14 years ago
#322 closed defect (invalid)
Isabelle: "error in process filter: Wrong number of arguments" when using tracing() in ML
| Reported by: | RafalKolanski | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | ML, tracing, isabelle |
| Cc: |
Description
When using the tracing function in an ML block, Proof General generates the error attached in SC.txt
To reproduce this error, use the attached SC.thy. It occurs at
apply (moo)
Isabelle version: 2009-1
PG version: latest CVS as of right now.
Attachments (2)
Change History (5)
Changed 14 years ago by
comment:1 Changed 14 years ago by
Oh, also, emacs version:
GNU Emacs 23.1.50.1 (x86_64-pc-linux-gnu, GTK+ Version 2.18.0)
of 2009-09-27 on crested, modified by Debian
running on Ubuntu 9.10.
comment:2 Changed 14 years ago by
And finally, when I open the *isabelle* buffer and press enter, Proof General becomes responsive again and resumes sync after the command is executed, so the command is executed properly, state is maintained properly, just something to do with the feedback to the user goes wrong.
Changed 14 years ago by
comment:4 Changed 14 years ago by
| Resolution: | → invalid |
|---|---|
| Status: | new → closed |
Not a PG bug. This turned out to be a problem with CVS somehow creating a mangled version over time when using "cvs up -d", consistently on two different machines. Using "cvs up -A" and "make clean" solved it. Thanks David!
Error generated by PG when trying to execute apply (moo)