[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2

[Makarius]

On Mon, 6 Dec 2010, Lucas Dixon wrote:

> ... at the moment I need Isabelle2009-2, too many dependencies to 
> quickly unravel... is there an easy way to disable 
> multi-threading/futures so that I can see what the real ML error is? a 
> quick pointer to what to hack in the ML-Systems dir? :)
>
> At the moment I need reliability/simplicity over speed; so will probably 
> need to do this anyway...

You merely need to get the effect of "usedir -M 1 -q 0" in interactive 
mode, which works via some Proof General menu items.  In ML the 
corresponding references can ge set as follows:

   Multithreading.max_threads := 1;
   Goal.parallel_proofs := 0;


 	Makarius