Put projects onto separate pages.

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);
+}
+