From fb10d3f0787aabe8548829453a31a355148f1d16 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 17 Jul 2006 09:49:29 +0000
Subject: [PATCH] - added format table (enable highlighting of differente file
 formats) - enclosed highlighted body in <pre> .. </pre> - added reference to
 the used .css

---
 helm/www/matita/cgi-bin/hl.cgi | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/helm/www/matita/cgi-bin/hl.cgi b/helm/www/matita/cgi-bin/hl.cgi
index 25e7bcfb5..53926c7fa 100755
--- a/helm/www/matita/cgi-bin/hl.cgi
+++ b/helm/www/matita/cgi-bin/hl.cgi
@@ -33,14 +33,19 @@ use Syntax::Highlight::Universal;
 my $documentroot = '/projects/matita/public_html/';
 my $protohrc = $documentroot . 'helm-proto.hrc';
 my $scriptsdir = $documentroot . 'library/';
-my $hlformat = "grafite";
+
+my %formatmap = (
+  ".ma" => "grafite",
+  ".c" => "c",	# debug
+);
 
 # Code
   
 my $query = CGI->new;                      # used globally by some 'sub' below
-print $query->header, $query->start_html;
+print $query->header;
 
 sub die_invalid_file() {
+  print $query->start_html;
   print 'Invalid script.';
   print $query->end_html;
   exit 0;
@@ -48,12 +53,14 @@ sub die_invalid_file() {
 
 sub lookup_script($) {
   my ($f) = @_;
-  die_invalid_file() unless $f =~ /^(.*)(\.ma)$/;
+  die_invalid_file() unless $f =~ /^(.*)(\.[^.]+)$/;
   my $base = $1;
+  my $extension = $2;
   die_invalid_file() unless $base =~ /[-a-zA-Z_]+(\/[-a-zA-Z_])*/;
+  die_invalid_file() unless exists $formatmap{$extension};
   my $path = $scriptsdir . $f;
   die_invalid_file() unless -f $path;
-  return $path;
+  return ($path, $formatmap{$extension});
 }
 
 my $fname = $query->param('f');
@@ -61,14 +68,16 @@ my $fname = $query->param('f');
 my $highlighter = Syntax::Highlight::Universal->new;
 $highlighter->addConfig($protohrc);
 
-my $script = lookup_script($fname);
+my ($script, $format) = lookup_script($fname);
 open SCRIPT, "< $script" or die "Can't open Matita script \"$script\"\n";
 my @lines = <SCRIPT>;
 my $text = join "", @lines;
 close SCRIPT;
 
-my $result = $highlighter->highlight($hlformat, $text);
+print $query->start_html(-style=>{"src"=>"/$format-format.css"});
+my $result = $highlighter->highlight($format, $text);
+print "<pre>\n";
 print $result;
-
+print "</pre>\n";
 print $query->end_html;
 
-- 
2.39.2