From: Claudio Sacerdoti Coen Date: Fri, 17 Nov 2000 11:40:00 +0000 (+0000) Subject: Initial revision X-Git-Tag: nogzip~163 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eecd02f892cd859e137c550aaa0f2668986c5f2b;p=helm.git Initial revision --- diff --git a/helm/cgi/mkindex.pl b/helm/cgi/mkindex.pl new file mode 100755 index 000000000..9bc41ef11 --- /dev/null +++ b/helm/cgi/mkindex.pl @@ -0,0 +1,93 @@ +#!/usr/bin/perl + +# the required file defines: $helm_dir, $helm_url_path, $getheader_url, +# $style_url, $webeq_url, $webeqp_url +require "/local/lib/helm/configuration.pl"; + +$baseuri0 = $dirname = $uri = $ENV{"REQUEST_URI"}; + +$dirname =~ s/$helm_url_path//; +$dirname = $helm_dir.$dirname; + +$baseuri0 =~ s/$helm_url_path//; + +opendir(DIR, $dirname); +@filenames = readdir(DIR); +closedir(DIR); + +$output = ""; +foreach $i (@filenames) { + if ($i eq "..") { + $output .= < Parent Directory +EOT + } elsif ($i !~ /^\./) { + # hidden files excluded + (undef,undef,$mode) = stat("$dirname$i"); + if ($mode &= 16384) { + # directory + $output .= < $i +EOT + } else { + # file + if ($i =~ /\.(con|var|ind)\.xml$/) { + my $i_without_xml = $i; + $i_without_xml =~ s/(.*)\.xml/$1/; + # cic file + my $baseuri = "cic:".$baseuri0; + $output .= < $i MathML HTML WEBEQ WEBEQ PRESENTATION ONLY +EOT + } elsif ($i =~ /\.(con|var|ind)\.ann\.xml$/) { + my $i_without_xml = $i; + my $i_without_ann_and_xml = $i; + $i_without_xml =~ s/(.*)\.xml/$1/; + $i_without_ann_and_xml =~ s/(.*)\.ann\.xml/$1/; + # cic file + my $baseuri = "cic:".$baseuri0; + $output .= < $i MathML HTML WEBEQ WEBEQ PRESENTATION ONLY +EOT + } elsif ($i =~ /\.theory\.xml$/) { + my $i_without_xml = $i; + $i_without_xml =~ s/(.*)\.xml/$1/; + # theory file + my $baseuri = "theory:".$baseuri0; + $output .= < $i MathML HTML +EOT + } else { + # other file + $output .= < $i +EOT + } + } + } +} + +print < + + +Index of $uri + + +
+Index of $uri +
+
+
+$output
+
+
+ + +EOT diff --git a/helm/dtd/annotations.dtd b/helm/dtd/annotations.dtd new file mode 100644 index 000000000..c7d379983 --- /dev/null +++ b/helm/dtd/annotations.dtd @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd new file mode 100644 index 000000000..e16b10287 --- /dev/null +++ b/helm/dtd/cic.dtd @@ -0,0 +1,176 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd new file mode 100644 index 000000000..1d9917b10 --- /dev/null +++ b/helm/dtd/cicobject.dtd @@ -0,0 +1,97 @@ + + + + + + + + + +%mathml; + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsa.ent b/helm/dtd/isoamsa.ent new file mode 100644 index 000000000..5ecf4db21 --- /dev/null +++ b/helm/dtd/isoamsa.ent @@ -0,0 +1,173 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsb.ent b/helm/dtd/isoamsb.ent new file mode 100644 index 000000000..08e646c2b --- /dev/null +++ b/helm/dtd/isoamsb.ent @@ -0,0 +1,146 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsc.ent b/helm/dtd/isoamsc.ent new file mode 100644 index 000000000..cce399cf9 --- /dev/null +++ b/helm/dtd/isoamsc.ent @@ -0,0 +1,49 @@ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsn.ent b/helm/dtd/isoamsn.ent new file mode 100644 index 000000000..cddeba066 --- /dev/null +++ b/helm/dtd/isoamsn.ent @@ -0,0 +1,117 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamso.ent b/helm/dtd/isoamso.ent new file mode 100644 index 000000000..8ac4bdb61 --- /dev/null +++ b/helm/dtd/isoamso.ent @@ -0,0 +1,77 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isoamsr.ent b/helm/dtd/isoamsr.ent new file mode 100644 index 000000000..7fec58255 --- /dev/null +++ b/helm/dtd/isoamsr.ent @@ -0,0 +1,205 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isobox.ent b/helm/dtd/isobox.ent new file mode 100644 index 000000000..630edc559 --- /dev/null +++ b/helm/dtd/isobox.ent @@ -0,0 +1,67 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isocyr1.ent b/helm/dtd/isocyr1.ent new file mode 100644 index 000000000..4bcc9e416 --- /dev/null +++ b/helm/dtd/isocyr1.ent @@ -0,0 +1,94 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isocyr2.ent b/helm/dtd/isocyr2.ent new file mode 100644 index 000000000..67c477b24 --- /dev/null +++ b/helm/dtd/isocyr2.ent @@ -0,0 +1,53 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isodia.ent b/helm/dtd/isodia.ent new file mode 100644 index 000000000..ba6496300 --- /dev/null +++ b/helm/dtd/isodia.ent @@ -0,0 +1,41 @@ + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isogrk3.ent b/helm/dtd/isogrk3.ent new file mode 100644 index 000000000..fa0335504 --- /dev/null +++ b/helm/dtd/isogrk3.ent @@ -0,0 +1,70 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isolat1.ent b/helm/dtd/isolat1.ent new file mode 100644 index 000000000..849d360ae --- /dev/null +++ b/helm/dtd/isolat1.ent @@ -0,0 +1,89 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isolat2.ent b/helm/dtd/isolat2.ent new file mode 100644 index 000000000..3049be7f1 --- /dev/null +++ b/helm/dtd/isolat2.ent @@ -0,0 +1,148 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isomfrk.ent b/helm/dtd/isomfrk.ent new file mode 100644 index 000000000..d3d92aaee --- /dev/null +++ b/helm/dtd/isomfrk.ent @@ -0,0 +1,79 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isomopf.ent b/helm/dtd/isomopf.ent new file mode 100644 index 000000000..6b5e01f79 --- /dev/null +++ b/helm/dtd/isomopf.ent @@ -0,0 +1,53 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isomscr.ent b/helm/dtd/isomscr.ent new file mode 100644 index 000000000..75d3bc5df --- /dev/null +++ b/helm/dtd/isomscr.ent @@ -0,0 +1,79 @@ + + + +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > +" > diff --git a/helm/dtd/isonum.ent b/helm/dtd/isonum.ent new file mode 100644 index 000000000..d6d346169 --- /dev/null +++ b/helm/dtd/isonum.ent @@ -0,0 +1,106 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isopub.ent b/helm/dtd/isopub.ent new file mode 100644 index 000000000..5591fc390 --- /dev/null +++ b/helm/dtd/isopub.ent @@ -0,0 +1,111 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/isotech.ent b/helm/dtd/isotech.ent new file mode 100644 index 000000000..8b30af833 --- /dev/null +++ b/helm/dtd/isotech.ent @@ -0,0 +1,183 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +" > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mathml2-qname-1.mod b/helm/dtd/mathml2-qname-1.mod new file mode 100644 index 000000000..4dea63a00 --- /dev/null +++ b/helm/dtd/mathml2-qname-1.mod @@ -0,0 +1,268 @@ + + + + + + + + + + + + + + + + + + + + + + + +]]> + + + + +]]> + + + + +]]> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mathml2.dtd b/helm/dtd/mathml2.dtd new file mode 100644 index 000000000..a9b7bf1ac --- /dev/null +++ b/helm/dtd/mathml2.dtd @@ -0,0 +1,1948 @@ + + + + + + + + + +%mathml-qname.mod;]]> + + +--> + +]]> + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +%ent-isoamsa; + + +%ent-isoamsb; + + +%ent-isoamsc; + + +%ent-isoamsn; + + +%ent-isoamso; + + +%ent-isoamsr; + + +%ent-isogrk3; + + +%ent-isomfrk; + + +%ent-isomopf; + + +%ent-isomscr; + + +%ent-isotech; + + + + +%ent-isobox; + + +%ent-isocyr1; + + +%ent-isocyr2; + + +%ent-isodia; + + +%ent-isolat1; + + +%ent-isolat2; + + +%ent-isonum; + + +%ent-isopub; + + + + +%ent-mmlextra; + + + + +%ent-mmlalias; + +]]> + + + + + + diff --git a/helm/dtd/maththeory.dtd b/helm/dtd/maththeory.dtd new file mode 100644 index 000000000..85469b6ce --- /dev/null +++ b/helm/dtd/maththeory.dtd @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mmlalias.ent b/helm/dtd/mmlalias.ent new file mode 100644 index 000000000..f5901b384 --- /dev/null +++ b/helm/dtd/mmlalias.ent @@ -0,0 +1,529 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/mmlextra.ent b/helm/dtd/mmlextra.ent new file mode 100644 index 000000000..e76de448c --- /dev/null +++ b/helm/dtd/mmlextra.ent @@ -0,0 +1,134 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/dtd/provastruct.theory.xml b/helm/dtd/provastruct.theory.xml new file mode 100644 index 000000000..23c8f7c6d --- /dev/null +++ b/helm/dtd/provastruct.theory.xml @@ -0,0 +1,158 @@ + + + +
+ +
+ + cast + + Prop + + + Type + + + +
+ + cast + + Prop + + + Type + + + + 1: A 0: B + cast + + arrow + A + + arrow + arrow + A + + B + + + B + + + + + Prop + + + + 1: A 0: B + A0 + A + + H + arrow + A + + B + + + app + conj + A + B + A0 + app + axiom + A0 + H + + + + + + cast + + arrow + A + + arrow + arrow + A + + B + + + AB + + + + + Prop + + + +
+
+ + cast + + Set + + + Type + + + + 1: A + cast + + prodA + Prop + + arrow + A + + A + + + + + Prop + + + +
+ 0: A + A0 + Prop + + H + A0 + + H + + + + cast + + prodA + Prop + + arrow + A + + A + + + + + Prop + + + +
+
+ + diff --git a/helm/dtd/theoryobject.dtd b/helm/dtd/theoryobject.dtd new file mode 100644 index 000000000..8ff26cfb2 --- /dev/null +++ b/helm/dtd/theoryobject.dtd @@ -0,0 +1,14 @@ + + + + + + + + + +%cicobj; + + + + diff --git a/helm/header/getheader.xml b/helm/header/getheader.xml new file mode 100644 index 000000000..a0f903f87 --- /dev/null +++ b/helm/header/getheader.xml @@ -0,0 +1,21 @@ + + + + + + + + + String baseURL = request.getParameter("baseurl"); + String styleURL1 = request.getParameter("stylesheet1"); + String styleURL2 = request.getParameter("stylesheet2"); + String xmlURI = request.getParameter("xmluri"); + String annURI = request.getParameter("annuri"); + + baseURL + styleURL1 + styleURL2 + xmlURI + annURI + + diff --git a/helm/header/provaurl b/helm/header/provaurl new file mode 100644 index 000000000..86344dc78 --- /dev/null +++ b/helm/header/provaurl @@ -0,0 +1 @@ +http://phd.cs.unibo.it/helm/PARSER/examples/header/getheader.xml?baseurl=http://cartoonia.cs.unibo.it/helm/PARSER/examples/style/&stylesheet1=content.xsl&stylesheet2=mmlextension.xsl&xmlfile=file:///really_very_local/helm/PARSER/examples/prove/provaIota/bool_ind.con.xml diff --git a/helm/header/provaurl1 b/helm/header/provaurl1 new file mode 100644 index 000000000..d95769884 --- /dev/null +++ b/helm/header/provaurl1 @@ -0,0 +1,2 @@ +http://cartoonia.cs.unibo.it/helm/PARSER/examples/header/getheader.xml?baseurl=http://cartoonia.cs.unibo.it/helm/PARSER/examples/style/&stylesheet1=content.xsl&stylesheet2=content_to_html.xsl&xmlfile=/really_very_local/helm/PARSER/examples/prove/prova/forest_rec.con.xml:wq + diff --git a/helm/header/setheader.xsl b/helm/header/setheader.xsl new file mode 100644 index 000000000..a1ba13199 --- /dev/null +++ b/helm/header/setheader.xsl @@ -0,0 +1,33 @@ + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + +