365 { |
365 { |
366 if (!(browser_info + Path.explode("index.html")).is_file) { |
366 if (!(browser_info + Path.explode("index.html")).is_file) { |
367 Isabelle_System.make_directory(browser_info) |
367 Isabelle_System.make_directory(browser_info) |
368 Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), |
368 Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), |
369 browser_info + Path.explode("isabelle.gif")) |
369 browser_info + Path.explode("isabelle.gif")) |
|
370 val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" |
370 File.write(browser_info + Path.explode("index.html"), |
371 File.write(browser_info + Path.explode("index.html"), |
371 File.read(Path.explode("~~/lib/html/library_index_header.template")) + |
372 """<?xml version="1.0" encoding="iso-8859-1"?> |
372 File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
373 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
373 File.read(Path.explode("~~/lib/html/library_index_footer.template"))) |
374 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
375 |
|
376 <html xmlns="http://www.w3.org/1999/xhtml"> |
|
377 <head> |
|
378 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" /> |
|
379 <title>""" + title + """</title> |
|
380 </head> |
|
381 |
|
382 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040"> |
|
383 <center> |
|
384 <table width="100%" border="0" cellspacing="10" cellpadding="0"> |
|
385 <tr> |
|
386 <td width="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td> |
|
387 |
|
388 <td width="80%" valign="middle" align="center"> |
|
389 <table width="90%" border="0" cellspacing="0" cellpadding="20"> |
|
390 <tr> |
|
391 <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td> |
|
392 </tr> |
|
393 </table> |
|
394 </td> |
|
395 </tr> |
|
396 </table> |
|
397 </center> |
|
398 <hr /> |
|
399 <ul> |
|
400 <li>Higher-Order Logic</li> |
|
401 |
|
402 <li style="list-style: none"> |
|
403 <ul> |
|
404 <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a> |
|
405 is a version of classical higher-order logic resembling |
|
406 that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>. |
|
407 </li> |
|
408 </ul> |
|
409 </li> |
|
410 </ul> |
|
411 |
|
412 <ul> |
|
413 <li>First-Order Logic</li> |
|
414 |
|
415 <li style="list-style: none"> |
|
416 <ul> |
|
417 <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a> |
|
418 provides basic classical and intuitionistic first-order logic. It is |
|
419 polymorphic. |
|
420 </li> |
|
421 |
|
422 <li><a href="ZF/index.html">ZF (Set Theory)</a> |
|
423 offers a formulation of Zermelo-Fraenkel set theory on top of FOL. |
|
424 </li> |
|
425 |
|
426 <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li> |
|
427 |
|
428 <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li> |
|
429 |
|
430 <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li> |
|
431 </ul> |
|
432 </li> |
|
433 </ul> |
|
434 |
|
435 <ul> |
|
436 <li>Miscellaneous</li> |
|
437 |
|
438 <li style="list-style: none"> |
|
439 <ul> |
|
440 <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li> |
|
441 |
|
442 <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a> |
|
443 is an extensional version of Martin-Löf's Type Theory.</li> |
|
444 |
|
445 <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li> |
|
446 |
|
447 <li><a href="Pure/index.html">The Pure logical framework</a></li> |
|
448 |
|
449 <li><a href="Doc/index.html">Sources of Documentation</a></li> |
|
450 </ul> |
|
451 </li> |
|
452 </ul> |
|
453 </body> |
|
454 </html> |
|
455 """) |
374 } |
456 } |
375 } |
457 } |
376 |
458 |
377 |
459 |
378 /* present session */ |
460 /* present session */ |