Re: [isabelle] *** exception ValueMissing raised



On Thu, 17 Apr 2008, Jeremy Dawson wrote:

> I'm using a very recent version of Isabelle, and I get the message
> 
> *** exception ValueMissing raised
> 
> I can't find such an exception anywhere in the source code.
> 
> What does it mean, and where does it come from?

This exception appears in Poly/ML at least until 5.0 (I did not check 5.1; 
it is absent in recent development versions of Poly/ML 5.2).

To get an idea where the problem originates just do

  ML_command {* set Toplevel.debug *}

and look at the raw output (in the *isabelle* buffer of Proof General).

Sometimes you may have to wrap suspicious code into PolyML.exception_trace 
to get to the point.


	Makarius






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