From 228d207d77101f153312e1c2cef1b8f2b5ec329f Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 14 Jul 2006 12:54:10 +0000
Subject: [PATCH] proof of concept implementation of scripts highlighting,
 grafite.hrc is still bugged

---
 helm/www/matita/cgi-bin/hl.cgi |  74 +++++++++++++
 helm/www/matita/grafite.hrc    | 188 +++++++++++++++++++++++++++++++++
 helm/www/matita/helm-proto.hrc |  22 ++++
 3 files changed, 284 insertions(+)
 create mode 100755 helm/www/matita/cgi-bin/hl.cgi
 create mode 100644 helm/www/matita/grafite.hrc
 create mode 100644 helm/www/matita/helm-proto.hrc

diff --git a/helm/www/matita/cgi-bin/hl.cgi b/helm/www/matita/cgi-bin/hl.cgi
new file mode 100755
index 000000000..25e7bcfb5
--- /dev/null
+++ b/helm/www/matita/cgi-bin/hl.cgi
@@ -0,0 +1,74 @@
+#!/usr/bin/perl -w
+use strict;
+
+# Copyright (C) 2006, HELM Team.
+#
+# This file is part of HELM, an Hypertextual, Electronic
+# Library of Mathematics, developed at the Computer Science
+# Department, University of Bologna, Italy.
+#
+# HELM is free software; you can redistribute it and/or
+# modify it under the terms of the GNU General Public License
+# as published by the Free Software Foundation; either version 2
+# of the License, or (at your option) any later version.
+#
+# HELM is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with HELM; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+# MA  02111-1307, USA.
+#
+# For details, see the HELM World-Wide-Web page,
+# http://helm.cs.unibo.it/
+
+use CGI;
+use Syntax::Highlight::Universal;
+
+# Configuration
+
+my $documentroot = '/projects/matita/public_html/';
+my $protohrc = $documentroot . 'helm-proto.hrc';
+my $scriptsdir = $documentroot . 'library/';
+my $hlformat = "grafite";
+
+# Code
+  
+my $query = CGI->new;                      # used globally by some 'sub' below
+print $query->header, $query->start_html;
+
+sub die_invalid_file() {
+  print 'Invalid script.';
+  print $query->end_html;
+  exit 0;
+}
+
+sub lookup_script($) {
+  my ($f) = @_;
+  die_invalid_file() unless $f =~ /^(.*)(\.ma)$/;
+  my $base = $1;
+  die_invalid_file() unless $base =~ /[-a-zA-Z_]+(\/[-a-zA-Z_])*/;
+  my $path = $scriptsdir . $f;
+  die_invalid_file() unless -f $path;
+  return $path;
+}
+
+my $fname = $query->param('f');
+
+my $highlighter = Syntax::Highlight::Universal->new;
+$highlighter->addConfig($protohrc);
+
+my $script = 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 $result;
+
+print $query->end_html;
+
diff --git a/helm/www/matita/grafite.hrc b/helm/www/matita/grafite.hrc
new file mode 100644
index 000000000..4b88fa91d
--- /dev/null
+++ b/helm/www/matita/grafite.hrc
@@ -0,0 +1,188 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE language SYSTEM "language.dtd">
+<language _name="grafite" version="1.0" _section="Sources" mimetypes="text/x-matita">
+
+  <escape-char>\</escape-char>
+
+  <block-comment _name = "Commented Code" style = "Comment">
+    <start-regex>\(\*\*[^\)]</start-regex>
+    <end-regex>[^\(]\*\*\)</end-regex>
+  </block-comment>
+
+  <block-comment _name = "Block Comment" style = "Comment">
+    <start-regex>\(\*</start-regex>
+    <end-regex>\*\)</end-regex>
+  </block-comment>
+
+  <keyword-list _name = "Theorem Kinds" style = "Keyword" case-sensitive="TRUE">
+    <keyword>theorem</keyword>
+    <keyword>definition</keyword>
+    <keyword>lemma</keyword>
+    <keyword>fact</keyword>
+    <keyword>remark</keyword>
+    <keyword>variant</keyword>
+    <keyword>axiom</keyword>
+  </keyword-list>
+    
+  <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">
+    <keyword>alias</keyword>
+    <keyword>and</keyword>
+    <keyword>as</keyword>
+    <keyword>coercion</keyword>
+    <keyword>coinductive</keyword>
+    <keyword>corec</keyword>
+    <keyword>default</keyword>
+    <keyword>for</keyword>
+    <keyword>include</keyword>
+    <keyword>include'</keyword>
+    <keyword>inductive</keyword>
+    <keyword>in</keyword>
+    <keyword>interpretation</keyword>
+    <keyword>let</keyword>
+    <keyword>match</keyword>
+    <keyword>names</keyword>
+    <keyword>notation</keyword>
+    <keyword>on</keyword>
+    <keyword>qed</keyword>
+    <keyword>rec</keyword>
+    <keyword>record</keyword>
+    <keyword>return</keyword>
+    <keyword>to</keyword>
+    <keyword>using</keyword>
+    <keyword>with</keyword>
+  </keyword-list>
+
+  <pattern-item _name = "Command [" style = "Keyword">
+    <regex>\[</regex>
+  </pattern-item>
+  <pattern-item _name = "Command |" style = "Keyword">
+    <regex>\|</regex>
+  </pattern-item>
+  <pattern-item _name = "Command ]" style = "Keyword">
+    <regex>\]</regex>
+  </pattern-item>
+  <pattern-item _name = "Command {" style = "Keyword">
+    <regex>\{</regex>
+  </pattern-item>
+  <pattern-item _name = "Command }" style = "Keyword">
+    <regex>\}</regex>
+  </pattern-item>
+  <pattern-item _name = "Notation ast mark" style = "Keyword">
+    <regex>@</regex>
+  </pattern-item>
+  <pattern-item _name = "Notation meta mark" style = "Keyword">
+    <regex>\$</regex>
+  </pattern-item>
+
+  <keyword-list _name = "Sorts" style = "Data Type" case-sensitive="TRUE">
+    <keyword>Set</keyword>
+    <keyword>Prop</keyword>
+    <keyword>Type</keyword>
+  </keyword-list>
+
+  <keyword-list _name = "Tactics" style = "Others 2" case-sensitive="TRUE">
+    <keyword>absurd</keyword>
+    <keyword>apply</keyword>
+    <keyword>assumption</keyword>
+    <keyword>auto</keyword>
+    <keyword>paramodulation</keyword>
+    <keyword>clear</keyword>
+    <keyword>clearbody</keyword>
+    <keyword>change</keyword>
+    <keyword>constructor</keyword>
+    <keyword>contradiction</keyword>
+    <keyword>cut</keyword>
+    <keyword>decompose</keyword>
+    <keyword>discriminate</keyword>
+    <keyword>elim</keyword>
+    <keyword>elimType</keyword>
+    <keyword>exact</keyword>
+    <keyword>exists</keyword>
+    <keyword>fail</keyword>
+    <keyword>fold</keyword>
+    <keyword>fourier</keyword>
+    <keyword>fwd</keyword>
+    <keyword>generalize</keyword>
+    <keyword>goal</keyword>
+    <keyword>id</keyword>
+    <keyword>injection</keyword>
+    <keyword>intro</keyword>
+    <keyword>intros</keyword>
+    <keyword>inversion</keyword>
+    <keyword>lapply</keyword>
+    <keyword>linear</keyword>
+    <keyword>left</keyword>
+    <keyword>letin</keyword>
+    <keyword>normalize</keyword>
+    <keyword>reduce</keyword>
+    <keyword>reflexivity</keyword>
+    <keyword>replace</keyword>
+    <keyword>rewrite</keyword>
+    <keyword>ring</keyword>
+    <keyword>right</keyword>
+    <keyword>symmetry</keyword>
+    <keyword>simplify</keyword>
+    <keyword>split</keyword>
+    <keyword>to</keyword>
+    <keyword>transitivity</keyword>
+    <keyword>unfold</keyword>
+    <keyword>whd</keyword>
+  </keyword-list>
+
+  <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
+    <keyword>try</keyword>
+    <keyword>solve</keyword>
+    <keyword>do</keyword>
+    <keyword>repeat</keyword>
+    <keyword>first</keyword>
+    <keyword>focus</keyword>
+    <keyword>unfocus</keyword>
+  </keyword-list>
+
+
+  <keyword-list _name = "Matita Macro" style = "Others 3" case-sensitive="TRUE">
+    <keyword>check</keyword>
+    <keyword>hint</keyword>
+    <keyword>set</keyword>
+  </keyword-list>
+  
+  <keyword-list _name = "Whelp Macro" style = "Others 3"
+    case-sensitive="TRUE" 
+    beginning-regex="whelp *" 
+    match-empty-string-at-beginning="FALSE"
+    match-empty-string-at-end="FALSE" >
+    <keyword>elim</keyword>
+    <keyword>hint</keyword>
+    <keyword>instance</keyword>
+    <keyword>locate</keyword>
+    <keyword>match</keyword>
+  </keyword-list>
+    
+  <keyword-list _name = "TeX Macro" style = "Preprocessor" 
+    case-sensitive="TRUE" 
+    beginning-regex="\\" 
+    match-empty-string-at-beginning="FALSE"
+    match-empty-string-at-end="FALSE" >
+     <keyword>def</keyword>
+     <keyword>forall</keyword>
+     <keyword>lambda</keyword>
+     <keyword>to</keyword>
+     <keyword>exists</keyword>
+     <keyword>Rightarrow</keyword>
+     <keyword>Assign</keyword>
+     <keyword>land</keyword>
+     <keyword>lor</keyword>
+     <keyword>lnot</keyword>
+     <keyword>liff</keyword>
+     <keyword>subst</keyword>
+     <keyword>vdash</keyword>
+     <keyword>iforall</keyword>
+     <keyword>iexists</keyword>
+  </keyword-list>
+
+  <string _name = "String" style = "String" >
+    <start-regex>&quot;</start-regex>
+    <end-regex>&quot;</end-regex>
+  </string>
+ 
+</language>
diff --git a/helm/www/matita/helm-proto.hrc b/helm/www/matita/helm-proto.hrc
new file mode 100644
index 000000000..f67842452
--- /dev/null
+++ b/helm/www/matita/helm-proto.hrc
@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding='Windows-1251'?>
+<!DOCTYPE hrc PUBLIC "-//Cail Lomecb//DTD Colorer HRC take5//EN"
+  "http://colorer.sf.net/2003/hrc.dtd">
+<hrc version="take5" xmlns="http://colorer.sf.net/2003/hrc"
+     xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+     xsi:schemaLocation="http://colorer.sf.net/2003/hrc http://colorer.sf.net/2003/hrc.xsd">
+
+  <annotation>
+   <documentation>
+   This is a base HRC file with prototype defines and types linking information.
+   </documentation>
+  </annotation>
+
+  <!--  main languages  -->
+  <prototype name="grafite" group="helm" description="Matita script language">
+    <location link="grafite.hrc" />
+    <filename>/\.ma$/i</filename>
+  </prototype>
+
+  <type name="default"><scheme name="grafite"/></type>
+
+</hrc>
-- 
2.39.2