
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=koi8-r">

<style type="text/css" style="display:none"><!-- p { margin-top: 0px; margin-bottom: 0px; }--></style>

</head>

<body dir="ltr" style="font-size:12pt;color:#000000;background-color:#FFFFFF;font-family:Calibri,Arial,Helvetica,sans-serif;">

<p><span style="color: rgb(33, 33, 33); font-size: 12pt;">> I</span><span style="color: rgb(33, 33, 33); font-size: 12pt;">sn't there something like IO.defaultCase? I can't check right now but I'm pretty sure there is</span><br>

</p>

<p><br>

</p>

<p>Ah, there is IO.enumFallback(). It rarely used and was not obvious for me that</p>

<p>it do the same I tried to invent. Thanks for hint, <span style="font-size: 12pt;">with it patch will </span><span style="font-size: 12pt;">be</span><span style="font-size: 12pt;"> trivial..</span></p>

<p><br>

</p>

<p>George.<br>

</p>

</body>

</html>