484 make |
484 make |
485 \end{ttbox} |
485 \end{ttbox} |
486 |
486 |
487 When using ML databases made this way to load additional theories or |
487 When using ML databases made this way to load additional theories or |
488 derive other databases from them, you have to be aware that HTML |
488 derive other databases from them, you have to be aware that HTML |
489 generation remains activated. |
489 generation remains activated. Also be especially careful when making |
|
490 such databases publicly available since it means that your users might |
|
491 get into trouble that they don't expect, like IO exceptions caused by |
|
492 insufficient write access. |
490 |
493 |
491 The reason is that the boolean reference variable {\tt make_html} (see |
494 The reason is that the boolean reference variable {\tt make_html} (see |
492 below) is set. Therefore HTML files are generated unless you assign a |
495 below) is set. Therefore HTML files are generated unless you assign a |
493 value of {\tt false} to {\tt make_html}. The only place where the |
496 value of {\tt false} to {\tt make_html}. |
494 environment variable {\tt MAKE_HTML} is used is in the makefile where |
497 |
495 it determines the initial value of {\tt make_html} for a newly made |
498 This is not influenced by the environment variable {\tt MAKE_HTML}, |
|
499 because the only place where it is used is in the makefile where it |
|
500 determines the initial value of {\tt make_html} for a newly made |
496 database. |
501 database. |
497 |
502 |
498 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on |
503 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on |
499 {\tt FOL}) and because the HTML files list a theory's ancestors, you |
504 {\tt FOL}) and because the HTML files list a theory's ancestors, you |
500 should not make HTML files for a logic if the HTML files for the base |
505 should not make HTML files for a logic if the HTML files for the base |