From: Stefano Zacchiroli Date: Mon, 17 Jul 2006 09:49:29 +0000 (+0000) Subject: - added format table (enable highlighting of differente file formats) X-Git-Tag: make_still_working~7063 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb10d3f0787aabe8548829453a31a355148f1d16;p=helm.git - added format table (enable highlighting of differente file formats) - enclosed highlighted body in
 .. 
- added reference to the used .css --- 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 =