From 2b2b90087f836c2f32291935216549e9370e68c3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 18:20:44 +0000 Subject: [PATCH] dir reorganization --- .../{ => DEVEL}/gtkmathview-bonobo/.cvsignore | 0 helm/{ => DEVEL}/gtkmathview-bonobo/AUTHORS | 0 helm/{ => DEVEL}/gtkmathview-bonobo/ChangeLog | 0 helm/{ => DEVEL}/gtkmathview-bonobo/LICENSE | 0 .../gtkmathview-bonobo/Makefile.am | 0 helm/{ => DEVEL}/gtkmathview-bonobo/NEWS | 0 helm/{ => DEVEL}/gtkmathview-bonobo/README | 0 helm/{ => DEVEL}/gtkmathview-bonobo/TODO | 0 .../gtkmathview-bonobo/configure.ac | 0 .../gtkmathview-bonobo.pc.in | 0 .../gtkmathview-bonobo/idl/.cvsignore | 0 .../gtkmathview-bonobo/idl/GtkMathView.idl | 0 .../gtkmathview-bonobo/idl/Makefile.am | 0 .../gtkmathview-bonobo/src/.cvsignore | 0 .../src/GNOME_GtkMathView.server.in.in | 0 .../gtkmathview-bonobo/src/Makefile.am | 0 .../{ => DEVEL}/gtkmathview-bonobo/src/aux.cc | 0 helm/{ => DEVEL}/gtkmathview-bonobo/src/aux.h | 0 .../gtkmathview-bonobo/src/control-data.c | 0 .../gtkmathview-bonobo/src/control-data.h | 0 .../gtkmathview-bonobo/src/control-factory.c | 0 .../gtkmathview-bonobo/src/control-factory.h | 0 .../gtkmathview-bonobo/src/handlers.c | 0 .../gtkmathview-bonobo/src/handlers.h | 0 .../gtkmathview-bonobo/src/persist-file.c | 0 .../gtkmathview-bonobo/src/persist-file.h | 0 .../gtkmathview-bonobo/src/persist-stream.c | 0 .../gtkmathview-bonobo/src/persist-stream.h | 0 .../{ => DEVEL}/gtkmathview-bonobo/src/view.c | 0 .../{ => DEVEL}/gtkmathview-bonobo/src/view.h | 0 .../gtkmathview-bonobo/test/.cvsignore | 0 .../gtkmathview-bonobo/test/Makefile.am | 0 .../gtkmathview-bonobo/test/embedding.html | 0 .../gtkmathview-bonobo/test/embedding.xml | 0 .../gtkmathview-bonobo/test/main.c | 0 .../gtkmathview-bonobo/test/test.mml | 0 .../test/testembedding.html | 0 helm/annotationHelper/.cvsignore | 1 - helm/annotationHelper/.depend | 4 - helm/annotationHelper/Makefile | 47 -- helm/annotationHelper/cicAnnotationHelper.ml | 594 ------------------ helm/annotationHelper/cicAnnotationHinter.ml | 393 ------------ helm/annotationHelper/cicAnnotationHinter.mli | 46 -- helm/cgi/mkcontrol.pl | 109 ---- helm/cgi/mkheader.pl | 44 -- helm/cgi/mkindex.pl | 52 -- helm/cgi/mkindexcic.pl | 113 ---- helm/cgi/mkindextheory.pl | 112 ---- helm/configuration/.cvsignore | 3 - helm/configuration/AUTHORS | 4 - helm/configuration/COPYING | 340 ---------- helm/configuration/ChangeLog | 1 - helm/configuration/Makefile.in | 47 -- helm/configuration/NEWS | 1 - helm/configuration/README | 8 - helm/configuration/config.cache.pkg | 15 - helm/configuration/configure.in | 186 ------ helm/configuration/etc/.cvsignore | 1 - helm/configuration/etc/configuration.dtd | 60 -- helm/configuration/etc/configuration.xml.in | 49 -- helm/configuration/etc/helm-dictionary.xml | 31 - .../etc/helm-font-configuration.xml | 36 -- .../etc/helm-math-engine-configuration.xml.in | 38 -- helm/configuration/helm-config.in | 84 --- helm/configuration/helm_configuration.spec.in | 43 -- helm/configuration/lib/.cvsignore | 1 - helm/configuration/lib/configuration.pl.in | 65 -- helm/configuration/library/servers.txt | 1 - helm/configuration/library/urls_of_uris.db | Bin 4096 -> 0 bytes 69 files changed, 2529 deletions(-) rename helm/{ => DEVEL}/gtkmathview-bonobo/.cvsignore (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/AUTHORS (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/ChangeLog (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/LICENSE (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/Makefile.am (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/NEWS (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/README (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/TODO (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/configure.ac (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/gtkmathview-bonobo.pc.in (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/idl/.cvsignore (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/idl/GtkMathView.idl (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/idl/Makefile.am (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/.cvsignore (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/GNOME_GtkMathView.server.in.in (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/Makefile.am (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/aux.cc (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/aux.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/control-data.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/control-data.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/control-factory.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/control-factory.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/handlers.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/handlers.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/persist-file.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/persist-file.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/persist-stream.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/persist-stream.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/view.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/src/view.h (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/.cvsignore (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/Makefile.am (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/embedding.html (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/embedding.xml (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/main.c (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/test.mml (100%) rename helm/{ => DEVEL}/gtkmathview-bonobo/test/testembedding.html (100%) delete mode 100644 helm/annotationHelper/.cvsignore delete mode 100644 helm/annotationHelper/.depend delete mode 100644 helm/annotationHelper/Makefile delete mode 100644 helm/annotationHelper/cicAnnotationHelper.ml delete mode 100644 helm/annotationHelper/cicAnnotationHinter.ml delete mode 100644 helm/annotationHelper/cicAnnotationHinter.mli delete mode 100755 helm/cgi/mkcontrol.pl delete mode 100755 helm/cgi/mkheader.pl delete mode 100755 helm/cgi/mkindex.pl delete mode 100755 helm/cgi/mkindexcic.pl delete mode 100755 helm/cgi/mkindextheory.pl delete mode 100644 helm/configuration/.cvsignore delete mode 100644 helm/configuration/AUTHORS delete mode 100644 helm/configuration/COPYING delete mode 100644 helm/configuration/ChangeLog delete mode 100644 helm/configuration/Makefile.in delete mode 100644 helm/configuration/NEWS delete mode 100644 helm/configuration/README delete mode 100644 helm/configuration/config.cache.pkg delete mode 100644 helm/configuration/configure.in delete mode 100644 helm/configuration/etc/.cvsignore delete mode 100644 helm/configuration/etc/configuration.dtd delete mode 100644 helm/configuration/etc/configuration.xml.in delete mode 100644 helm/configuration/etc/helm-dictionary.xml delete mode 100644 helm/configuration/etc/helm-font-configuration.xml delete mode 100644 helm/configuration/etc/helm-math-engine-configuration.xml.in delete mode 100644 helm/configuration/helm-config.in delete mode 100644 helm/configuration/helm_configuration.spec.in delete mode 100644 helm/configuration/lib/.cvsignore delete mode 100644 helm/configuration/lib/configuration.pl.in delete mode 100644 helm/configuration/library/servers.txt delete mode 100644 helm/configuration/library/urls_of_uris.db diff --git a/helm/gtkmathview-bonobo/.cvsignore b/helm/DEVEL/gtkmathview-bonobo/.cvsignore similarity index 100% rename from helm/gtkmathview-bonobo/.cvsignore rename to helm/DEVEL/gtkmathview-bonobo/.cvsignore diff --git a/helm/gtkmathview-bonobo/AUTHORS b/helm/DEVEL/gtkmathview-bonobo/AUTHORS similarity index 100% rename from helm/gtkmathview-bonobo/AUTHORS rename to helm/DEVEL/gtkmathview-bonobo/AUTHORS diff --git a/helm/gtkmathview-bonobo/ChangeLog b/helm/DEVEL/gtkmathview-bonobo/ChangeLog similarity index 100% rename from helm/gtkmathview-bonobo/ChangeLog rename to helm/DEVEL/gtkmathview-bonobo/ChangeLog diff --git a/helm/gtkmathview-bonobo/LICENSE b/helm/DEVEL/gtkmathview-bonobo/LICENSE similarity index 100% rename from helm/gtkmathview-bonobo/LICENSE rename to helm/DEVEL/gtkmathview-bonobo/LICENSE diff --git a/helm/gtkmathview-bonobo/Makefile.am b/helm/DEVEL/gtkmathview-bonobo/Makefile.am similarity index 100% rename from helm/gtkmathview-bonobo/Makefile.am rename to helm/DEVEL/gtkmathview-bonobo/Makefile.am diff --git a/helm/gtkmathview-bonobo/NEWS b/helm/DEVEL/gtkmathview-bonobo/NEWS similarity index 100% rename from helm/gtkmathview-bonobo/NEWS rename to helm/DEVEL/gtkmathview-bonobo/NEWS diff --git a/helm/gtkmathview-bonobo/README b/helm/DEVEL/gtkmathview-bonobo/README similarity index 100% rename from helm/gtkmathview-bonobo/README rename to helm/DEVEL/gtkmathview-bonobo/README diff --git a/helm/gtkmathview-bonobo/TODO b/helm/DEVEL/gtkmathview-bonobo/TODO similarity index 100% rename from helm/gtkmathview-bonobo/TODO rename to helm/DEVEL/gtkmathview-bonobo/TODO diff --git a/helm/gtkmathview-bonobo/configure.ac b/helm/DEVEL/gtkmathview-bonobo/configure.ac similarity index 100% rename from helm/gtkmathview-bonobo/configure.ac rename to helm/DEVEL/gtkmathview-bonobo/configure.ac diff --git a/helm/gtkmathview-bonobo/gtkmathview-bonobo.pc.in b/helm/DEVEL/gtkmathview-bonobo/gtkmathview-bonobo.pc.in similarity index 100% rename from helm/gtkmathview-bonobo/gtkmathview-bonobo.pc.in rename to helm/DEVEL/gtkmathview-bonobo/gtkmathview-bonobo.pc.in diff --git a/helm/gtkmathview-bonobo/idl/.cvsignore b/helm/DEVEL/gtkmathview-bonobo/idl/.cvsignore similarity index 100% rename from helm/gtkmathview-bonobo/idl/.cvsignore rename to helm/DEVEL/gtkmathview-bonobo/idl/.cvsignore diff --git a/helm/gtkmathview-bonobo/idl/GtkMathView.idl b/helm/DEVEL/gtkmathview-bonobo/idl/GtkMathView.idl similarity index 100% rename from helm/gtkmathview-bonobo/idl/GtkMathView.idl rename to helm/DEVEL/gtkmathview-bonobo/idl/GtkMathView.idl diff --git a/helm/gtkmathview-bonobo/idl/Makefile.am b/helm/DEVEL/gtkmathview-bonobo/idl/Makefile.am similarity index 100% rename from helm/gtkmathview-bonobo/idl/Makefile.am rename to helm/DEVEL/gtkmathview-bonobo/idl/Makefile.am diff --git a/helm/gtkmathview-bonobo/src/.cvsignore b/helm/DEVEL/gtkmathview-bonobo/src/.cvsignore similarity index 100% rename from helm/gtkmathview-bonobo/src/.cvsignore rename to helm/DEVEL/gtkmathview-bonobo/src/.cvsignore diff --git a/helm/gtkmathview-bonobo/src/GNOME_GtkMathView.server.in.in b/helm/DEVEL/gtkmathview-bonobo/src/GNOME_GtkMathView.server.in.in similarity index 100% rename from helm/gtkmathview-bonobo/src/GNOME_GtkMathView.server.in.in rename to helm/DEVEL/gtkmathview-bonobo/src/GNOME_GtkMathView.server.in.in diff --git a/helm/gtkmathview-bonobo/src/Makefile.am b/helm/DEVEL/gtkmathview-bonobo/src/Makefile.am similarity index 100% rename from helm/gtkmathview-bonobo/src/Makefile.am rename to helm/DEVEL/gtkmathview-bonobo/src/Makefile.am diff --git a/helm/gtkmathview-bonobo/src/aux.cc b/helm/DEVEL/gtkmathview-bonobo/src/aux.cc similarity index 100% rename from helm/gtkmathview-bonobo/src/aux.cc rename to helm/DEVEL/gtkmathview-bonobo/src/aux.cc diff --git a/helm/gtkmathview-bonobo/src/aux.h b/helm/DEVEL/gtkmathview-bonobo/src/aux.h similarity index 100% rename from helm/gtkmathview-bonobo/src/aux.h rename to helm/DEVEL/gtkmathview-bonobo/src/aux.h diff --git a/helm/gtkmathview-bonobo/src/control-data.c b/helm/DEVEL/gtkmathview-bonobo/src/control-data.c similarity index 100% rename from helm/gtkmathview-bonobo/src/control-data.c rename to helm/DEVEL/gtkmathview-bonobo/src/control-data.c diff --git a/helm/gtkmathview-bonobo/src/control-data.h b/helm/DEVEL/gtkmathview-bonobo/src/control-data.h similarity index 100% rename from helm/gtkmathview-bonobo/src/control-data.h rename to helm/DEVEL/gtkmathview-bonobo/src/control-data.h diff --git a/helm/gtkmathview-bonobo/src/control-factory.c b/helm/DEVEL/gtkmathview-bonobo/src/control-factory.c similarity index 100% rename from helm/gtkmathview-bonobo/src/control-factory.c rename to helm/DEVEL/gtkmathview-bonobo/src/control-factory.c diff --git a/helm/gtkmathview-bonobo/src/control-factory.h b/helm/DEVEL/gtkmathview-bonobo/src/control-factory.h similarity index 100% rename from helm/gtkmathview-bonobo/src/control-factory.h rename to helm/DEVEL/gtkmathview-bonobo/src/control-factory.h diff --git a/helm/gtkmathview-bonobo/src/handlers.c b/helm/DEVEL/gtkmathview-bonobo/src/handlers.c similarity index 100% rename from helm/gtkmathview-bonobo/src/handlers.c rename to helm/DEVEL/gtkmathview-bonobo/src/handlers.c diff --git a/helm/gtkmathview-bonobo/src/handlers.h b/helm/DEVEL/gtkmathview-bonobo/src/handlers.h similarity index 100% rename from helm/gtkmathview-bonobo/src/handlers.h rename to helm/DEVEL/gtkmathview-bonobo/src/handlers.h diff --git a/helm/gtkmathview-bonobo/src/persist-file.c b/helm/DEVEL/gtkmathview-bonobo/src/persist-file.c similarity index 100% rename from helm/gtkmathview-bonobo/src/persist-file.c rename to helm/DEVEL/gtkmathview-bonobo/src/persist-file.c diff --git a/helm/gtkmathview-bonobo/src/persist-file.h b/helm/DEVEL/gtkmathview-bonobo/src/persist-file.h similarity index 100% rename from helm/gtkmathview-bonobo/src/persist-file.h rename to helm/DEVEL/gtkmathview-bonobo/src/persist-file.h diff --git a/helm/gtkmathview-bonobo/src/persist-stream.c b/helm/DEVEL/gtkmathview-bonobo/src/persist-stream.c similarity index 100% rename from helm/gtkmathview-bonobo/src/persist-stream.c rename to helm/DEVEL/gtkmathview-bonobo/src/persist-stream.c diff --git a/helm/gtkmathview-bonobo/src/persist-stream.h b/helm/DEVEL/gtkmathview-bonobo/src/persist-stream.h similarity index 100% rename from helm/gtkmathview-bonobo/src/persist-stream.h rename to helm/DEVEL/gtkmathview-bonobo/src/persist-stream.h diff --git a/helm/gtkmathview-bonobo/src/view.c b/helm/DEVEL/gtkmathview-bonobo/src/view.c similarity index 100% rename from helm/gtkmathview-bonobo/src/view.c rename to helm/DEVEL/gtkmathview-bonobo/src/view.c diff --git a/helm/gtkmathview-bonobo/src/view.h b/helm/DEVEL/gtkmathview-bonobo/src/view.h similarity index 100% rename from helm/gtkmathview-bonobo/src/view.h rename to helm/DEVEL/gtkmathview-bonobo/src/view.h diff --git a/helm/gtkmathview-bonobo/test/.cvsignore b/helm/DEVEL/gtkmathview-bonobo/test/.cvsignore similarity index 100% rename from helm/gtkmathview-bonobo/test/.cvsignore rename to helm/DEVEL/gtkmathview-bonobo/test/.cvsignore diff --git a/helm/gtkmathview-bonobo/test/Makefile.am b/helm/DEVEL/gtkmathview-bonobo/test/Makefile.am similarity index 100% rename from helm/gtkmathview-bonobo/test/Makefile.am rename to helm/DEVEL/gtkmathview-bonobo/test/Makefile.am diff --git a/helm/gtkmathview-bonobo/test/embedding.html b/helm/DEVEL/gtkmathview-bonobo/test/embedding.html similarity index 100% rename from helm/gtkmathview-bonobo/test/embedding.html rename to helm/DEVEL/gtkmathview-bonobo/test/embedding.html diff --git a/helm/gtkmathview-bonobo/test/embedding.xml b/helm/DEVEL/gtkmathview-bonobo/test/embedding.xml similarity index 100% rename from helm/gtkmathview-bonobo/test/embedding.xml rename to helm/DEVEL/gtkmathview-bonobo/test/embedding.xml diff --git a/helm/gtkmathview-bonobo/test/main.c b/helm/DEVEL/gtkmathview-bonobo/test/main.c similarity index 100% rename from helm/gtkmathview-bonobo/test/main.c rename to helm/DEVEL/gtkmathview-bonobo/test/main.c diff --git a/helm/gtkmathview-bonobo/test/test.mml b/helm/DEVEL/gtkmathview-bonobo/test/test.mml similarity index 100% rename from helm/gtkmathview-bonobo/test/test.mml rename to helm/DEVEL/gtkmathview-bonobo/test/test.mml diff --git a/helm/gtkmathview-bonobo/test/testembedding.html b/helm/DEVEL/gtkmathview-bonobo/test/testembedding.html similarity index 100% rename from helm/gtkmathview-bonobo/test/testembedding.html rename to helm/DEVEL/gtkmathview-bonobo/test/testembedding.html diff --git a/helm/annotationHelper/.cvsignore b/helm/annotationHelper/.cvsignore deleted file mode 100644 index b79ea367a..000000000 --- a/helm/annotationHelper/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iox] *.o cicAnnotationHelper cicAnnotationHelper.opt diff --git a/helm/annotationHelper/.depend b/helm/annotationHelper/.depend deleted file mode 100644 index 699b8de3a..000000000 --- a/helm/annotationHelper/.depend +++ /dev/null @@ -1,4 +0,0 @@ -cicAnnotationHinter.cmo: cicAnnotationHinter.cmi -cicAnnotationHinter.cmx: cicAnnotationHinter.cmi -cicAnnotationHelper.cmo: cicAnnotationHinter.cmi -cicAnnotationHelper.cmx: cicAnnotationHinter.cmx diff --git a/helm/annotationHelper/Makefile b/helm/annotationHelper/Makefile deleted file mode 100644 index 272ac3eba..000000000 --- a/helm/annotationHelper/Makefile +++ /dev/null @@ -1,47 +0,0 @@ -BIN_DIR = /usr/local/bin -REQUIRES = lablgtkmathview helm-cic_annotations_cache -PREDICATES = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamldep - -LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) - -all: cicAnnotationHelper -opt: cicAnnotationHelper.opt - -DEPOBJS = cicAnnotationHinter.mli cicAnnotationHinter.ml cicAnnotationHelper.ml - -CICANNOTATIONHELPEROBJS = cicAnnotationHinter.cmo cicAnnotationHelper.cmo - -depend: - $(OCAMLDEP) $(DEPOBJS) > .depend - -cicAnnotationHelper: $(CICANNOTATIONHELPEROBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o cicAnnotationHelper $(CICANNOTATIONHELPEROBJS) - -cicAnnotationHelper.opt: $(CICANNOTATIONHELPEROBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o cicAnnotationHelper.opt $(CICANNOTATIONHELPEROBJS:.cmo=.cmx) - -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: $(LIBRARIES) - $(OCAMLC) -c $< -.mli.cmi: $(LIBRARIES) - $(OCAMLC) -c $< -.ml.cmx: $(LIBRARIES_OPT) - $(OCAMLOPT) -c $< - -clean: - rm -f *.cm[iox] *.o cicAnnotationHelper cicAnnotationHelper.opt - -install: - cp cicAnnotationHelper cicAnnotationHelper.opt $(BIN_DIR) - -uninstall: - rm -f $(BIN_DIR)/cicAnnotationHelper $(BIN_DIR)/cicAnnotationHelper.opt - -.PHONY: install uninstall clean - -include .depend diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml deleted file mode 100644 index 5ed1fa26d..000000000 --- a/helm/annotationHelper/cicAnnotationHelper.ml +++ /dev/null @@ -1,594 +0,0 @@ -(* Copyright (C) 2000, 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://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 03/04/2001 *) -(* *) -(* This is a simple gtk interface to the Coq-like pretty printer cicPp for *) -(* cic terms exported in xml. It uses directly the modules cicPp and *) -(* cicCcache and indirectly all the other modules (cicParser, cicParser2, *) -(* cicParser3, getter). *) -(* The syntax is "gtkInterface[.opt] filename1 ... filenamen" where *) -(* filenamei is the path-name of an xml file describing a cic term. *) -(* The terms are loaded in cache and then pretty-printed one at a time and *) -(* only once, when the user wants to look at it: if the user wants to look at *) -(* a term again, then the pretty-printed term is showed again, but not *) -(* recomputed *) -(* *) -(******************************************************************************) - -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) - -let annotated_obj = ref None;; (* reference to a triple option where *) - (* the first component is the current *) - (* annotated object, the second is the *) - (* map from ids to annotated targets and *) - (* the third is the map from ids to *) - (* annotations. *) -let current_id = ref None;; (* id of the element to annotate *) -let radio_some_status = ref false;; (* is the radio_some button selected? *) -let current_url = ref "";; - -(* GLOBAL CONSTANTS *) - -let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; - -(* MISC FUNCTIONS *) - -let pathname_of_annuri uristring = - Configuration.annotations_dir ^ - Str.replace_first (Str.regexp "^cic:") "" uristring -;; - -let make_dirs dirpath = - ignore (Unix.system ("mkdir -p " ^ dirpath)) -;; - -module UrlManipulator = - struct - exception No_param_dot_CICURI_or_param_dot_annotations_found_in of string;; - exception No_param_found_in of string * string;; - exception Bad_formed_url of string;; - - let uri_from_url url = - let module N = Neturl in - let founduri = ref None in - let foundann = ref None in - let rec find_uri = - function - [] -> raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) - | he::tl -> - match Str.split (Str.regexp "=") he with - ["param.CICURI";uri] -> - if !founduri <> None then - raise (Bad_formed_url url) - else - begin - founduri := Some uri ; - if !foundann = None then - find_uri tl - end - | ["param.annotations";ann] -> - if !foundann <> None then - raise (Bad_formed_url url) - else - begin - foundann := - Some - (match ann with - "yes" -> ".ann" - | "no" -> "" - | _ -> raise (Bad_formed_url url) - ) ; - if !founduri = None then - find_uri tl - end - | _ -> find_uri tl - in - find_uri - (Str.split (Str.regexp "&") - (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) ; - match !founduri,!foundann with - (Some uri),(Some ann) -> uri ^ ann - | _ , _ -> - raise (No_param_dot_CICURI_or_param_dot_annotations_found_in url) - ;; - - let extractParam param url = - let module N = Neturl in - let rec find_param = - function - [] -> raise (No_param_found_in (param,url)) - | he::tl -> - match Str.split (Str.regexp "=") he with - [name;value] when name = param -> value - | _ -> find_param tl - in - find_param - (Str.split (Str.regexp "&") - (N.url_query ~encoded:true (N.url_of_string N.ip_url_syntax url))) - ;; - - let set_annotations_to_yes query url = - let found =ref false in - let rec aux = - function - [] -> - if !found then "" - else raise (No_param_found_in ("param.annotations",url)) - | he::tl -> - match Str.split (Str.regexp "=") he with - ["param.annotations" as s ; ann] -> - found := true ; - let auxtl = aux tl in - s ^ "=yes" ^ - (if auxtl = "" then "" else "&" ^ auxtl) - | [name ; value] -> - let auxtl = aux tl in - name ^ "=" ^ value ^ - (if auxtl = "" then "" else "&" ^ auxtl) - | [name] -> - let auxtl = aux tl in - name ^ "=" ^ - (if auxtl = "" then "" else "&" ^ auxtl) - | _ -> raise (Bad_formed_url url) - in - aux (Str.split (Str.regexp "&") query) - ;; - - let annurl_of_url url = - let module N = Neturl in - let nurl = N.url_of_string N.ip_url_syntax url in - let query = N.url_query ~encoded:true nurl in - let newquery = set_annotations_to_yes query url in - N.string_of_url (N.modify_url ~encoded:true ~query:newquery nurl) - ;; -end - -let get_current_uri () = - UriManager.uri_of_string (UrlManipulator.uri_from_url !current_url) -;; - -(* CALLBACKS *) - -let get_annotated_obj () = - match !annotated_obj with - None -> - let annobj = - let (annobj,ids_to_annotations) = - match CicCache.get_annobj (get_current_uri ()) with - (annobj,None) -> annobj, Hashtbl.create 503 - | (annobj, Some ids_to_annotations) -> (annobj,ids_to_annotations) - in - let ids_to_targets = CicXPath.get_ids_to_targets annobj in - (annobj,ids_to_targets,ids_to_annotations) - in - annotated_obj := Some annobj ; - annobj - | Some annobj -> annobj -;; - -let update_output rendering_window url = - rendering_window#label#set_text (UrlManipulator.uri_from_url url) ; - rendering_window#output#load url -;; - -let choose_selection rendering_window (element : Gdome.element option) = - let module G = Gdome in - let rec aux element = - if element#hasAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref") - then - rendering_window#output#set_selection (Some element) - else - match element#get_parentNode with - None -> assert false - (*CSC: OCAML DIVERGES! - | Some p -> aux (new G.element_of_node p) - *) - | Some p -> aux (new Gdome.element_of_node p) - in - match element with - Some x -> aux x - | None -> rendering_window#output#set_selection None -;; - -let annotateb_pressed rendering_window annotation_window () = - let module G = Gdome in - match rendering_window#output#get_selection with - Some element -> - let xpath = - ((element : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then - rendering_window#label#set_text ("ERROR: No xref found!!!\n") - else - let annobj = get_annotated_obj () in - let (anno, ids_to_targets, ids_to_annotations) = annobj in - let annotation = (annotation_window#annotation : GEdit.text) in - let id = xpath in - current_id := Some id ; - let ann = CicXPath.get_annotation ids_to_annotations id in - CicAnnotationHinter.create_hints annotation_window ids_to_targets - xpath ; - annotation#delete_text 0 annotation#length ; - begin - match ann with - None -> - annotation#misc#set_sensitive false ; - annotation_window#radio_none#set_active true ; - radio_some_status := false - | Some ann' -> - annotation#insert ann' ; - annotation#misc#set_sensitive true ; - annotation_window#radio_some#set_active true ; - radio_some_status := true - end ; - GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; - annotation_window#show () ; - | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n") -;; - -let change_annotation ids_to_annotations id ann = - begin - try - Hashtbl.remove ids_to_annotations id - with - Not_found -> () - end ; - match ann with - None -> () - | Some ann' -> Hashtbl.add ids_to_annotations id ann' -;; - -(* called when the annotation is confirmed *) -let save_annotation (annotation : GEdit.text) = - let module S = Str in - let module U = UriManager in - let (annobj,ids_to_annotations) = - match !annotated_obj with - None -> assert false - | Some (annobj,_,ids_to_annotations) -> annobj,ids_to_annotations - in - change_annotation ids_to_annotations - (match !current_id with - Some id -> id - | None -> assert false - ) - (if !radio_some_status then - Some (annotation#get_chars 0 annotation#length) - else - None - ) ; - let uri = get_current_uri () in - let annxml = - CicAnnotation2Xml.pp_annotation annobj ids_to_annotations uri - in - make_dirs - (pathname_of_annuri (U.buri_of_uri uri)) ; - Xml.pp ~quiet:true annxml - (Some - (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ - ".xml" - ) - ) -;; - -(* STUFF TO BUILD THE GTK INTERFACE *) - -(* Stuff for the widget settings *) - -let export_to_postscript (output : GMathView.math_view) () = - output#export_to_postscript ~filename:"output.ps" (); -;; - -let activate_t1 (output : GMathView.math_view) - button_set_anti_aliasing button_set_kerning - button_set_transparency button_export_to_postscript button_t1 () -= - let is_set = button_t1#active in - output#set_font_manager_type - (if is_set then `font_manager_t1 else `font_manager_gtk) ; - if is_set then - begin - button_set_anti_aliasing#misc#set_sensitive true ; - button_set_kerning#misc#set_sensitive true ; - button_set_transparency#misc#set_sensitive true ; - button_export_to_postscript#misc#set_sensitive true ; - end - else - begin - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; - end -;; - -let set_anti_aliasing output button_set_anti_aliasing () = - output#set_anti_aliasing button_set_anti_aliasing#active -;; - -let set_kerning output button_set_kerning () = - output#set_kerning button_set_kerning#active -;; - -let set_transparency output button_set_transparency () = - output#set_transparency button_set_transparency#active -;; - -let changefont output font_size_spinb () = - output#set_font_size font_size_spinb#value_as_int -;; - -let set_log_verbosity output log_verbosity_spinb () = - output#set_log_verbosity log_verbosity_spinb#value_as_int -;; - -class settings_window (output : GMathView.math_view) - sw button_export_to_postscript selection_changed_callback -= - let settings_window = GWindow.window ~title:"GtkMathView settings" () in - let vbox = - GPack.vbox ~packing:settings_window#add () in - let table = - GPack.table - ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let button_t1 = - GButton.toggle_button ~label:"activate t1 fonts" - ~packing:(table#attach ~left:0 ~top:0) () in - let button_set_anti_aliasing = - GButton.toggle_button ~label:"set_anti_aliasing" - ~packing:(table#attach ~left:0 ~top:1) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:1 ~top:1) () in - let button_set_transparency = - GButton.toggle_button ~label:"set_transparency" - ~packing:(table#attach ~left:2 ~top:1) () in - let table = - GPack.table - ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let font_size_label = - GMisc.label ~text:"font size:" - ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in - let font_size_spinb = - let sadj = - GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in - let log_verbosity_label = - GMisc.label ~text:"log verbosity:" - ~packing:(table#attach ~left:0 ~top:1) () in - let log_verbosity_spinb = - let sadj = - GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in -object(self) - method show = settings_window#show - initializer - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - (* Signals connection *) - ignore(button_t1#connect#clicked - ~callback:(activate_t1 output button_set_anti_aliasing button_set_kerning - button_set_transparency button_export_to_postscript button_t1)) ; - ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; - ignore(button_set_anti_aliasing#connect#toggled - (set_anti_aliasing output button_set_anti_aliasing)); - ignore(button_set_kerning#connect#toggled - (set_kerning output button_set_kerning)) ; - ignore(button_set_transparency#connect#toggled - (set_transparency output button_set_transparency)) ; - ignore(log_verbosity_spinb#connect#changed - (set_log_verbosity output log_verbosity_spinb)) ; - ignore(closeb#connect#clicked ~callback:settings_window#misc#hide) -end;; - -(* Main windows *) - -class annotation_window output label = - let window_to_annotate = - GWindow.window ~title:"Annotating environment" ~border_width:2 () in - let hbox1 = - GPack.hbox ~packing:window_to_annotate#add () in - let vbox1 = - GPack.vbox ~packing:(hbox1#pack ~padding:5) () in - let hbox2 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let radio_some = GButton.radio_button ~label:"Annotation below" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let radio_none = GButton.radio_button ~label:"No annotation" - ~group:radio_some#group - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) - ~active:true () in - let annotation = GEdit.text ~editable:true ~width:400 ~height:180 - ~packing:(vbox1#pack ~padding:5) () in - let table = - GPack.table ~rows:3 ~columns:3 ~packing:(vbox1#pack ~padding:5) () in - let annotation_hints = - Array.init 9 - (function i -> - GButton.button ~label:("Hint " ^ string_of_int i) - ~packing:(table#attach ~left:(i mod 3) ~top:(i / 3)) () - ) in - let vbox2 = - GPack.vbox ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let confirmb = - GButton.button ~label:"O.K." - ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in - let abortb = - GButton.button ~label:"Abort" - ~packing:(vbox2#pack ~expand:false ~fill:false ~padding:5) () in -object (self) - method window_to_annotate = window_to_annotate - method annotation = annotation - method radio_some = radio_some - method radio_none = radio_none - method annotation_hints = annotation_hints - method output = (output : GMathView.math_view) - method show () = window_to_annotate#show () - initializer - (* signal handlers here *) - ignore (window_to_annotate#event#connect#delete - (fun _ -> - window_to_annotate#misc#hide () ; - GMain.Grab.remove (window_to_annotate#coerce) ; - true - )) ; - ignore (confirmb#connect#clicked - ~callback:(fun () -> - window_to_annotate#misc#hide () ; - save_annotation annotation ; - GMain.Grab.remove (window_to_annotate#coerce) ; - let new_current_uri = UriManager.annuri_of_uri (get_current_uri ()) in - Getter.register new_current_uri - (Configuration.annotations_url ^ - Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri new_current_uri) ^ ".xml" - ) ; - let new_current_url = UrlManipulator.annurl_of_url !current_url in - current_url := new_current_url ; - label#set_text (UriManager.string_of_uri new_current_uri) ; - output#load new_current_url - )) ; - ignore (abortb#connect#clicked - ~callback:(fun () -> - window_to_annotate#misc#hide () ; - GMain.Grab.remove (window_to_annotate#coerce) - )); - ignore (radio_some#connect#clicked - ~callback:(fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ; - ignore (radio_none #connect#clicked - ~callback:(fun () -> - annotation#misc#set_sensitive false; - radio_some_status := false) - ) -end;; - -class rendering_window annotation_window output (label : GMisc.label) = - let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in - let vbox = - GPack.vbox ~packing:window#add () in - let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in - let scrolled_window0 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let _ = scrolled_window0#add output#coerce in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let annotateb = - GButton.button ~label:"Annotate" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let settingsb = - GButton.button ~label:"Settings" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let button_export_to_postscript = - GButton.button ~label:"export_to_postscript" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in -object(self) - method label = label - method output = (output : GMathView.math_view) - method show () = window#show () - initializer - button_export_to_postscript#misc#set_sensitive false ; - - (* signal handlers here *) - ignore(output#connect#selection_changed (choose_selection self)) ; - ignore(closeb#connect#clicked ~callback:(fun _ -> GMain.Main.quit ())) ; - ignore(annotateb#connect#clicked - ~callback:(annotateb_pressed self annotation_window)) ; - let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (choose_selection self) in - ignore(settingsb#connect#clicked ~callback:settings_window#show) ; - ignore(button_export_to_postscript#connect#clicked ~callback:(export_to_postscript output)) ; - ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) -end;; - -(* MAIN *) - -let initialize_everything tmpfile url = - let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:380 () - and label = GMisc.label ~text:"???" () in - let annotation_window = new annotation_window output label in - let rendering_window = - new rendering_window annotation_window output label - in - rendering_window#show () ; - rendering_window#label#set_text (UrlManipulator.uri_from_url url) ; - rendering_window#output#load tmpfile ; - GMain.Main.main () -;; - -let _ = - let filename = ref "" in - let usage_msg = - "\nusage: annotationHelper[.opt] file url\n\n List of options:" - in - Arg.parse [] - (fun x -> - if x = "" then raise (Arg.Bad "Empty filename or URL not allowed") ; - if !filename = "" then - filename := x - else if !current_url = "" then - current_url := x - else - begin - prerr_string "More than two arguments provided\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end - ) usage_msg ; - Getter.getter_url := - Netencoding.Url.decode - (UrlManipulator.extractParam "param.getterURL" !current_url) ; - initialize_everything !filename !current_url -;; diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml deleted file mode 100644 index 7cf3cddbb..000000000 --- a/helm/annotationHelper/cicAnnotationHinter.ml +++ /dev/null @@ -1,393 +0,0 @@ -(* Copyright (C) 2000, 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://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 14/06/2000 *) -(* *) -(* *) -(******************************************************************************) - -let deactivate_hints_from annotation_window n = - let annotation_hints = annotation_window#annotation_hints in - for i = n to Array.length annotation_hints - 1 do - annotation_hints.(i)#misc#hide () - done -;; - -(* CSC: orripilante *) -(* the list of the signal ids *) -let sig_ids = ref ([] : GtkSignal.id list);; - -let disconnect_hint annotation_window buttonno = - match !sig_ids with - id::ids -> - annotation_window#annotation_hints.(buttonno)#misc#disconnect id ; - sig_ids := ids - | _ -> assert false -;; - -(* link_hint annotation_window n label hint *) -(* set the label of the nth hint button of annotation_window to label *) -(* and the correspondent hint to hint *) -let link_hint annotation_window buttonno label hint = - let button = annotation_window#annotation_hints.(buttonno) in - sig_ids := - (button#connect#clicked - ~callback:(fun () -> (annotation_window#annotation : GEdit.text)#insert hint) - ) :: !sig_ids ; - button#misc#show () ; - match button#children with - [labelw] -> (GMisc.label_cast labelw)#set_text label - | _ -> assert false -;; - -exception TooManyHints;; - -let link_hints annotation_window a = - if Array.length a > Array.length annotation_window#annotation_hints then - raise TooManyHints ; - for i = List.length !sig_ids - 1 downto 0 do - disconnect_hint annotation_window i - done ; - Array.iteri - (fun i (label,hint) -> link_hint annotation_window i label hint) a ; - deactivate_hints_from annotation_window (Array.length a) -;; - -let list_mapi f = - let rec aux n = - function - [] -> [] - | he::tl -> (f n he)::(aux (n + 1) tl) - in - aux 0 -;; - -let get_id annterm = - let module C = Cic in - match annterm with - C.ARel (id,_,_) - | C.AVar (id,_) - | C.AMeta (id,_,_) - | C.ASort (id,_) - | C.AImplicit id - | C.ACast (id,_,_) - | C.AProd (id,_,_,_) - | C.ALambda (id,_,_,_) - | C.ALetIn (id,_,_,_) - | C.AAppl (id,_) - | C.AConst (id,_,_) - | C.AMutInd (id,_,_,_) - | C.AMutConstruct (id,_,_,_,_) - | C.AMutCase (id,_,_,_,_,_,_) - | C.AFix (id,_,_) - | C.ACoFix (id,_,_) -> id -;; - -let create_hint_from_term annotation_window annterm = - let module C = Cic in - match annterm with - C.ARel (id,_,_) -> - link_hints annotation_window - [| "Binder", "" |] - | C.AVar (id,_) -> - link_hints annotation_window - [| "relURI???", "" |] - | C.AMeta (id,_,subst) -> - let res = - Array.append - [| "Number", "" |] - (Array.mapi - (fun i s -> - match s with - None -> - "Argument " ^ string_of_int i, "_" - | Some t -> - "Argument " ^ string_of_int i, "" - ) (Array.of_list subst) - ) - in - link_hints annotation_window res - | C.ASort (id,_) -> - link_hints annotation_window - [| "Value", "" |] - | C.AImplicit id -> - link_hints annotation_window [| |] - | C.ACast (id,bo,ty) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Body", "" ; - "Type", "" - |] - | C.AProd (id,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Body", "" ; - "Type", "" - |] - | C.ALambda (id,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Body", "" ; - "Type", "" - |] - | C.ALetIn (id,_,ty,bo) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Binder", - "" ; - "Term", "" ; - "Target", "" - |] - | C.AAppl (id,args) -> - let argsid = - Array.mapi - (fun i te -> "Argument " ^ string_of_int i, "") - (Array.of_list args) - in - link_hints annotation_window argsid - | C.AConst (id,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutInd (id,_,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutConstruct (id,_,_,_,_) -> - link_hints annotation_window - [| "Uri???", "" |] - | C.AMutCase (id,_,_,_,outty,te,pl) -> - let outtyid = get_id outty - and teid = get_id te - and plid = - Array.mapi - (fun i te -> "Pattern " ^ string_of_int i, "") - (Array.of_list pl) - in - link_hints annotation_window - (Array.append - [| "Uri???", "" ; - "Case Type", "" ; - "Term", "" ; - |] - plid) - | C.AFix (id,_,funl) -> - let funtylid = - Array.mapi - (fun i (_,_,ty,_) -> - "Type " ^ string_of_int i, "") - (Array.of_list funl) - and funbolid = - Array.mapi - (fun i (_,_,_,bo) -> - "Body " ^ string_of_int i, "") - (Array.of_list funl) - and funnamel = - Array.mapi - (fun i (_,_,_,_) -> - "Name " ^ string_of_int i, "") - (Array.of_list funl) - and funrecindexl = - Array.mapi - (fun i (_,_,_,_) -> - "Recursive Index??? " ^ string_of_int i, "") - (Array.of_list funl) - in - link_hints annotation_window - (Array.concat - [ funtylid ; - funbolid ; - funnamel ; - funrecindexl ; - [| "NoFun???", "" |] - ] - ) - | C.ACoFix (id,_,funl) -> - let funtylid = - Array.mapi - (fun i (_,ty,_) -> - "Type " ^ string_of_int i, "") - (Array.of_list funl) - and funbolid = - Array.mapi - (fun i (_,_,bo) -> - "Body " ^ string_of_int i, "") - (Array.of_list funl) - and funnamel = - Array.mapi - (fun i (_,_,_) -> - "Name " ^ string_of_int i, "") - (Array.of_list funl) - in - link_hints annotation_window - (Array.concat - [ funtylid ; - funbolid ; - funnamel ; - [| "NoFun???", "" |] - ] - ) -;; - -(*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *) -let create_hint_from_obj annotation_window annobj = - let module C = Cic in - match annobj with - C.ADefinition (id,_,bo,ty,_) -> - let boid = get_id bo - and tyid = get_id ty in - link_hints annotation_window - [| "Name", "" ; - "Ingredients", "" ; - "Body", "" ; - "Type", "" - |] - | C.AAxiom (id,_,ty,_) -> - let tyid = get_id ty in - link_hints annotation_window - [| "Name", "" ; - "Ingredients", "" ; - "Type", "" - |] - | C.AVariable (id,_,bo,ty) -> - let tyid = get_id ty in - link_hints annotation_window - (match bo with - None -> - [| "Name", "" ; - "Type", "" - |] - | Some bo -> - let boid = get_id bo in - [| "Name", "" ; - "Body", "" ; - "Type", "" - |] - ) - | C.ACurrentProof (id,_,conjs,bo,ty) -> - let boid = get_id bo - and tyid = get_id ty - and conjsid = List.map (fun (id,_,_,_) -> id) conjs in - link_hints annotation_window -(*CSC: never tested since the introduction of the new Metas *) - (Array.append - [| "Name", "" ; - "Ingredients", "" ; - "Body", "" ; - "Type", "" - |] - (Array.mapi - (fun i id -> - "Conjecture " ^ string_of_int i, "" - ) (Array.of_list conjsid) - ) - ) - | C.AInductiveDefinition (id,itl,_,_) -> - let itlids = - List.map - (fun (_,_,arity,cons) -> - get_id arity, - List.map (fun (_,ty,_) -> get_id ty) cons - ) itl - in - link_hints annotation_window - (Array.concat - [ - [| "Ingredients","" |]; - (Array.mapi - (fun i _ -> - "Type Name " ^ string_of_int i, - "" - ) (Array.of_list itlids) - ) ; - (Array.mapi - (fun i (id,_) -> - "Type " ^ string_of_int i, "" - ) (Array.of_list itlids) - ) ; - (Array.concat - (list_mapi - (fun i (_,consid) -> - (Array.mapi - (fun j _ -> - "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j, - "" - ) (Array.of_list consid) - ) ; - ) itlids - ) - ) ; - (Array.concat - (list_mapi - (fun i (_,consid) -> - (Array.mapi - (fun j id -> - "Constructor " ^ string_of_int i ^ " " ^ string_of_int j, - "" - ) (Array.of_list consid) - ) ; - ) itlids - ) - ) - ] - ) -;; - -exception IdUnknown of string;; - -let create_hints annotation_window ids_to_targets xpath = - try - match Hashtbl.find ids_to_targets xpath with - Cic.Object annobj -> create_hint_from_obj annotation_window annobj - | Cic.Term annterm -> create_hint_from_term annotation_window annterm -(*CSC: never tested since the introduction of the new Metas *) - | Cic.Hypothesis _ - | Cic.Conjecture _ -> assert false - with - Not_found -> raise (IdUnknown xpath) -;; diff --git a/helm/annotationHelper/cicAnnotationHinter.mli b/helm/annotationHelper/cicAnnotationHinter.mli deleted file mode 100644 index 8cfc04c22..000000000 --- a/helm/annotationHelper/cicAnnotationHinter.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* Copyright (C) 2000, 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://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* *) -(******************************************************************************) - -val create_hints : - < annotation : GEdit.text; - annotation_hints : < children : < as_widget : 'a Gtk.obj; .. > list; - connect : < clicked : callback:(unit -> unit) -> GtkSignal.id; - .. >; - misc : < disconnect : GtkSignal.id -> 'b; - hide : unit -> 'c; show : unit -> 'd; .. >; - .. > - array; - .. > -> - (Cic.id, Cic.anntarget) Hashtbl.t -> string -> unit diff --git a/helm/cgi/mkcontrol.pl b/helm/cgi/mkcontrol.pl deleted file mode 100755 index e314aa778..000000000 --- a/helm/cgi/mkcontrol.pl +++ /dev/null @@ -1,109 +0,0 @@ -#!/usr/bin/perl - -# First of all, let's load HELM configuration -use Env; -my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; -# this should be the only fixed constant -my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; -if (defined ($HELM_LIB_DIR)) { - $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; -} else { - $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; -} - -# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm -require $HELM_LIB_PATH; - -use CGI; - -$cgi = new CGI($ENV{"REQUEST_URL"}); -$mode = $cgi->param('mode'); -$cicuri = $cgi->param('cicuri'); -$theoryuri = $cgi->param('theoryuri'); -$topurl = $cgi->param('topurl'); -$processorURL = $cgi->param('processorURL'); -$getterURL = $cgi->param('getterURL'); -($mode1,$mode2,$mode3,$mode4,$mode5) = split(/,/, $mode); -$natural = "checked" if ($mode4 eq "yes"); -$annotations = "checked" if ($mode5 eq "yes"); -if ($mode1 eq "raw") { - $format_raw = "selected"; -} else { - $format_processed = "selected"; -} - -print < - - -Control panel - - - -
- - - - - - - - - - - -
- Format: - - - - - Reload
- (do it also before attempting to take a link to the current page) - -
-  Natural Language -  Annotations - - Configuration panel -
-
- - -EOT diff --git a/helm/cgi/mkheader.pl b/helm/cgi/mkheader.pl deleted file mode 100755 index b3db1cfa3..000000000 --- a/helm/cgi/mkheader.pl +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/perl - -# First of all, let's load HELM configuration -use Env; -my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; -# this should be the only fixed constant -my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; -if (defined ($HELM_LIB_DIR)) { - $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; -} else { - $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; -} - -# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm -require $HELM_LIB_PATH; - -use CGI; - -$cgi = new CGI($ENV{"REQUEST_URL"}); -$uri = $cgi->param('uri'); - -print < - - -Control panel - - - - - - - -
- Index of $uri -
-
- - -EOT diff --git a/helm/cgi/mkindex.pl b/helm/cgi/mkindex.pl deleted file mode 100755 index 955d6d8b0..000000000 --- a/helm/cgi/mkindex.pl +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/perl - -# First of all, let's load HELM configuration -use Env; -my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; -# this should be the only fixed constant -my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; -if (defined ($HELM_LIB_DIR)) { - $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; -} else { - $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; -} - -# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm -require $HELM_LIB_PATH; - -#use URI::Escape; -use CGI; - -$cgi = new CGI($ENV{"REQUEST_URL"}); - -$mode = $cgi->param('mode'); -$cicuri = $cgi->param('cicuri'); -$theoryuri = $cgi->param('theoryuri'); -$processorURL = $cgi->param('processorURL'); -$getterURL = $cgi->param('getterURL'); -$topurl = $cgi->url(); - -print < - - - Index of $cicuri and $theoryuri - - - - - - - - - - - - - - - -EOT diff --git a/helm/cgi/mkindexcic.pl b/helm/cgi/mkindexcic.pl deleted file mode 100755 index a31f5ecfb..000000000 --- a/helm/cgi/mkindexcic.pl +++ /dev/null @@ -1,113 +0,0 @@ -#!/usr/bin/perl - -# First of all, let's load HELM configuration -use Env; -my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; -# this should be the only fixed constant -my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; -if (defined ($HELM_LIB_DIR)) { - $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; -} else { - $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; -} - -# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm -require $HELM_LIB_PATH; - -use URI::Escape; -use LWP::UserAgent; -use CGI; - -my $cgi = new CGI($ENV{"REQUEST_URL"}); -$uri = $cgi->param('cicuri'); -$getterURL = $cgi->param('getterURL'); -$uri =~ s/(.*)\/$/$1/; # Remove a final slash if present -$uri .= "/"; # Put a final slash -$myurl = $cgi->url(); - -$cont = ""; # modified by side-effect by &callback -my $ua = LWP::UserAgent->new; -my $request = HTTP::Request->new(GET => $getterURL."ls?format=txt&baseuri=".$uri); -my $response = $ua->request($request, \&callback); - -@filenames = split(/\n/, $cont); - -my $uridotdot = $uri; -$uridotdot =~ s/(.*)\/.+/$1/; -if ($uri ne "cic:/") { - # Let's print the link to the parent directory - $output = < -[BACK] -Parent Directory - -EOT -} - -foreach $i (@filenames) { - my ($type,$name,$flags) = split(/, /, $i); - my ($flagscic, $flagstypes) = split(/,/, $flags); - $flagscic =~ s/^<(.*)/$1/; - $flagstypes =~ s/(.*)>$/$1/; - if ($type eq "dir") { - $output .= < -[DIR] -$name - - -EOT - } elsif ($type eq "object") { - if ($name =~ /\.(con|var|ind)$/) { - # cic file - $output .= < -[DIR] -$name - -EOT - } else { - $output .= < -[DIR] -$name - -EOT - } - } else { - $output .= < -[DIR] -$name - -EOT - } -} - -print < - - -Index of $uri - - - - -$output -
-
- - -EOT - -#================================ - -sub callback -{ - my ($data) = @_; - $cont .= $data; -} diff --git a/helm/cgi/mkindextheory.pl b/helm/cgi/mkindextheory.pl deleted file mode 100755 index 424f688ff..000000000 --- a/helm/cgi/mkindextheory.pl +++ /dev/null @@ -1,112 +0,0 @@ -#!/usr/bin/perl - -# First of all, let's load HELM configuration -use Env; -my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; -# this should be the only fixed constant -my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; -if (defined ($HELM_LIB_DIR)) { - $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; -} else { - $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; -} - -# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm -require $HELM_LIB_PATH; - -use URI::Escape; -use LWP::UserAgent; -use CGI; - -my $cgi = new CGI($ENV{"REQUEST_URL"}); -$uri = $cgi->param('theoryuri'); -$getterURL = $cgi->param('getterURL'); -$uri =~ s/(.*)\/$/$1/; # Remove a final slash if present -$uri .= "/"; # Put a final slash -$myurl = $cgi->url(); - -$cont = ""; # modified by side-effect by &callback -my $ua = LWP::UserAgent->new; -my $request = HTTP::Request->new(GET => $getterURL."ls?format=txt&baseuri=".$uri); -my $response = $ua->request($request, \&callback); - -@filenames = split(/\n/, $cont); - -my $uridotdot = $uri; -$uridotdot =~ s/(.*)\/.+/$1/; -if ($uri ne "theory:/") { - # Let's print the link to the parent directory - $output = < -[BACK] -Parent Directory - -EOT -} - -foreach $i (@filenames) { - my ($type,$name,$flags) = split(/, /, $i); - my ($flagscic, $flagstypes) = split(/,/, $flags); - $flagscic =~ s/^<(.*)/$1/; - $flagstypes =~ s/(.*)>$/$1/; - if ($type eq "dir") { - $output .= < -[DIR] -$name - -EOT - } elsif ($type eq "object") { - if ($name =~ /\.theory$/) { - # theory file - $output .= < -[DIR] -$name - -EOT - } else { - $output .= < -[DIR] -$name - -EOT - } - } else { - $output .= < -[DIR] -$name - -EOT - } -} - -print < - - -Index of $uri - - - - -$output -
-
- - -EOT - -#================================ - -sub callback -{ - my ($data) = @_; - $cont .= $data; -} diff --git a/helm/configuration/.cvsignore b/helm/configuration/.cvsignore deleted file mode 100644 index d8a7ecb4a..000000000 --- a/helm/configuration/.cvsignore +++ /dev/null @@ -1,3 +0,0 @@ -Makefile configure config.log config.cache config.status -helm-config -helm_configuration.spec diff --git a/helm/configuration/AUTHORS b/helm/configuration/AUTHORS deleted file mode 100644 index 0ceb16fd5..000000000 --- a/helm/configuration/AUTHORS +++ /dev/null @@ -1,4 +0,0 @@ -Andrea Asperti -Luca Padovani -Claudio Sacerdoti Coen -Irene Schena diff --git a/helm/configuration/COPYING b/helm/configuration/COPYING deleted file mode 100644 index d60c31a97..000000000 --- a/helm/configuration/COPYING +++ /dev/null @@ -1,340 +0,0 @@ - GNU GENERAL PUBLIC LICENSE - Version 2, June 1991 - - Copyright (C) 1989, 1991 Free Software Foundation, Inc. - 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The licenses for most software are designed to take away your -freedom to share and change it. By contrast, the GNU General Public -License is intended to guarantee your freedom to share and change free -software--to make sure the software is free for all its users. This -General Public License applies to most of the Free Software -Foundation's software and to any other program whose authors commit to -using it. (Some other Free Software Foundation software is covered by -the GNU Library General Public License instead.) You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -this service if you wish), that you receive source code or can get it -if you want it, that you can change the software or use pieces of it -in new free programs; and that you know you can do these things. - - To protect your rights, we need to make restrictions that forbid -anyone to deny you these rights or to ask you to surrender the rights. -These restrictions translate to certain responsibilities for you if you -distribute copies of the software, or if you modify it. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must give the recipients all the rights that -you have. You must make sure that they, too, receive or can get the -source code. And you must show them these terms so they know their -rights. - - We protect your rights with two steps: (1) copyright the software, and -(2) offer you this license which gives you legal permission to copy, -distribute and/or modify the software. - - Also, for each author's protection and ours, we want to make certain -that everyone understands that there is no warranty for this free -software. If the software is modified by someone else and passed on, we -want its recipients to know that what they have is not the original, so -that any problems introduced by others will not reflect on the original -authors' reputations. - - Finally, any free program is threatened constantly by software -patents. We wish to avoid the danger that redistributors of a free -program will individually obtain patent licenses, in effect making the -program proprietary. To prevent this, we have made it clear that any -patent must be licensed for everyone's free use or not licensed at all. - - The precise terms and conditions for copying, distribution and -modification follow. - - GNU GENERAL PUBLIC LICENSE - TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION - - 0. This License applies to any program or other work which contains -a notice placed by the copyright holder saying it may be distributed -under the terms of this General Public License. The "Program", below, -refers to any such program or work, and a "work based on the Program" -means either the Program or any derivative work under copyright law: -that is to say, a work containing the Program or a portion of it, -either verbatim or with modifications and/or translated into another -language. (Hereinafter, translation is included without limitation in -the term "modification".) Each licensee is addressed as "you". - -Activities other than copying, distribution and modification are not -covered by this License; they are outside its scope. The act of -running the Program is not restricted, and the output from the Program -is covered only if its contents constitute a work based on the -Program (independent of having been made by running the Program). -Whether that is true depends on what the Program does. - - 1. You may copy and distribute verbatim copies of the Program's -source code as you receive it, in any medium, provided that you -conspicuously and appropriately publish on each copy an appropriate -copyright notice and disclaimer of warranty; keep intact all the -notices that refer to this License and to the absence of any warranty; -and give any other recipients of the Program a copy of this License -along with the Program. - -You may charge a fee for the physical act of transferring a copy, and -you may at your option offer warranty protection in exchange for a fee. - - 2. You may modify your copy or copies of the Program or any portion -of it, thus forming a work based on the Program, and copy and -distribute such modifications or work under the terms of Section 1 -above, provided that you also meet all of these conditions: - - a) You must cause the modified files to carry prominent notices - stating that you changed the files and the date of any change. - - b) You must cause any work that you distribute or publish, that in - whole or in part contains or is derived from the Program or any - part thereof, to be licensed as a whole at no charge to all third - parties under the terms of this License. - - c) If the modified program normally reads commands interactively - when run, you must cause it, when started running for such - interactive use in the most ordinary way, to print or display an - announcement including an appropriate copyright notice and a - notice that there is no warranty (or else, saying that you provide - a warranty) and that users may redistribute the program under - these conditions, and telling the user how to view a copy of this - License. (Exception: if the Program itself is interactive but - does not normally print such an announcement, your work based on - the Program is not required to print an announcement.) - -These requirements apply to the modified work as a whole. If -identifiable sections of that work are not derived from the Program, -and can be reasonably considered independent and separate works in -themselves, then this License, and its terms, do not apply to those -sections when you distribute them as separate works. But when you -distribute the same sections as part of a whole which is a work based -on the Program, the distribution of the whole must be on the terms of -this License, whose permissions for other licensees extend to the -entire whole, and thus to each and every part regardless of who wrote it. - -Thus, it is not the intent of this section to claim rights or contest -your rights to work written entirely by you; rather, the intent is to -exercise the right to control the distribution of derivative or -collective works based on the Program. - -In addition, mere aggregation of another work not based on the Program -with the Program (or with a work based on the Program) on a volume of -a storage or distribution medium does not bring the other work under -the scope of this License. - - 3. You may copy and distribute the Program (or a work based on it, -under Section 2) in object code or executable form under the terms of -Sections 1 and 2 above provided that you also do one of the following: - - a) Accompany it with the complete corresponding machine-readable - source code, which must be distributed under the terms of Sections - 1 and 2 above on a medium customarily used for software interchange; or, - - b) Accompany it with a written offer, valid for at least three - years, to give any third party, for a charge no more than your - cost of physically performing source distribution, a complete - machine-readable copy of the corresponding source code, to be - distributed under the terms of Sections 1 and 2 above on a medium - customarily used for software interchange; or, - - c) Accompany it with the information you received as to the offer - to distribute corresponding source code. (This alternative is - allowed only for noncommercial distribution and only if you - received the program in object code or executable form with such - an offer, in accord with Subsection b above.) - -The source code for a work means the preferred form of the work for -making modifications to it. For an executable work, complete source -code means all the source code for all modules it contains, plus any -associated interface definition files, plus the scripts used to -control compilation and installation of the executable. However, as a -special exception, the source code distributed need not include -anything that is normally distributed (in either source or binary -form) with the major components (compiler, kernel, and so on) of the -operating system on which the executable runs, unless that component -itself accompanies the executable. - -If distribution of executable or object code is made by offering -access to copy from a designated place, then offering equivalent -access to copy the source code from the same place counts as -distribution of the source code, even though third parties are not -compelled to copy the source along with the object code. - - 4. You may not copy, modify, sublicense, or distribute the Program -except as expressly provided under this License. Any attempt -otherwise to copy, modify, sublicense or distribute the Program is -void, and will automatically terminate your rights under this License. -However, parties who have received copies, or rights, from you under -this License will not have their licenses terminated so long as such -parties remain in full compliance. - - 5. You are not required to accept this License, since you have not -signed it. However, nothing else grants you permission to modify or -distribute the Program or its derivative works. These actions are -prohibited by law if you do not accept this License. Therefore, by -modifying or distributing the Program (or any work based on the -Program), you indicate your acceptance of this License to do so, and -all its terms and conditions for copying, distributing or modifying -the Program or works based on it. - - 6. Each time you redistribute the Program (or any work based on the -Program), the recipient automatically receives a license from the -original licensor to copy, distribute or modify the Program subject to -these terms and conditions. You may not impose any further -restrictions on the recipients' exercise of the rights granted herein. -You are not responsible for enforcing compliance by third parties to -this License. - - 7. If, as a consequence of a court judgment or allegation of patent -infringement or for any other reason (not limited to patent issues), -conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot -distribute so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you -may not distribute the Program at all. For example, if a patent -license would not permit royalty-free redistribution of the Program by -all those who receive copies directly or indirectly through you, then -the only way you could satisfy both it and this License would be to -refrain entirely from distribution of the Program. - -If any portion of this section is held invalid or unenforceable under -any particular circumstance, the balance of the section is intended to -apply and the section as a whole is intended to apply in other -circumstances. - -It is not the purpose of this section to induce you to infringe any -patents or other property right claims or to contest validity of any -such claims; this section has the sole purpose of protecting the -integrity of the free software distribution system, which is -implemented by public license practices. Many people have made -generous contributions to the wide range of software distributed -through that system in reliance on consistent application of that -system; it is up to the author/donor to decide if he or she is willing -to distribute software through any other system and a licensee cannot -impose that choice. - -This section is intended to make thoroughly clear what is believed to -be a consequence of the rest of this License. - - 8. If the distribution and/or use of the Program is restricted in -certain countries either by patents or by copyrighted interfaces, the -original copyright holder who places the Program under this License -may add an explicit geographical distribution limitation excluding -those countries, so that distribution is permitted only in or among -countries not thus excluded. In such case, this License incorporates -the limitation as if written in the body of this License. - - 9. The Free Software Foundation may publish revised and/or new versions -of the General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - -Each version is given a distinguishing version number. If the Program -specifies a version number of this License which applies to it and "any -later version", you have the option of following the terms and conditions -either of that version or of any later version published by the Free -Software Foundation. If the Program does not specify a version number of -this License, you may choose any version ever published by the Free Software -Foundation. - - 10. If you wish to incorporate parts of the Program into other free -programs whose distribution conditions are different, write to the author -to ask for permission. For software which is copyrighted by the Free -Software Foundation, write to the Free Software Foundation; we sometimes -make exceptions for this. Our decision will be guided by the two goals -of preserving the free status of all derivatives of our free software and -of promoting the sharing and reuse of software generally. - - NO WARRANTY - - 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY -FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN -OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES -PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED -OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF -MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS -TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE -PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, -REPAIR OR CORRECTION. - - 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING -WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR -REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, -INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING -OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED -TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY -YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER -PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE -POSSIBILITY OF SUCH DAMAGES. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -convey the exclusion of warranty; and each file should have at least -the "copyright" line and a pointer to where the full notice is found. - - - Copyright (C) - - This program 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. - - This program 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 this program; if not, write to the Free Software - Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - - -Also add information on how to contact you by electronic and paper mail. - -If the program is interactive, make it output a short notice like this -when it starts in an interactive mode: - - Gnomovision version 69, Copyright (C) year name of author - Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, the commands you use may -be called something other than `show w' and `show c'; they could even be -mouse-clicks or menu items--whatever suits your program. - -You should also get your employer (if you work as a programmer) or your -school, if any, to sign a "copyright disclaimer" for the program, if -necessary. Here is a sample; alter the names: - - Yoyodyne, Inc., hereby disclaims all copyright interest in the program - `Gnomovision' (which makes passes at compilers) written by James Hacker. - - , 1 April 1989 - Ty Coon, President of Vice - -This General Public License does not permit incorporating your program into -proprietary programs. If your program is a subroutine library, you may -consider it more useful to permit linking proprietary applications with the -library. If this is what you want to do, use the GNU Library General -Public License instead of this License. diff --git a/helm/configuration/ChangeLog b/helm/configuration/ChangeLog deleted file mode 100644 index 20c36b475..000000000 --- a/helm/configuration/ChangeLog +++ /dev/null @@ -1 +0,0 @@ -28/12/2000: First alpha release diff --git a/helm/configuration/Makefile.in b/helm/configuration/Makefile.in deleted file mode 100644 index 00c3893dc..000000000 --- a/helm/configuration/Makefile.in +++ /dev/null @@ -1,47 +0,0 @@ - -HELM_BIN_DIR=@HELM_BIN_DIR@ -HELM_LIB_DIR=@HELM_LIB_DIR@ -HELM_ETC_DIR=@HELM_ETC_DIR@ -HELM_SHARE_DIR=@HELM_SHARE_DIR@ -HELM_VAR_DIR=@HELM_VAR_DIR@ -HELM_DTD_DIR=@HELM_DTD_DIR@ -HELM_STYLE_DIR=@HELM_STYLE_DIR@ -HELM_LIBRARY_DIR=@HELM_LIBRARY_DIR@ - -all: - -install: - mkdir -p $(HELM_BIN_DIR) - cp helm-config $(HELM_BIN_DIR) - mkdir -p $(HELM_LIB_DIR) - mkdir -p $(HELM_ETC_DIR) - mkdir -p $(HELM_SHARE_DIR) - mkdir -p $(HELM_VAR_DIR) - chmod 777 $(HELM_VAR_DIR) - mkdir -p $(HELM_LIBRARY_DIR) - chmod 777 $(HELM_LIBRARY_DIR) - mkdir -p $(HELM_DTD_DIR) - mkdir -p $(HELM_STYLE_DIR) - cp lib/configuration.pl $(HELM_LIB_DIR) - cp etc/configuration.dtd etc/configuration.xml etc/helm-dictionary.xml \ - etc/helm-font-configuration.xml etc/helm-math-engine-configuration.xml\ - $(HELM_ETC_DIR) - cp library/servers.txt library/urls_of_uris.db $(HELM_VAR_DIR) - chmod 666 $(HELM_VAR_DIR)/servers.txt \ - $(HELM_VAR_DIR)/urls_of_uris.db - -clean: - -distclean: - rm -f Makefile configure config.log config.cache config.status \ - etc/configuration.xml etc/helm-math-engine-configuration.xml \ - lib/configuration.pl helm-config helm_configuration.spec - -dist: clean - rm -rf ../@PACKAGE@-@VERSION@ - mkdir ../@PACKAGE@-@VERSION@ - cp -r * ../@PACKAGE@-@VERSION@ - (cd .. ; tar cvfz @PACKAGE@-@VERSION@.tar.gz @PACKAGE@-@VERSION@ ; rm -rf @PACKAGE@-@VERSION@) - -.PHONY: all install distclean - diff --git a/helm/configuration/NEWS b/helm/configuration/NEWS deleted file mode 100644 index 20c36b475..000000000 --- a/helm/configuration/NEWS +++ /dev/null @@ -1 +0,0 @@ -28/12/2000: First alpha release diff --git a/helm/configuration/README b/helm/configuration/README deleted file mode 100644 index 9f6eb3534..000000000 --- a/helm/configuration/README +++ /dev/null @@ -1,8 +0,0 @@ -NOTE: This is the first alpha release of project HELM. - -HELM (Hypertextual Electronic Library of Mathematics) is a project aimed -at the creation of tools for the development and exploitation of a huge -distributed library of formal mathematical knowledge. This package holds -the configuration files shared by all this tools. - -For more information see http://www.cs.unibo.it/helm diff --git a/helm/configuration/config.cache.pkg b/helm/configuration/config.cache.pkg deleted file mode 100644 index 434e570a2..000000000 --- a/helm/configuration/config.cache.pkg +++ /dev/null @@ -1,15 +0,0 @@ -# This file is a shell script that caches the results of configure -# tests run on this system so they can be shared between configure -# scripts and configure runs. It is not useful on other systems. -# If it contains results you don't want to keep, you may remove or edit it. -# -# By default, configure uses ./config.cache as the cache file, -# creating it if it does not exist already. You can give configure -# the --cache-file=FILE option to use a different cache file; that is -# what configure does when it calls configure scripts in -# subdirectories, so they share the cache. -# Giving --cache-file=/dev/null disables caching, for debugging configure. -# config.status only pays attention to the cache file if you give it the -# --recheck option to rerun configure. -# -helm_cv_HELM_VAR_DIR=${helm_cv_HELM_VAR_DIR='/var/local/helm'} diff --git a/helm/configuration/configure.in b/helm/configuration/configure.in deleted file mode 100644 index 03c923e9d..000000000 --- a/helm/configuration/configure.in +++ /dev/null @@ -1,186 +0,0 @@ -AC_INIT(etc/configuration.xml.in) - -PACKAGE=helm_configuration - -HELM_MAJOR_VERSION=0 -HELM_MINOR_VERSION=0 -HELM_MICRO_VERSION=2 -HELM_VERSION=$HELM_MAJOR_VERSION.$HELM_MINOR_VERSION.$HELM_MICRO_VERSION -VERSION=$HELM_VERSION - -DEFAULT_HELM_VAR_DIR=/var/local/helm -DEFAULT_HELM_TMP_DIR=/tmp - -AC_ARG_ENABLE( - defaults, - [ --enable-defaults[=ARG] if yes then use defaults (don't ask user) [default=auto]], - USE_DEFAULTS=$enableval, - USE_DEFAULTS=auto -) - -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 - -dnl General -HELM_BIN_DIR=$RESOLVED_EXEC_PREFIX/bin -HELM_LIB_DIR=$RESOLVED_EXEC_PREFIX/lib/helm -HELM_ETC_DIR=$RESOLVED_PREFIX/etc/helm -HELM_SHARE_DIR=$RESOLVED_PREFIX/share/helm - -dnl Checking for the variable directory -if test $USE_DEFAULTS != yes; then - echo - echo "Now you have to choose a suitable directory for variable files." - echo "Normally, this directory would be something like /var/local/helm, you" - echo "have to be sure that the directory (and the subdirectories in it)" - echo "is world-writable." - echo - echo -n "[[$DEFAULT_HELM_VAR_DIR]] ? " - read HELM_VAR_DIR - echo - if test x$HELM_VAR_DIR = x; then - HELM_VAR_DIR="/var/local/helm" - fi -else - HELM_VAR_DIR=$DEFAULT_HELM_VAR_DIR -fi - -AC_MSG_CHECKING(for HELM variable dir) -AC_MSG_RESULT($HELM_VAR_DIR) - -dnl Checking for the /tmp directory -DEFAULTS=$USE_DEFAULTS -if test $DEFAULTS = auto; then - if test -d $DEFAULT_HELM_TMP_DIR ; then - HELM_TMP_DIR=$DEFAULT_HELM_TMP_DIR - else - DEFAULTS=no - fi -fi - -if test $DEFAULTS = no; then - echo - echo "Please, tell me the name of a directory which can be used to store" - echo "temporary files (normally it is something like /tmp)" - echo - echo -n "[[$DEFAULT_HELM_TMP_DIR]]" - read HELM_TMP_DIR - echo - if test x$HELM_TMP_DIR = x; then - HELM_TMP_DIR=$DEFAULT_HELM_TMP_DIR - fi -else - HELM_TMP_DIR=$DEFAULT_HELM_TMP_DIR -fi - -AC_MSG_CHECKING(for $HELM_TMP_DIR) -if test ! -d $HELM_TMP_DIR; then - AC_MSG_RESULT(no) - AC_MSG_ERROR(please check your installation) -fi -AC_MSG_RESULT(ok) - -dnl Checks for GtkMathView -AC_CHECK_PROG(HAVE_GTKMATHVIEW_CONFIG, gtkmathview-config, yes, no) -if test $HAVE_GTKMATHVIEW_CONFIG = no; then - AC_MSG_ERROR(Could not find gtkmathview-config) -fi -GTKMATHVIEW_PREFIX=`gtkmathview-config --prefix` - -AC_CACHE_CHECK( - for dictionary.xml, - helm_cv_GTKMATHVIEW_DICTIONARY_PATH, - helm_cv_GTKMATHVIEW_DICTIONARY_PATH=$GTKMATHVIEW_PREFIX/share/gtkmathview/dictionary.xml - if test ! -f $helm_cv_GTKMATHVIEW_DICTIONARY_PATH; then - read helm_cv_GTKMATHVIEW_DICTIONARY_PATH - fi -) -GTKMATHVIEW_DICTIONARY_PATH=$helm_cv_GTKMATHVIEW_DICTIONARY_PATH - -AC_CACHE_CHECK( - for font-configuration.xml, - helm_cv_GTKMATHVIEW_FONT_CONFIGURATION_PATH, - helm_cv_GTKMATHVIEW_FONT_CONFIGURATION_PATH=$GTKMATHVIEW_PREFIX/share/gtkmathview/font-configuration.xml - if test ! -f $helm_cv_GTKMATHVIEW_FONT_CONFIGURATION_PATH; then - read helm_cv_GTKMATHVIEW_FONT_CONFIGURATION_PATH - fi -) -GTKMATHVIEW_FONT_CONFIGURATION_PATH=$helm_cv_GTKMATHVIEW_FONT_CONFIGURATION_PATH - -AC_CACHE_CHECK( - for t1lib configuration file, - helm_cv_GTKMATHVIEW_T1_CONFIG_FILE, - helm_cv_GTKMATHVIEW_T1_CONFIG_FILE=$GTKMATHVIEW_PREFIX/share/gtkmathview/t1.config - if test ! -f $helm_cv_GTKMATHVIEW_T1_CONFIG_FILE; then - read GTKMATHVIEW_T1_CONFIG_FILE - fi -) -GTKMATHVIEW_T1_CONFIG_FILE=$helm_cv_GTKMATHVIEW_T1_CONFIG_FILE - -HELM_DICTIONARY_PATH=$HELM_ETC_DIR/helm-dictionary.xml -HELM_FONT_CONFIGURATION_PATH=$HELM_ETC_DIR/helm-font-configuration.xml - -dnl Only for HELM XML configuration -HELM_LIBRARY_DIR=$HELM_VAR_DIR/library -HELM_SERVERS_FILE=$HELM_VAR_DIR/servers.txt -HELM_URIS_DBM=$HELM_VAR_DIR/urls_of_uris.db - -dnl CSC: FIXME: getters should download the DTDs -HELM_DTD_DIR=$HELM_SHARE_DIR/dtd -HELM_STYLE_DIR=$HELM_SHARE_DIR/style - -dnl HELM prefixes -AC_SUBST(RESOLVED_PREFIX) -AC_SUBST(RESOLVED_EXEC_PREFIX) - -dnl HELM version -AC_SUBST(PACKAGE) -AC_SUBST(VERSION) - -dnl HELM directories -AC_SUBST(HELM_BIN_DIR) -AC_SUBST(HELM_LIB_DIR) -AC_SUBST(HELM_ETC_DIR) -AC_SUBST(HELM_SHARE_DIR) -AC_SUBST(HELM_VAR_DIR) -AC_SUBST(HELM_TMP_DIR) - -dnl HELM download directory -AC_SUBST(HELM_LIBRARY_DIR) - -dnl HELM servers -AC_SUBST(HELM_SERVERS_FILE) - -dnl HELM URIS data-base -AC_SUBST(HELM_URIS_DBM) - -dnl HELM DTDs -AC_SUBST(HELM_DTD_DIR) - -dnl HELM stylesheets -AC_SUBST(HELM_STYLE_DIR) - -dnl HELM customized GtkMathView configuration -AC_SUBST(HELM_DICTIONARY_PATH) -AC_SUBST(HELM_FONT_CONFIGURATION_PATH) -AC_SUBST(GTKMATHVIEW_DICTIONARY_PATH) -AC_SUBST(GTKMATHVIEW_FONT_CONFIGURATION_PATH) -AC_SUBST(GTKMATHVIEW_T1_CONFIG_FILE) - -AC_OUTPUT( -[ Makefile - helm-config - lib/configuration.pl - etc/helm-math-engine-configuration.xml - etc/configuration.xml - helm_configuration.spec -], chmod +x helm-config) diff --git a/helm/configuration/etc/.cvsignore b/helm/configuration/etc/.cvsignore deleted file mode 100644 index c85a7bd9b..000000000 --- a/helm/configuration/etc/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -helm-math-engine-configuration.xml configuration.xml diff --git a/helm/configuration/etc/configuration.dtd b/helm/configuration/etc/configuration.dtd deleted file mode 100644 index 8fc5612a8..000000000 --- a/helm/configuration/etc/configuration.dtd +++ /dev/null @@ -1,60 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/configuration/etc/configuration.xml.in b/helm/configuration/etc/configuration.xml.in deleted file mode 100644 index db034369d..000000000 --- a/helm/configuration/etc/configuration.xml.in +++ /dev/null @@ -1,49 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @HELM_LIBRARY_DIR@ - - @HELM_DTD_DIR@ - @HELM_STYLE_DIR@ - - @HELM_SERVERS_FILE@ - @HELM_URIS_DBM@ - - index.txt - @HELM_TMP_DIR@ - - /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/ - http://localhost:8080/helm/servlet/uwobo/ - diff --git a/helm/configuration/etc/helm-dictionary.xml b/helm/configuration/etc/helm-dictionary.xml deleted file mode 100644 index 6d1caf722..000000000 --- a/helm/configuration/etc/helm-dictionary.xml +++ /dev/null @@ -1,31 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/configuration/etc/helm-font-configuration.xml b/helm/configuration/etc/helm-font-configuration.xml deleted file mode 100644 index b5a9f7cf5..000000000 --- a/helm/configuration/etc/helm-font-configuration.xml +++ /dev/null @@ -1,36 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/configuration/etc/helm-math-engine-configuration.xml.in b/helm/configuration/etc/helm-math-engine-configuration.xml.in deleted file mode 100644 index 96839778f..000000000 --- a/helm/configuration/etc/helm-math-engine-configuration.xml.in +++ /dev/null @@ -1,38 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @HELM_DICTIONARY_PATH@ - @GTKMATHVIEW_DICTIONARY_PATH@ - @HELM_FONT_CONFIGURATION_PATH@ - @GTKMATHVIEW_FONT_CONFIGURATION_PATH@ - @GTKMATHVIEW_T1_CONFIG_FILE@ - - - - - diff --git a/helm/configuration/helm-config.in b/helm/configuration/helm-config.in deleted file mode 100644 index 3b569dec9..000000000 --- a/helm/configuration/helm-config.in +++ /dev/null @@ -1,84 +0,0 @@ - -usage() -{ - cat <&2 -fi - -while test $# -gt 0; do - case "$1" in - -*=*) optarg=`echo "$1" | sed 's/[-_a-zA-Z0-9]*=//'` ;; - *) optarg= ;; - esac - - case $1 in - --version) - echo @VERSION@ - ;; - --prefix) - echo @RESOLVED_PREFIX@ - ;; - --exec-prefix) - echo @RESOLVED_EXEC_PREFIX@ - ;; - --bin-dir) - echo @HELM_BIN_DIR@ - ;; - --lib-dir) - echo @HELM_LIB_DIR@ - ;; - --etc-dir) - echo @HELM_ETC_DIR@ - ;; - --share-dir) - echo @HELM_SHARE_DIR@ - ;; - --var-dir) - echo @HELM_VAR_DIR@ - ;; - --tmp-dir) - echo @HELM_TMP_DIR@ - ;; - --library-dir) - echo @HELM_LIBRARY_DIR@ - ;; - --servers) - echo @HELM_SERVERS_FILE@ - ;; - --uris-dbm) - echo @HELM_URIS_DBM@ - ;; - --dtd-dir) - echo @HELM_DTD_DIR@ - ;; - --style-dir) - echo @HELM_STYLE_DIR@ - ;; - *) - usage 1 1>&2 - ;; - esac - shift -done - diff --git a/helm/configuration/helm_configuration.spec.in b/helm/configuration/helm_configuration.spec.in deleted file mode 100644 index 56695c263..000000000 --- a/helm/configuration/helm_configuration.spec.in +++ /dev/null @@ -1,43 +0,0 @@ -Summary: The configuration files shared by all the tools of project HELM -Name: @PACKAGE@ -Version: @VERSION@ -Release: 1 -Copyright: GPL -URL: http://www.cs.unibo.it/helm -Packager: Claudio Sacerdoti Coen -Group: Applications/Publishing -Source: www.cs.unibo.it:/helm/@PACKAGE@-@VERSION@.tar.gz -%description -HELM (Hypertextual Electronic Library of Mathematics) is a project aimed -at the creation of tools for the development and exploitation of a huge -distributed library of formal mathematical knowledge. This package holds -the configuration files shared by all this tools. -For more information see http://www.cs.unibo.it/helm - -%prep -%setup - -%build -cp config.cache.pkg config.cache -./configure --enable-defaults -make - -%install -make install - -%files -%doc AUTHORS COPYING ChangeLog NEWS README - -/usr/local/bin/helm-config -/usr/local/lib/helm/configuration.pl -/usr/local/etc/helm/configuration.dtd -/usr/local/etc/helm/helm-font-configuration.xml -/usr/local/etc/helm/configuration.xml -/usr/local/etc/helm/helm-math-engine-configuration.xml -/usr/local/etc/helm/helm-dictionary.xml -%attr(666,root,root) /var/local/helm/servers.txt -%attr(666,root,root) /var/local/helm/urls_of_uris.db - -%dir /var/local/helm/library -%dir /usr/local/share/helm/dtd -%dir /usr/local/share/helm/style diff --git a/helm/configuration/lib/.cvsignore b/helm/configuration/lib/.cvsignore deleted file mode 100644 index ff6af6814..000000000 --- a/helm/configuration/lib/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -configuration.pl diff --git a/helm/configuration/lib/configuration.pl.in b/helm/configuration/lib/configuration.pl.in deleted file mode 100644 index 6540b800e..000000000 --- a/helm/configuration/lib/configuration.pl.in +++ /dev/null @@ -1,65 +0,0 @@ -# Copyright (C) 2000, 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://cs.unibo.it/helm/. - -use XML::Parser; - -use Env; -my $HELM_CONFIGURATION_DIR = $ENV{"HELM_CONFIGURATION_DIR"}; -my $DEFAULT_HELM_CONFIGURATION_DIR = "@HELM_ETC_DIR@"; -# this should be the only fixed constant -if (defined ($HELM_CONFIGURATION_DIR)) { - $configuration_file = $HELM_CONFIGURATION_DIR."/configuration.xml"; -} else { - $configuration_file = $DEFAULT_HELM_CONFIGURATION_DIR."/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]; -} diff --git a/helm/configuration/library/servers.txt b/helm/configuration/library/servers.txt deleted file mode 100644 index 5a172e462..000000000 --- a/helm/configuration/library/servers.txt +++ /dev/null @@ -1 +0,0 @@ -http://www.cs.unibo.it/~sacerdot/examples diff --git a/helm/configuration/library/urls_of_uris.db b/helm/configuration/library/urls_of_uris.db deleted file mode 100644 index 9f01b7ae56a99f46c91c897315a822ee4ef873a6..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4096 zcmZQzK!8M1HU?G@SAc z4RQcsT;?ZiU|`^Y1rjbr)DfqTEflyl66nGi_ktWi7@skQKy?buE*u2})ZsIO9J#?3 zfXL~~3WtXdY$7Xt4K}ah@EvKw$l--c=ZDRs;ROpDV!}&dD>>mcERz=lG2s;etaV1q zdq@f!E$?ADjW`-Pec>waH|!uQeGSVDi5y