From f1963225783effe6f19d5ad6f44f3c049f76cd6e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Dec 2000 14:15:17 +0000 Subject: [PATCH] All files previously in local/$i/helm moved in $i --- .../local/etc/helm/configuration.dtd | 34 ----------------- .../local/etc/helm/configuration.xml | 22 ----------- .../local/etc/helm/helm-dictionary.xml | 4 -- .../etc/helm/helm-font-configuration.xml | 35 ----------------- .../helm/helm-math-engine-configuration.xml | 37 ------------------ .../local/lib/helm/configuration.pl | 38 ------------------- 6 files changed, 170 deletions(-) delete mode 100644 helm/configuration/local/etc/helm/configuration.dtd delete mode 100644 helm/configuration/local/etc/helm/configuration.xml delete mode 100644 helm/configuration/local/etc/helm/helm-dictionary.xml delete mode 100644 helm/configuration/local/etc/helm/helm-font-configuration.xml delete mode 100644 helm/configuration/local/etc/helm/helm-math-engine-configuration.xml delete mode 100644 helm/configuration/local/lib/helm/configuration.pl diff --git a/helm/configuration/local/etc/helm/configuration.dtd b/helm/configuration/local/etc/helm/configuration.dtd deleted file mode 100644 index 2a2428d1d..000000000 --- a/helm/configuration/local/etc/helm/configuration.dtd +++ /dev/null @@ -1,34 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/configuration/local/etc/helm/configuration.xml b/helm/configuration/local/etc/helm/configuration.xml deleted file mode 100644 index 29672d5e1..000000000 --- a/helm/configuration/local/etc/helm/configuration.xml +++ /dev/null @@ -1,22 +0,0 @@ - - - - - /home/pauillac/coq3/sacerdot/HELM/V6.2/examples - - /home/pauillac/coq3/sacerdot/HELM/dtd - /home/pauillac/coq3/sacerdot/HELM/V6.2/servers.txt - /home/pauillac/coq3/sacerdot/HELM/V6.2/urls_of_uris - - index.txt - /tmp - - /home/lpadovan/helm/PARSER/examples - http://localhost/really_very_local/helm/header/getheader.xml - http://localhost/really_very_local/helm/style/ - http://localhost/cgi-bin/helm/webeq.pl - http://localhost/cgi-bin/helm/webeqp.pl - http://localhost/cgi-bin/helm/use_webeqp.pl - ?baseurl=&stylesheet1=rootcontent.xsl&stylesheet2=content_to_html.xsl&xmluri= - http://localhost:8081/get?uri= - diff --git a/helm/configuration/local/etc/helm/helm-dictionary.xml b/helm/configuration/local/etc/helm/helm-dictionary.xml deleted file mode 100644 index a81bb886b..000000000 --- a/helm/configuration/local/etc/helm/helm-dictionary.xml +++ /dev/null @@ -1,4 +0,0 @@ - - - - diff --git a/helm/configuration/local/etc/helm/helm-font-configuration.xml b/helm/configuration/local/etc/helm/helm-font-configuration.xml deleted file mode 100644 index 19da22c6b..000000000 --- a/helm/configuration/local/etc/helm/helm-font-configuration.xml +++ /dev/null @@ -1,35 +0,0 @@ - - - - - - - - - - - diff --git a/helm/configuration/local/etc/helm/helm-math-engine-configuration.xml b/helm/configuration/local/etc/helm/helm-math-engine-configuration.xml deleted file mode 100644 index 560bd3be3..000000000 --- a/helm/configuration/local/etc/helm/helm-math-engine-configuration.xml +++ /dev/null @@ -1,37 +0,0 @@ - - - - - - /projects/helm/V7/phd/local/etc/helm/helm-dictionary.xml - /projects/helm/local/share/gtkmathview/dictionary.xml - /projects/helm/V7/phd/local/etc/helm/helm-font-configuration.xml - /projects/helm/local/share/gtkmathview/font-configuration.xml - /projects/helm/local/share/gtkmathview/t1.config - - - - - diff --git a/helm/configuration/local/lib/helm/configuration.pl b/helm/configuration/local/lib/helm/configuration.pl deleted file mode 100644 index f761e7129..000000000 --- a/helm/configuration/local/lib/helm/configuration.pl +++ /dev/null @@ -1,38 +0,0 @@ -use XML::Parser; - -use Env; -my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"}; -# this should be the only fixed constant -$configuration_file = - $HELM_CONFIGURATION_PREFIX."/local/etc/helm/configuration.xml"; - -$parser = new XML::Parser(Handlers => {Start => \&handle_start, - End => \&handle_end, - Char => \&handle_char}); - - -$parser->parsefile($configuration_file, ErrorContext => 3); - - -sub handle_start -{ - if ($_[1] eq "value-of") { - $$varname .= ${$_[3]}; - } elsif ($_[1] ne "configuration") { - $varname = $_[1]; - } -} - -sub handle_end -{ - if ($_[1] ne "value-of" && $_[1] ne "configuration") { - # Next line for debugging only: - # print "OK: #$_[1]# := #$$varname#\n"; - $varname = undef; - } -} - -sub handle_char -{ - $$varname .= $_[1]; -} -- 2.39.2