diff options
| author | David Aspinall | 1999-10-15 17:49:29 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-15 17:49:29 +0000 |
| commit | 564a582e9f3b8f491a553c6db5eb6d156157e068 (patch) | |
| tree | d0a6bd0360c3d3fd1b6e1027556a048107177117 | |
| parent | ac5723025f1de3b6d7131b58b42fa6d4a867efe5 (diff) | |
Doc fixes, php streamlining
| -rw-r--r-- | html/doc.phtml | 2 | ||||
| -rw-r--r-- | html/features.phtml | 2 | ||||
| -rw-r--r-- | html/functions.php3 | 22 | ||||
| -rw-r--r-- | html/notes.txt | 2 |
4 files changed, 14 insertions, 14 deletions
diff --git a/html/doc.phtml b/html/doc.phtml index 7f1f9a10..221fdb3f 100644 --- a/html/doc.phtml +++ b/html/doc.phtml @@ -1,7 +1,7 @@ <h2>Manual</h2> <p> -Here is the Proof +Here is the <?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","Proof General manual","Proof General Manual") ?> in HTML form. <br> For printing you can download the diff --git a/html/features.phtml b/html/features.phtml index 4c0e1819..3e5e4c55 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -39,7 +39,7 @@ assistant, and you'd like some of the following features: coloured to reflect whether the proof assistant has loaded it in this session. <p> - Dependencies between script files is + Dependencies between script files are communicated from the proof assistant to Proof General. If you want to edit a file which has been loaded into the proof assistant already, Proof General will unlock the file diff --git a/html/functions.php3 b/html/functions.php3 index 3d215f4f..65e9b155 100644 --- a/html/functions.php3 +++ b/html/functions.php3 @@ -12,6 +12,13 @@ // +// Project configuration + +$project_email = "proofgen@dcs.ed.ac.uk"; +$project_list = "proofgeneral@dcs.ed.ac.uk"; +$project_title = "Proof General" +$project_subtitle = "Organize your Proofs!"; + // DTD $dtd_strict = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.0//EN\" \"http://www.w3.org/TR/REC-html40/strict.dtd\">\n"; @@ -24,19 +31,12 @@ print $dtd_loose; $validator = "http://validator.dcs.ed.ac.uk/"; // $validator = "http://localhost/validator/"; -/* Some handy constants */ - -$pg_email = "proofgen@dcs.ed.ac.uk"; -$pg_list = "proofgeneral@dcs.ed.ac.uk"; - -$pg_title = "Proof General --- Organize your Proofs!"; - function mlink($addr) { print "<a href=\"mailto:" . $addr . "\">" . $addr . "</a>"; } -function pg_email() { - mlink("proofgen@dcs.ed.ac.uk"); +function project_email() { + mlink($project_email); } @@ -147,7 +147,9 @@ function footer($filemodified=".") { } function click_to_go_back() { - print "<p>\nClick <a href=\"index.phtml\">here</a> to go back to the Proof General front page.</p>\n"; + print "<p>\nClick <a href=\"index.phtml\">here</a> to go back to the "; + print $project_title; + print " front page.</p>\n"; } /* Link to a marked up file */ diff --git a/html/notes.txt b/html/notes.txt index 3698a1e6..b73a7db1 100644 --- a/html/notes.txt +++ b/html/notes.txt @@ -30,5 +30,3 @@ Suggestions for improving web pages after Rod reading them: - separate feature list - explain what a proof script is and what script management buys you -Get Dave a laptop to do demos on! - |