X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fcgi-bin%2Fhl.cgi;h=f2a146ccc98355f503cb632f72d25ab60d5ee592;hb=ab8006e4e28764820462d5963b0e87c210376ccd;hp=25e7bcfb5594b54ed44c744aa2bfc8889f0defff;hpb=228d207d77101f153312e1c2cef1b8f2b5ec329f;p=helm.git

diff --git a/helm/www/matita/cgi-bin/hl.cgi b/helm/www/matita/cgi-bin/hl.cgi
index 25e7bcfb5..f2a146ccc 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(-type=>'text/html', -charset=>'utf-8');
 
 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,17 @@ 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;
+my $text = join '', @lines;
 close SCRIPT;
 
-my $result = $highlighter->highlight($hlformat, $text);
+print $query->start_html(-style=>{'src'=>"/$format-format.css"},
+			 -encoding=>'utf-8');
+my $result = $highlighter->highlight($format, $text);
+print "<pre>\n";
 print $result;
-
+print "</pre>\n";
 print $query->end_html;