25 Feb
2013
25 Feb
'13
7:25 a.m.
On 24/02/13 02:40, Lucas Dixon wrote:
How about:
val use_depth = ref 0; fun use s= (use_depth := (!use_depth) + 1; PolyML.use s; use_depth := (!use_depth) - 1);
Presumably you'd want to handle any exceptions raised by PolyML.use too (and reraise them after decrementing use_depth).
Phil