diff options
Diffstat (limited to 'html/functions.php3')
| -rw-r--r-- | html/functions.php3 | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/html/functions.php3 b/html/functions.php3 index 75c2291c..86ef295a 100644 --- a/html/functions.php3 +++ b/html/functions.php3 @@ -182,6 +182,8 @@ function htmlshow($filename,$text="",$title="") { } + + /* Markup plain text file, by escaping < and > */ function markup_plain_text($filename) { @@ -262,3 +264,25 @@ function hack_html($filename,$title="") { } + +/* Display a small page with standard header, footer added on. + Much like htmlshow. */ + +function smallpage($filename,$text="",$title="",$message="") { + if ( $text == "") { $text=$filename; }; + if ( $message == "") { $message=$title; }; + if ( $message == "") { $message=$filename; }; + $urlbits = parse_url($filename); + hlink("smallpage.phtml" + . "?title=" . urlencode($title) + . "&file=" . urlencode($urlbits["path"]) + . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]), + $text, $message); +} + +/* Specialised version for projects */ + +function pgproject($filename,$title) { + smallpage("projects/$filename.html",$title,"Proof General Project",$title); +} + |