Opened 12 years ago

Closed 12 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)

SC.txt (495 bytes) - added by RafalKolanski 12 years ago.
Error generated by PG when trying to execute apply (moo)
SC.thy (407 bytes) - added by RafalKolanski 12 years ago.

Download all attachments as: .zip

Change History (5)

Changed 12 years ago by RafalKolanski

Attachment: SC.txt added

Error generated by PG when trying to execute apply (moo)

comment:1 Changed 12 years ago by RafalKolanski

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 12 years ago by RafalKolanski

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 12 years ago by RafalKolanski

Attachment: SC.thy added

comment:4 Changed 12 years ago by RafalKolanski

Resolution: invalid
Status: newclosed

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!

Note: See TracTickets for help on using tickets.