<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You could also do something like in<br>
<a href="http://www.ccs.neu.edu/racket/pubs/stop09-ft.pdf" target="_blank">http://www.ccs.neu.edu/racket/pubs/stop09-ft.pdf</a>, to ensure that the<br>
only part of the code knows about the option value, and everyone else<br>
does not.</blockquote><div><br></div><div>Apropos to the need at hand.  Thanks. </div></div>