[isabelle] PG CVS: "error in process filter: Wrong number of arguments"



Dear Isabelle Users,

I'd like to ask you about an issue I have with Proof General (CVS version) and see if someone has a quick work-around of any kind.

I've already filed a bug report, but as it's the only PG activity in the last 90+ days, I don't know if anyone will get around to looking at it:
	http://proofgeneral.inf.ed.ac.uk/trac/ticket/322

Basically, attempting to use the "tracing" function inside ML makes PG choke, at least when it is done inside a proof method (which I use for debugging when writing a new proof method). Here is an example:

theory SC imports Main
begin

ML {*
  fun moo_tac ctxt (ct,i) = (
      tracing ("Target: MOO!");
      no_tac);
*}

method_setup moo = {*
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (CSUBGOAL (moo_tac ctxt)))
*} "Some proof method reduced to a simple thing which fails."

(* don't match on different state vars *)
lemma "X ==> Y"
  apply (moo)

At this point, PG stops with:

error in process filter: proof-shell-process-urgent-message: Wrong number of arguments: #[(str) [...] [proof-trace-buffer str newline] 1 ("/home/rafalk/repos/l4.verified/isabelle/contrib/ProofGeneral/generic/pg-response.elc" . 12897)], 3

The [...] includes non-printable characters, hence omitted.

Has anyone seen anything similar?

Sincerely,

Rafal Kolanski.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.