172 |
<script type="text/javascript" src="$js_url"></script> |
<script type="text/javascript" src="$js_url"></script> |
173 |
</head> |
</head> |
174 |
|
|
175 |
|
<!-- |
176 |
<body onLoad="show_hide_display(show,hide);"> |
<body onLoad="show_hide_display(show,hide);"> |
177 |
|
--> |
178 |
|
<body> |
179 |
|
|
180 |
<div style="float: right; width: 10em;"> |
<div style="float: right; width: 10em;"> |
181 |
Folding: |
Folding: |
365 |
|
|
366 |
print HTML " " x $level . |
print HTML " " x $level . |
367 |
qq{<a name="mfn$mfn"></a>\n <ul id="mfn$mfn"}. |
qq{<a name="mfn$mfn"></a>\n <ul id="mfn$mfn"}. |
368 |
($style ? ' style="$style"' : ""). |
($style ? ' style="'.$style.'"' : ''). |
369 |
qq{>\n}; |
qq{>\n}; |
370 |
|
|
371 |
if ($style) { |
if ($style) { |