]> matita.cs.unibo.it Git - helm.git/commitdiff
Using autoconf
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Dec 2000 14:11:27 +0000 (14:11 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Dec 2000 14:11:27 +0000 (14:11 +0000)
12 files changed:
helm/configuration/AUTHORS [new file with mode: 0644]
helm/configuration/ChangeLog [new file with mode: 0644]
helm/configuration/Makefile.in [new file with mode: 0644]
helm/configuration/NEWS [new file with mode: 0644]
helm/configuration/README [new file with mode: 0644]
helm/configuration/configure.in [new file with mode: 0644]
helm/configuration/etc/configuration.dtd [new file with mode: 0644]
helm/configuration/etc/configuration.xml [new file with mode: 0644]
helm/configuration/etc/helm-dictionary.xml [new file with mode: 0644]
helm/configuration/etc/helm-font-configuration.xml [new file with mode: 0644]
helm/configuration/etc/helm-math-engine-configuration.xml [new file with mode: 0644]
helm/configuration/lib/configuration.pl [new file with mode: 0644]

diff --git a/helm/configuration/AUTHORS b/helm/configuration/AUTHORS
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/configuration/ChangeLog b/helm/configuration/ChangeLog
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/configuration/Makefile.in b/helm/configuration/Makefile.in
new file mode 100644 (file)
index 0000000..597add5
--- /dev/null
@@ -0,0 +1,8 @@
+HELM_LIB_DIR=@HELM_LIB_DIR@
+HELM_ETC_DIR=@HELM_ETC_DIR@
+
+install:
+       cp lib/configuration.pl $(HELM_LIB_DIR)
+       cp etc/* $(HELM_ETC_DIR)
+
+.PHONY: install
diff --git a/helm/configuration/NEWS b/helm/configuration/NEWS
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/configuration/README b/helm/configuration/README
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/configuration/configure.in b/helm/configuration/configure.in
new file mode 100644 (file)
index 0000000..9a4d94c
--- /dev/null
@@ -0,0 +1,21 @@
+AC_INIT(etc/configuration.xml)
+
+if test "x$prefix" != xNONE; then
+  RESOLVED_PREFIX=$prefix
+else
+  RESOLVED_PREFIX=$ac_default_prefix
+fi
+
+if test "x$exec_prefix" != xNONE; then
+  RESOLVED_EXEC_PREFIX=$exec_prefix
+else
+  RESOLVED_EXEC_PREFIX=$RESOLVED_PREFIX
+fi
+
+HELM_LIB_DIR=$RESOLVED_EXEC_PREFIX/lib/helm
+HELM_ETC_DIR=$RESOLVED_PREFIX/etc/helm
+
+AC_SUBST(HELM_LIB_DIR)
+AC_SUBST(HELM_ETC_DIR)
+
+AC_OUTPUT([Makefile])
diff --git a/helm/configuration/etc/configuration.dtd b/helm/configuration/etc/configuration.dtd
new file mode 100644 (file)
index 0000000..2a2428d
--- /dev/null
@@ -0,0 +1,34 @@
+<?xml encoding="ISO-8859-1"?>
+
+<!--*****************************************************************-->
+<!-- DTD FOR HELM CONFIGURATION FILE:                                -->
+<!--  First draft: June 6 2000, Claudio Sacerdoti Coen               -->
+<!--  Last Revision: June 6 2000, Claudio Sacerdoti Coen             -->
+<!--*****************************************************************-->
+
+<!ELEMENT configuration (helm_dir, dtd_dir, servers_file, uris_dbm, dest,
+                        indexname, tmpdir, helm_url_path,
+                         getheader_url, style_url, webeq_url, webeqp_url,
+                         use_webeqp_url, html_link, getter_url)>
+
+<!ENTITY % expr '(#PCDATA | value-of)*'>
+
+<!ELEMENT value-of EMPTY>
+<!ATTLIST value-of
+       var NMTOKEN #REQUIRED >
+
+<!ELEMENT helm_dir       %expr;>
+<!ELEMENT dtd_dir        %expr;>
+<!ELEMENT servers_file   %expr;>
+<!ELEMENT uris_dbm       %expr;>
+<!ELEMENT dest           %expr;>
+<!ELEMENT indexname      %expr;>
+<!ELEMENT tmpdir         %expr;>
+<!ELEMENT helm_url_path  %expr;>
+<!ELEMENT getheader_url  %expr;>
+<!ELEMENT style_url      %expr;>
+<!ELEMENT webeq_url      %expr;>
+<!ELEMENT webeqp_url     %expr;>
+<!ELEMENT use_webeqp_url %expr;>
+<!ELEMENT html_link      %expr;>
+<!ELEMENT getter_url     %expr;>
diff --git a/helm/configuration/etc/configuration.xml b/helm/configuration/etc/configuration.xml
new file mode 100644 (file)
index 0000000..29672d5
--- /dev/null
@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+<!DOCTYPE configuration SYSTEM "configuration.dtd">
+
+<configuration>
+ <helm_dir>/home/pauillac/coq3/sacerdot/HELM/V6.2/examples</helm_dir>
+
+ <dtd_dir>/home/pauillac/coq3/sacerdot/HELM/dtd</dtd_dir>
+ <servers_file>/home/pauillac/coq3/sacerdot/HELM/V6.2/servers.txt</servers_file>
+ <uris_dbm>/home/pauillac/coq3/sacerdot/HELM/V6.2/urls_of_uris</uris_dbm>
+ <dest><value-of var="helm_dir"/></dest>
+ <indexname>index.txt</indexname>
+ <tmpdir>/tmp</tmpdir>
+
+ <helm_url_path>/home/lpadovan/helm/PARSER/examples</helm_url_path>
+ <getheader_url>http://localhost/really_very_local/helm/header/getheader.xml</getheader_url>
+ <style_url>http://localhost/really_very_local/helm/style/</style_url>
+ <webeq_url>http://localhost/cgi-bin/helm/webeq.pl</webeq_url>
+ <webeqp_url>http://localhost/cgi-bin/helm/webeqp.pl</webeqp_url>
+ <use_webeqp_url>http://localhost/cgi-bin/helm/use_webeqp.pl</use_webeqp_url>
+ <html_link><value-of var="getheader_url"/>?baseurl=<value-of var="style_url"/>&amp;stylesheet1=rootcontent.xsl&amp;stylesheet2=content_to_html.xsl&amp;xmluri=</html_link>
+ <getter_url>http://localhost:8081/get?uri=</getter_url>
+</configuration>
diff --git a/helm/configuration/etc/helm-dictionary.xml b/helm/configuration/etc/helm-dictionary.xml
new file mode 100644 (file)
index 0000000..a81bb88
--- /dev/null
@@ -0,0 +1,4 @@
+<dictionary>
+ <operator name="&Union;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
+ <operator name="&Intersection;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
+</dictionary>
diff --git a/helm/configuration/etc/helm-font-configuration.xml b/helm/configuration/etc/helm-font-configuration.xml
new file mode 100644 (file)
index 0000000..19da22c
--- /dev/null
@@ -0,0 +1,35 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE font-configuration SYSTEM "font-configuration.dtd">
+<!--
+Copyright (C) 2000, Luca Padovani (luca.padovani@cs.unibo.it).
+
+This file is part of GtkMathView, a Gtk widget for MathML.
+
+GtkMathView 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.
+
+GtkMathView 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 GtkMathView; if not, write to the Free Software
+Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+
+For details, see the GtkMathView World-Wide-Web page,
+http://cs.unibo.it/~lpadovan/mml-widget, or send a mail to
+(luca.padovani@cs.unibo.it)
+-->
+
+<font-configuration>
+  <font type="x" mode="math" map="adobe-symbol-forall"
+       x-foundry="adobe" x-family="symbol" x-encoding="fontspecific"
+       />
+
+  <map id="adobe-symbol-forall">
+    <single code="0x2200" index="0x22"/>
+  </map>
+</font-configuration>
diff --git a/helm/configuration/etc/helm-math-engine-configuration.xml b/helm/configuration/etc/helm-math-engine-configuration.xml
new file mode 100644 (file)
index 0000000..560bd3b
--- /dev/null
@@ -0,0 +1,37 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE math-engine-configuration SYSTEM "math-engine-configuration.dtd">
+<!--
+Copyright (C) 2000, Luca Padovani (luca.padovani@cs.unibo.it).
+
+This file is part of GtkMathView, a Gtk widget for MathML.
+
+GtkMathView 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.
+
+GtkMathView 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 GtkMathView; if not, write to the Free Software
+Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+
+For details, see the GtkMathView World-Wide-Web page,
+http://cs.unibo.it/~lpadovan/mml-widget, or send a mail to
+(luca.padovani@cs.unibo.it)
+-->
+
+<math-engine-configuration>
+  <dictionary-path>/projects/helm/V7/phd/local/etc/helm/helm-dictionary.xml</dictionary-path>
+  <dictionary-path>/projects/helm/local/share/gtkmathview/dictionary.xml</dictionary-path>
+  <font-configuration-path>/projects/helm/V7/phd/local/etc/helm/helm-font-configuration.xml</font-configuration-path>
+  <font-configuration-path>/projects/helm/local/share/gtkmathview/font-configuration.xml</font-configuration-path>
+  <t1-config-file>/projects/helm/local/share/gtkmathview/t1.config</t1-config-file>
+  <font-size     size="14pt"/>
+  <color         foreground="black" background="white"/>
+  <link-color    foreground="#32648b" background="white"/>
+  <select-color  foreground="black" background="#87cefa"/>
+</math-engine-configuration>
diff --git a/helm/configuration/lib/configuration.pl b/helm/configuration/lib/configuration.pl
new file mode 100644 (file)
index 0000000..e88d8fb
--- /dev/null
@@ -0,0 +1,40 @@
+use XML::Parser;
+
+use Env;
+my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"};
+# this should be the only fixed constant
+if (defined ($HELM_CONFIGURATION_PREFIX) {
+   $configuration_file =
+    $HELM_CONFIGURATION_PREFIX."/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];
+}