From 76ad23ea1e83e8c187a4593027e9baed1bb022e3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 18:42:41 +0000 Subject: [PATCH] daemons tamed --- helm/DEVEL/profile-manager/Makefile | 36 - helm/DEVEL/profile-manager/control.html | 240 ------ .../DEVEL/profile-manager/profile-manager.xsl | 55 -- helm/DEVEL/profile-manager/profile.ml | 119 --- helm/DEVEL/profile-manager/profile_manager.ml | 177 ----- .../profile-manager/profile_manager_env.ml | 6 - helm/DEVEL/profile-manager/response.ml | 8 - helm/helm_data/.cvsignore | 1 - helm/helm_data/AUTHORS | 4 - helm/helm_data/ChangeLog | 1 - helm/helm_data/LICENSE | 22 - helm/helm_data/LICENSE.ml | 25 - helm/helm_data/LICENSE.script | 22 - helm/helm_data/LICENSE.xml | 24 - helm/helm_data/Makefile.in | 23 - helm/helm_data/NEWS | 1 - helm/helm_data/README | 9 - helm/helm_data/config.cache.pkg | 4 - helm/helm_data/configure.in | 61 -- helm/helm_data/helm_data.spec.in | 34 - helm/helmpot/.cvsignore | 18 - helm/helmpot/AUTHORS | 1 - helm/helmpot/ChangeLog | 0 helm/helmpot/LICENSE | 23 - helm/helmpot/Makefile.am | 26 - helm/helmpot/NEWS | 0 helm/helmpot/README | 18 - helm/helmpot/acconfig.h | 47 -- helm/helmpot/configure.in | 70 -- helm/helmpot/debian/changelog | 42 -- helm/helmpot/debian/control | 14 - helm/helmpot/debian/copyright | 30 - helm/helmpot/debian/docs | 2 - helm/helmpot/debian/rules | 75 -- helm/helmpot/guiGTK.c | 684 ------------------ helm/helmpot/guiGTK.h | 50 -- helm/helmpot/helmpot.spec.in | 24 - helm/helmpot/main.c | 121 ---- helm/helmpot/pot_mask | 6 - helm/http_getter/COPYING | 340 --------- .../daemons}/graphs/jsmenu/HM_Arrays.js | 0 .../daemons}/graphs/jsmenu/HM_Arrays_prova.js | 0 .../daemons}/graphs/jsmenu/HM_Loader.js | 0 .../daemons}/graphs/jsmenu/HM_Loader_prova.js | 0 .../graphs/jsmenu/HM_More_black_left.gif | Bin .../graphs/jsmenu/HM_More_black_right.gif | Bin .../graphs/jsmenu/HM_More_blue_left.gif | Bin .../graphs/jsmenu/HM_More_blue_right.gif | Bin .../graphs/jsmenu/HM_More_cyan_left.gif | Bin .../graphs/jsmenu/HM_More_cyan_right.gif | Bin .../graphs/jsmenu/HM_More_green_left.gif | Bin .../graphs/jsmenu/HM_More_green_right.gif | Bin .../graphs/jsmenu/HM_More_magenta_left.gif | Bin .../graphs/jsmenu/HM_More_magenta_right.gif | Bin .../graphs/jsmenu/HM_More_red_left.gif | Bin .../graphs/jsmenu/HM_More_red_right.gif | Bin .../graphs/jsmenu/HM_More_white_left.gif | Bin .../graphs/jsmenu/HM_More_white_right.gif | Bin .../graphs/jsmenu/HM_More_yellow_left.gif | Bin .../graphs/jsmenu/HM_More_yellow_right.gif | Bin .../daemons}/graphs/jsmenu/HM_ScriptDOM.js | 0 .../daemons}/graphs/jsmenu/HM_ScriptIE4.js | 0 .../daemons}/graphs/jsmenu/HM_ScriptNS4.js | 0 .../daemons}/graphs/jsmenu/LoadMe.html | 0 .../daemons}/graphs/jsmenu/prova.gif | Bin .../daemons}/graphs/jsmenu/prova.html | 0 .../daemons}/graphs/tools/.cvsignore | 0 .../daemons}/graphs/tools/Makefile | 0 .../graphs/tools/drawGraph.conf.xml.sample | 0 .../daemons}/graphs/tools/drawGraph.ml | 0 .../daemons}/graphs/tools/mk_html.pl | 0 .../graphs/tools/simplify_deps/.cvsignore | 0 .../graphs/tools/simplify_deps/Makefile | 0 .../tools/simplify_deps/simplify_deps.ml | 0 .../graphs/tools/uriSetQueue.conf.xml.sample | 0 .../daemons}/graphs/tools/uriSetQueue.ml | 0 .../daemons}/http_getter/.cvsignore | 0 .../daemons}/http_getter/AUTHORS | 0 helm/{ => software/daemons}/http_getter/BUGS | 0 .../daemons/http_getter}/COPYING | 0 .../daemons}/http_getter/ChangeLog | 0 .../daemons}/http_getter/Makefile | 0 .../daemons}/http_getter/Makefile.overrides | 0 helm/{ => software/daemons}/http_getter/NEWS | 0 .../{ => software/daemons}/http_getter/README | 0 .../daemons}/http_getter/buildTimeOpts.ml.in | 0 .../daemons}/http_getter/configure.ac | 0 .../http_getter/http_getter.conf.xml.sample | 0 .../daemons}/http_getter/main.ml | 0 .../daemons}/http_getter/panel/.cvsignore | 0 .../daemons}/http_getter/panel/Makefile | 0 .../daemons}/http_getter/panel/control.html | 0 .../daemons}/http_getter/panel/control.js | 0 .../daemons/http_getter/panel}/index.html | 0 .../daemons/http_getter/panel}/welcome.html | 0 .../daemons}/http_getter/tools/dump_db.ml | 0 .../daemons}/http_getter/tools/dump_db.pl | 0 .../daemons}/http_getter/tools/uri_escape.pl | 0 .../http_getter/tools/uri_unescape.pl | 0 .../daemons}/proofChecker/.cvsignore | 0 .../daemons}/proofChecker/.depend | 0 .../daemons}/proofChecker/Makefile | 0 .../proofChecker/proofChecker.conf.xml.sample | 0 .../daemons}/proofChecker/proofChecker.ml | 0 .../daemons}/rdfly/.cvsignore | 0 .../daemons}/rdfly/Makefile | 0 .../daemons}/rdfly/rdfly.conf.xml.sample | 0 .../daemons}/rdfly/rdfly.ml | 0 helm/{ => software/daemons}/uwobo/.cvsignore | 0 helm/{ => software/daemons}/uwobo/.depend | 0 helm/{ => software/daemons}/uwobo/Makefile | 0 .../daemons}/uwobo/doc/uwobo.tex | 0 .../daemons}/uwobo/log/.cvsignore | 0 .../daemons/uwobo/panel}/.cvsignore | 0 .../daemons/uwobo/panel}/Makefile | 0 .../daemons/uwobo/panel}/control.html | 0 .../daemons/uwobo/panel}/control.js | 0 .../daemons/uwobo}/panel/index.html | 0 .../daemons/uwobo}/panel/welcome.html | 0 .../daemons}/uwobo/uwobo.conf.xml.sample | 0 helm/{ => software/daemons}/uwobo/uwobo.ml | 0 .../daemons}/uwobo/uwobo_common.ml | 0 .../daemons}/uwobo/uwobo_common.mli | 0 .../daemons}/uwobo/uwobo_engine.ml | 0 .../daemons}/uwobo/uwobo_engine.mli | 0 .../daemons}/uwobo/uwobo_logger.ml | 0 .../daemons}/uwobo/uwobo_logger.mli | 0 .../daemons}/uwobo/uwobo_profiles.ml | 0 .../daemons}/uwobo/uwobo_profiles.mli | 0 .../daemons}/uwobo/uwobo_styles.ml | 0 .../daemons}/uwobo/uwobo_styles.mli | 0 .../daemons/whelp}/.cvsignore | 0 .../daemons/whelp}/.depend | 0 .../daemons/whelp}/Makefile | 0 .../daemons/whelp}/html/Makefile | 0 .../daemons/whelp}/html/includes.xsl | 0 .../daemons/whelp}/html/manual/alias.jpg | Bin .../daemons/whelp}/html/manual/ex1.jpg | Bin .../daemons/whelp}/html/manual/frames.jpg | Bin .../daemons/whelp}/html/manual/index.html | 0 .../daemons/whelp}/html/moogle.html.src | 0 .../daemons/whelp}/html/moogle.png | Bin .../daemons/whelp}/html/moogle_chat.html.src | 0 .../daemons/whelp}/html/moogle_form.html.src | 0 .../whelp}/html/moogle_header.html.src | 0 .../daemons/whelp}/html/moogle_help.html | 0 .../daemons/whelp}/html/moogle_init.html | 0 .../whelp}/html/moogle_querybar.html.src | 0 .../daemons/whelp}/html/moogle_small.png | Bin .../daemons/whelp}/html/moogle_syntax.html | 0 .../whelp}/html/moogle_trailer.html.src | 0 .../daemons/whelp}/html/whelp.png | Bin .../daemons/whelp}/html/whelp.svg | 0 .../daemons/whelp}/html/whelp_small.png | Bin .../daemons/whelp}/mooglePp.ml | 0 .../daemons/whelp}/mooglePp.mli | 0 .../daemons/whelp}/preloaded_uris.txt | 0 .../whelp}/searchEngine.conf.xml.sample | 0 .../daemons/whelp}/searchEngine.ml | 0 helm/uwobo-panel/index.html | 8 - helm/uwobo-panel/welcome.html | 6 - helm/xmltheory/Coq_v2theoryxml/.cvsignore | 1 - helm/xmltheory/Coq_v2theoryxml/.depend | 0 helm/xmltheory/Coq_v2theoryxml/Makefile | 17 - .../Coq_v2theoryxml/coq_v2theoryxml.ml | 176 ----- helm/xmltheory/FakeCoq_vo2xml/README | 3 - helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml | 4 - helm/xmltheory/XmlTheory/.cvsignore | 1 - helm/xmltheory/XmlTheory/.depend | 8 - helm/xmltheory/XmlTheory/COME_COMPILARE | 5 - helm/xmltheory/XmlTheory/Make | 5 - helm/xmltheory/XmlTheory/Makefile | 165 ----- helm/xmltheory/XmlTheory/README | 78 -- helm/xmltheory/XmlTheory/XmlTheory.v | 15 - helm/xmltheory/XmlTheory/iXml.ml | 53 -- helm/xmltheory/XmlTheory/iXml.mli | 7 - helm/xmltheory/XmlTheory/xmltheoryentries.ml | 371 ---------- helm/xmltheory/maththeory.dtd | 78 -- 178 files changed, 3464 deletions(-) delete mode 100644 helm/DEVEL/profile-manager/Makefile delete mode 100644 helm/DEVEL/profile-manager/control.html delete mode 100644 helm/DEVEL/profile-manager/profile-manager.xsl delete mode 100644 helm/DEVEL/profile-manager/profile.ml delete mode 100644 helm/DEVEL/profile-manager/profile_manager.ml delete mode 100644 helm/DEVEL/profile-manager/profile_manager_env.ml delete mode 100644 helm/DEVEL/profile-manager/response.ml delete mode 100644 helm/helm_data/.cvsignore delete mode 100644 helm/helm_data/AUTHORS delete mode 100644 helm/helm_data/ChangeLog delete mode 100644 helm/helm_data/LICENSE delete mode 100644 helm/helm_data/LICENSE.ml delete mode 100644 helm/helm_data/LICENSE.script delete mode 100644 helm/helm_data/LICENSE.xml delete mode 100644 helm/helm_data/Makefile.in delete mode 100644 helm/helm_data/NEWS delete mode 100644 helm/helm_data/README delete mode 100644 helm/helm_data/config.cache.pkg delete mode 100644 helm/helm_data/configure.in delete mode 100644 helm/helm_data/helm_data.spec.in delete mode 100644 helm/helmpot/.cvsignore delete mode 100644 helm/helmpot/AUTHORS delete mode 100644 helm/helmpot/ChangeLog delete mode 100644 helm/helmpot/LICENSE delete mode 100644 helm/helmpot/Makefile.am delete mode 100644 helm/helmpot/NEWS delete mode 100644 helm/helmpot/README delete mode 100644 helm/helmpot/acconfig.h delete mode 100644 helm/helmpot/configure.in delete mode 100644 helm/helmpot/debian/changelog delete mode 100644 helm/helmpot/debian/control delete mode 100644 helm/helmpot/debian/copyright delete mode 100644 helm/helmpot/debian/docs delete mode 100755 helm/helmpot/debian/rules delete mode 100644 helm/helmpot/guiGTK.c delete mode 100644 helm/helmpot/guiGTK.h delete mode 100644 helm/helmpot/helmpot.spec.in delete mode 100644 helm/helmpot/main.c delete mode 100644 helm/helmpot/pot_mask delete mode 100644 helm/http_getter/COPYING rename helm/{ => software/daemons}/graphs/jsmenu/HM_Arrays.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_Arrays_prova.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_Loader.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_Loader_prova.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_black_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_black_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_blue_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_blue_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_cyan_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_cyan_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_green_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_green_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_magenta_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_magenta_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_red_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_red_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_white_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_white_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_yellow_left.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_More_yellow_right.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_ScriptDOM.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_ScriptIE4.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/HM_ScriptNS4.js (100%) rename helm/{ => software/daemons}/graphs/jsmenu/LoadMe.html (100%) rename helm/{ => software/daemons}/graphs/jsmenu/prova.gif (100%) rename helm/{ => software/daemons}/graphs/jsmenu/prova.html (100%) rename helm/{ => software/daemons}/graphs/tools/.cvsignore (100%) rename helm/{ => software/daemons}/graphs/tools/Makefile (100%) rename helm/{ => software/daemons}/graphs/tools/drawGraph.conf.xml.sample (100%) rename helm/{ => software/daemons}/graphs/tools/drawGraph.ml (100%) rename helm/{ => software/daemons}/graphs/tools/mk_html.pl (100%) rename helm/{ => software/daemons}/graphs/tools/simplify_deps/.cvsignore (100%) rename helm/{ => software/daemons}/graphs/tools/simplify_deps/Makefile (100%) rename helm/{ => software/daemons}/graphs/tools/simplify_deps/simplify_deps.ml (100%) rename helm/{ => software/daemons}/graphs/tools/uriSetQueue.conf.xml.sample (100%) rename helm/{ => software/daemons}/graphs/tools/uriSetQueue.ml (100%) rename helm/{ => software/daemons}/http_getter/.cvsignore (100%) rename helm/{ => software/daemons}/http_getter/AUTHORS (100%) rename helm/{ => software/daemons}/http_getter/BUGS (100%) rename helm/{helm_data => software/daemons/http_getter}/COPYING (100%) rename helm/{ => software/daemons}/http_getter/ChangeLog (100%) rename helm/{ => software/daemons}/http_getter/Makefile (100%) rename helm/{ => software/daemons}/http_getter/Makefile.overrides (100%) rename helm/{ => software/daemons}/http_getter/NEWS (100%) rename helm/{ => software/daemons}/http_getter/README (100%) rename helm/{ => software/daemons}/http_getter/buildTimeOpts.ml.in (100%) rename helm/{ => software/daemons}/http_getter/configure.ac (100%) rename helm/{ => software/daemons}/http_getter/http_getter.conf.xml.sample (100%) rename helm/{ => software/daemons}/http_getter/main.ml (100%) rename helm/{ => software/daemons}/http_getter/panel/.cvsignore (100%) rename helm/{ => software/daemons}/http_getter/panel/Makefile (100%) rename helm/{ => software/daemons}/http_getter/panel/control.html (100%) rename helm/{ => software/daemons}/http_getter/panel/control.js (100%) rename helm/{DEVEL/profile-manager => software/daemons/http_getter/panel}/index.html (100%) rename helm/{DEVEL/profile-manager => software/daemons/http_getter/panel}/welcome.html (100%) rename helm/{ => software/daemons}/http_getter/tools/dump_db.ml (100%) rename helm/{ => software/daemons}/http_getter/tools/dump_db.pl (100%) rename helm/{ => software/daemons}/http_getter/tools/uri_escape.pl (100%) rename helm/{ => software/daemons}/http_getter/tools/uri_unescape.pl (100%) rename helm/{ => software/daemons}/proofChecker/.cvsignore (100%) rename helm/{ => software/daemons}/proofChecker/.depend (100%) rename helm/{ => software/daemons}/proofChecker/Makefile (100%) rename helm/{ => software/daemons}/proofChecker/proofChecker.conf.xml.sample (100%) rename helm/{ => software/daemons}/proofChecker/proofChecker.ml (100%) rename helm/{DEVEL => software/daemons}/rdfly/.cvsignore (100%) rename helm/{DEVEL => software/daemons}/rdfly/Makefile (100%) rename helm/{DEVEL => software/daemons}/rdfly/rdfly.conf.xml.sample (100%) rename helm/{DEVEL => software/daemons}/rdfly/rdfly.ml (100%) rename helm/{ => software/daemons}/uwobo/.cvsignore (100%) rename helm/{ => software/daemons}/uwobo/.depend (100%) rename helm/{ => software/daemons}/uwobo/Makefile (100%) rename helm/{ => software/daemons}/uwobo/doc/uwobo.tex (100%) rename helm/{ => software/daemons}/uwobo/log/.cvsignore (100%) rename helm/{uwobo-panel => software/daemons/uwobo/panel}/.cvsignore (100%) rename helm/{uwobo-panel => software/daemons/uwobo/panel}/Makefile (100%) rename helm/{uwobo-panel => software/daemons/uwobo/panel}/control.html (100%) rename helm/{uwobo-panel => software/daemons/uwobo/panel}/control.js (100%) rename helm/{http_getter => software/daemons/uwobo}/panel/index.html (100%) rename helm/{http_getter => software/daemons/uwobo}/panel/welcome.html (100%) rename helm/{ => software/daemons}/uwobo/uwobo.conf.xml.sample (100%) rename helm/{ => software/daemons}/uwobo/uwobo.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_common.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_common.mli (100%) rename helm/{ => software/daemons}/uwobo/uwobo_engine.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_engine.mli (100%) rename helm/{ => software/daemons}/uwobo/uwobo_logger.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_logger.mli (100%) rename helm/{ => software/daemons}/uwobo/uwobo_profiles.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_profiles.mli (100%) rename helm/{ => software/daemons}/uwobo/uwobo_styles.ml (100%) rename helm/{ => software/daemons}/uwobo/uwobo_styles.mli (100%) rename helm/{searchEngine => software/daemons/whelp}/.cvsignore (100%) rename helm/{searchEngine => software/daemons/whelp}/.depend (100%) rename helm/{searchEngine => software/daemons/whelp}/Makefile (100%) rename helm/{searchEngine => software/daemons/whelp}/html/Makefile (100%) rename helm/{searchEngine => software/daemons/whelp}/html/includes.xsl (100%) rename helm/{searchEngine => software/daemons/whelp}/html/manual/alias.jpg (100%) rename helm/{searchEngine => software/daemons/whelp}/html/manual/ex1.jpg (100%) rename helm/{searchEngine => software/daemons/whelp}/html/manual/frames.jpg (100%) rename helm/{searchEngine => software/daemons/whelp}/html/manual/index.html (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle.png (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_chat.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_form.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_header.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_help.html (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_init.html (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_querybar.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_small.png (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_syntax.html (100%) rename helm/{searchEngine => software/daemons/whelp}/html/moogle_trailer.html.src (100%) rename helm/{searchEngine => software/daemons/whelp}/html/whelp.png (100%) rename helm/{searchEngine => software/daemons/whelp}/html/whelp.svg (100%) rename helm/{searchEngine => software/daemons/whelp}/html/whelp_small.png (100%) rename helm/{searchEngine => software/daemons/whelp}/mooglePp.ml (100%) rename helm/{searchEngine => software/daemons/whelp}/mooglePp.mli (100%) rename helm/{searchEngine => software/daemons/whelp}/preloaded_uris.txt (100%) rename helm/{searchEngine => software/daemons/whelp}/searchEngine.conf.xml.sample (100%) rename helm/{searchEngine => software/daemons/whelp}/searchEngine.ml (100%) delete mode 100644 helm/uwobo-panel/index.html delete mode 100644 helm/uwobo-panel/welcome.html delete mode 100644 helm/xmltheory/Coq_v2theoryxml/.cvsignore delete mode 100644 helm/xmltheory/Coq_v2theoryxml/.depend delete mode 100644 helm/xmltheory/Coq_v2theoryxml/Makefile delete mode 100644 helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml delete mode 100644 helm/xmltheory/FakeCoq_vo2xml/README delete mode 100755 helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml delete mode 100644 helm/xmltheory/XmlTheory/.cvsignore delete mode 100644 helm/xmltheory/XmlTheory/.depend delete mode 100644 helm/xmltheory/XmlTheory/COME_COMPILARE delete mode 100644 helm/xmltheory/XmlTheory/Make delete mode 100644 helm/xmltheory/XmlTheory/Makefile delete mode 100644 helm/xmltheory/XmlTheory/README delete mode 100644 helm/xmltheory/XmlTheory/XmlTheory.v delete mode 100644 helm/xmltheory/XmlTheory/iXml.ml delete mode 100644 helm/xmltheory/XmlTheory/iXml.mli delete mode 100644 helm/xmltheory/XmlTheory/xmltheoryentries.ml delete mode 100644 helm/xmltheory/maththeory.dtd diff --git a/helm/DEVEL/profile-manager/Makefile b/helm/DEVEL/profile-manager/Makefile deleted file mode 100644 index 556644338..000000000 --- a/helm/DEVEL/profile-manager/Makefile +++ /dev/null @@ -1,36 +0,0 @@ -BIN_DIR = /usr/local/bin -REQUIRES = http -PREDICATES = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -OCAMLFIND = ocamlfind -OCAMLC = $(OCAMLFIND) ocamlc -thread $(OCAMLOPTIONS) -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(OCAMLOPTIONS) -OCAMLDEP = ocamldep -pp camlp4o - -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)) - -OBJS = response.cmo profile.cmo profile_manager_env.cmo profile_manager.cmo - -profile-manager: $(OBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o $@ $(OBJS) - -profile-manager.opt: $(OBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o $@ $(OBJS:.cmo=.cmx) - -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: - $(OCAMLC) -c $< -.mli.cmi: - $(OCAMLC) -c $< -.ml.cmx: - $(OCAMLOPT) -c $< - -$(OBJS): $(LIBRARIES) -$(OBJS:.cmo=.cmx)): $(LIBRARIES_OPT) - -clean: - rm -f *.cm[iox] *.o rdfly rdfly.opt - -.PHONY: install uninstall clean - diff --git a/helm/DEVEL/profile-manager/control.html b/helm/DEVEL/profile-manager/control.html deleted file mode 100644 index 2feb02fe9..000000000 --- a/helm/DEVEL/profile-manager/control.html +++ /dev/null @@ -1,240 +0,0 @@ - - - -Profile Manager Control Panel - - - - - - - - - - - -
Profile Manager Control Panel
- -
- -
-This is a control panel for the profile manager. You can control a -local or remote profile manager by filling the appropriate field below -and sending the desired commands. Any command issued to the profile -manager results into an XML response. Note that in order to use this -page you must have JavaScript enabled. If you have troubles, -please send an email to the author: lpadovan at cs dot unibo dot it. -
- -

-

-WARNING: the information stored in a profile, -including the password, IS NOT encrypted in the profile nor while it -is travelling from your computer to the profile manager. DO NOT USE -THE PROFILE MANAGER FOR STORING SENSIBLE INFORMATION LIKE PASSWORDS -FOR SECURE ACCOUNTS OR ANY OTHER PERSONAL DATA.
-

- -
-
- - - - - - - - - - - - - - - - - - - - - - - -
-
- Profile Manager URL - - -
-
-
- List the profiles currently stored in the Profile Manager
- -
-
-
- Create a new profile
- - - -
Profile ID: (leave blank if you want an ID to be assigned automatically)
Password: (optional)
- -
-
-
- Delete an existing profile
- - - -
Profile ID:
Password: (optional)
- -
-
-
- Retrieve an existing profile
- - - -
Profile ID:
Password: (optional)
- -
-
-
- Set the value for a field in an existing profile
- - - - - -
Profile ID:
Password: (optional)
Field:
Value: (optional, if blank will remove the field from the profile)
- -
-
-
- Set/Change the password for a profile
- - - - -
Profile ID:
Old password: (optional)
New password: (optional)
- -
-
-
- Set the access capabilities for a profile
- - - - - - -
Profile ID:
Password: (optional)
Read access: - -
Write access: - -
Profile access: - -
- -
-
-
- - - - - diff --git a/helm/DEVEL/profile-manager/profile-manager.xsl b/helm/DEVEL/profile-manager/profile-manager.xsl deleted file mode 100644 index e32d58739..000000000 --- a/helm/DEVEL/profile-manager/profile-manager.xsl +++ /dev/null @@ -1,55 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/helm/DEVEL/profile-manager/profile.ml b/helm/DEVEL/profile-manager/profile.ml deleted file mode 100644 index 9c19b3c9d..000000000 --- a/helm/DEVEL/profile-manager/profile.ml +++ /dev/null @@ -1,119 +0,0 @@ - -exception Permission_denied -exception Invalid_access of string - -type access_t = - Allowed - | Denied - | Password - -let access_of_string old = - function - None -> old - | Some "allowed" -> Allowed - | Some "denied" -> Denied - | Some "password" -> Password - | Some s -> raise (Invalid_access s) - -let string_of_access = - function - Allowed -> "allowed" - | Denied -> "denied" - | Password -> "password" - -type t = - { id : string; - mutable password : string; - mutable read_access : access_t; - mutable write_access : access_t; - mutable profile_access : access_t; - data : (string, string) Hashtbl.t; - } - -let serialize profile with_data = - let serialize_data data = - let sl = ref [] in - Hashtbl.iter - (fun field value -> - sl := (" " ^ (Response.quote value) ^ "\n")::!sl) - data ; - List.fold_left (^) "" !sl - in - "\n" ^ (if with_data then serialize_data profile.data else "") ^ "" - -let create key pwd = - let access, pwd' = - match pwd with - Some s -> Password, s - | None -> Allowed, "" - in - let profile = - { id = key; - password = pwd'; - read_access = access; - write_access = access; - profile_access = access; - data = Hashtbl.create 11 - } - in - profile - -let test_read_access profile pwd = - match pwd, profile.read_access with - Some s, Password when s = profile.password -> () - | None, Password when profile.password = "" -> () - | _, Allowed -> () - | _ -> raise Permission_denied - -let test_write_access profile pwd = - match pwd, profile.write_access with - Some s, Password when s = profile.password -> () - | None, Password when profile.password = "" -> () - | _, Allowed -> () - | _ -> raise Permission_denied - -let test_profile_access profile pwd = - match pwd, profile.profile_access with - Some s, Password when s = profile.password -> () - | None, Password when profile.password = "" -> () - | _, Allowed -> () - | _ -> raise Permission_denied - -let get profile pwd = - test_read_access profile pwd ; - serialize profile true - -let set profile field value pwd = - test_write_access profile pwd ; - begin - match value with - Some value' -> Hashtbl.replace profile.data field value' - | None -> Hashtbl.remove profile.data field - end ; - Response.ok () - -let del profile pwd = - test_profile_access profile pwd ; - Response.ok () - -let set_password profile new_pwd pwd = - test_profile_access profile pwd ; - let new_pwd' = - match new_pwd with - Some s -> s - | None -> "" - in - prerr_endline ("old " ^ profile.password ^ " new " ^ new_pwd') ; - profile.password <- new_pwd' ; - Response.ok () - -let set_access profile read_access write_access profile_access pwd = - test_profile_access profile pwd ; - profile.read_access <- access_of_string profile.read_access read_access ; - profile.write_access <- access_of_string profile.write_access write_access ; - profile.profile_access <- access_of_string profile.profile_access profile_access ; - Response.ok () diff --git a/helm/DEVEL/profile-manager/profile_manager.ml b/helm/DEVEL/profile-manager/profile_manager.ml deleted file mode 100644 index 1c61e6a3f..000000000 --- a/helm/DEVEL/profile-manager/profile_manager.ml +++ /dev/null @@ -1,177 +0,0 @@ -(* - * Copyright (C) 2003: - * Stefano Zacchiroli - * for the HELM Team http://helm.cs.unibo.it/ - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -exception Impossible - -let (profile_db : (string, Profile.t) Hashtbl.t) = - try - let ch = open_in Profile_manager_env.profile_db_path in - input_value ch - with - _ -> Hashtbl.create 211 - -let get_param_opt (req : Http_types.request) p = - try - match req#param p with - "" -> None - | s -> Some s - with - Http_types.Param_not_found _ -> None - -let new_key () = - let hex_of_nibble n = - if n >= 0 && n < 10 then - string_of_int n - else if n >= 10 && n < 16 then - String.make 1 (Char.chr (n - 10 + (Char.code 'A'))) - else - raise Impossible - in - let rec aux s = - function - 0 -> s - | n -> aux ((hex_of_nibble (Random.int 16)) ^ s) (n - 1) - in - aux "" 4 - -let new_unique_key = - let rec aux () = - let key = new_key () in - if Hashtbl.mem profile_db key then - aux () - else - key - in - aux - -let list_profiles () = - let pl = ref [] in - Hashtbl.iter - (fun _ profile -> pl := (Profile.serialize profile false) :: !pl) - profile_db ; - "" ^ (List.fold_left (^) "" !pl) ^ "" - -let get_profile id pwd = - let profile = Hashtbl.find profile_db id in - Profile.get profile pwd - -let new_profile id pwd = - match id with - Some id' when Hashtbl.mem profile_db id' -> get_profile id' pwd - | Some id' -> - let profile = Profile.create id' pwd in - Hashtbl.add profile_db profile.Profile.id profile ; - Profile.serialize profile true - | None -> - let profile = Profile.create (new_unique_key ()) None in - Hashtbl.add profile_db profile.Profile.id profile ; - Profile.serialize profile true - -let set_profile id field value pwd = - let profile = Hashtbl.find profile_db id in - Profile.set profile field value pwd - -let del_profile id pwd = - let profile = Hashtbl.find profile_db id in - let res = Profile.del profile pwd in - Hashtbl.remove profile_db id ; - res - -let set_password id new_pwd pwd = - let profile = Hashtbl.find profile_db id in - Profile.set_password profile new_pwd pwd - -let set_access id read_access write_access profile_access pwd = - let profile = Hashtbl.find profile_db id in - Profile.set_access profile read_access write_access profile_access pwd - -let callback (req : Http_types.request) outchan = - let res = - try - prerr_endline ("Connection from " ^ req#clientAddr) ; - prerr_endline ("Received request: " ^ req#path) ; - begin - match req#path with - "/list" -> list_profiles () - | "/get" -> - let id = req#param "id" - and pwd = get_param_opt req "password" in - get_profile id pwd - | "/set" -> - let id = req#param "id" - and field = req#param "field" - and value = get_param_opt req "value" - and pwd = get_param_opt req "password" in - set_profile id field value pwd - | "/del" -> - let id = req#param "id" - and pwd = get_param_opt req "password" in - del_profile id pwd - | "/new" -> - let id = get_param_opt req "id" - and pwd = get_param_opt req "password" in - new_profile id pwd - | "/password" -> - let id = req#param "id" - and old_pwd = get_param_opt req "old_password" - and new_pwd = get_param_opt req "new_password" in - set_password id new_pwd old_pwd - | "/access" -> - let id = req#param "id" - and pwd = get_param_opt req "password" - and read_access = get_param_opt req "read" - and write_access = get_param_opt req "write" - and profile_access = get_param_opt req "profile" in - set_access id read_access write_access profile_access pwd - | s -> Response.error ("unrecognized command: " ^ s) - end - with - Not_found -> Response.error "unknown profile" - | Profile.Permission_denied -> Response.error "permission denied" - | e -> Response.error ("uncaught exception: " ^ (Printexc.to_string e)) - in - Http_daemon.respond - ~body:res ~headers:["Content-Type", "text/xml"] outchan - - (* daemon initialization *) - -let save_db () = - let ch = open_out Profile_manager_env.profile_db_path in - output_value ch profile_db ; - close_out ch - -let main () = - at_exit save_db ; - Sys.catch_break true ; - try - Http_daemon.start' ~timeout:(Some 600) ~port:58099 ~mode:`Thread callback - with - Sys.Break -> () -in -main () - diff --git a/helm/DEVEL/profile-manager/profile_manager_env.ml b/helm/DEVEL/profile-manager/profile_manager_env.ml deleted file mode 100644 index cac43bd4e..000000000 --- a/helm/DEVEL/profile-manager/profile_manager_env.ml +++ /dev/null @@ -1,6 +0,0 @@ - -let profile_db_path = - try - Sys.getenv "PROFILE_MANAGER_DB_PATH" - with - Not_found -> "/tmp/profile.db" diff --git a/helm/DEVEL/profile-manager/response.ml b/helm/DEVEL/profile-manager/response.ml deleted file mode 100644 index e47a66651..000000000 --- a/helm/DEVEL/profile-manager/response.ml +++ /dev/null @@ -1,8 +0,0 @@ - -let quote_attribute s = s - -let quote s = s - -let error s = "" ^ (quote s) ^ "" - -let ok () = "" diff --git a/helm/helm_data/.cvsignore b/helm/helm_data/.cvsignore deleted file mode 100644 index cbb473e0b..000000000 --- a/helm/helm_data/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -Makefile configure config.log config.cache config.status diff --git a/helm/helm_data/AUTHORS b/helm/helm_data/AUTHORS deleted file mode 100644 index 963977a6f..000000000 --- a/helm/helm_data/AUTHORS +++ /dev/null @@ -1,4 +0,0 @@ -Andrea Asperti -Luca Padovani -Claudio Sacerdoti Coen -Irene Schena diff --git a/helm/helm_data/ChangeLog b/helm/helm_data/ChangeLog deleted file mode 100644 index 20c36b475..000000000 --- a/helm/helm_data/ChangeLog +++ /dev/null @@ -1 +0,0 @@ -28/12/2000: First alpha release diff --git a/helm/helm_data/LICENSE b/helm/helm_data/LICENSE deleted file mode 100644 index 72f9426c8..000000000 --- a/helm/helm_data/LICENSE +++ /dev/null @@ -1,22 +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/. diff --git a/helm/helm_data/LICENSE.ml b/helm/helm_data/LICENSE.ml deleted file mode 100644 index 2f1b31e35..000000000 --- a/helm/helm_data/LICENSE.ml +++ /dev/null @@ -1,25 +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/. - *) - diff --git a/helm/helm_data/LICENSE.script b/helm/helm_data/LICENSE.script deleted file mode 100644 index bad51618d..000000000 --- a/helm/helm_data/LICENSE.script +++ /dev/null @@ -1,22 +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/. diff --git a/helm/helm_data/LICENSE.xml b/helm/helm_data/LICENSE.xml deleted file mode 100644 index 6077c5215..000000000 --- a/helm/helm_data/LICENSE.xml +++ /dev/null @@ -1,24 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/helm_data/Makefile.in b/helm/helm_data/Makefile.in deleted file mode 100644 index 498577fa0..000000000 --- a/helm/helm_data/Makefile.in +++ /dev/null @@ -1,23 +0,0 @@ - -HELM_DTD_DIR=@HELM_DTD_DIR@ -HELM_STYLE_DIR=@HELM_STYLE_DIR@ - -all: - -install: - cp dtd/* $(HELM_DTD_DIR) - cp style/*.xsl $(HELM_STYLE_DIR) - -clean: - -distclean: clean - rm -f Makefile configure config.log config.cache config.status *.spec - rm -rf dtd style - -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/helm_data/NEWS b/helm/helm_data/NEWS deleted file mode 100644 index 20c36b475..000000000 --- a/helm/helm_data/NEWS +++ /dev/null @@ -1 +0,0 @@ -28/12/2000: First alpha release diff --git a/helm/helm_data/README b/helm/helm_data/README deleted file mode 100644 index cc0522b13..000000000 --- a/helm/helm_data/README +++ /dev/null @@ -1,9 +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 base DTDs and XSLT stylesheets developed by the members of project -HELM. - -For more information see http://www.cs.unibo.it/helm diff --git a/helm/helm_data/config.cache.pkg b/helm/helm_data/config.cache.pkg deleted file mode 100644 index 5d80ae922..000000000 --- a/helm/helm_data/config.cache.pkg +++ /dev/null @@ -1,4 +0,0 @@ -# This is the config.cache that holds the ``standard'' path for the -# HELM library. It is supposed to be used when creating packages - -helm_cv_HELM_DTDS_DIR=${helm_cv_HELM_DTDS_DIR='$RESOLVED_PREFIX/share/helm/dtd'} diff --git a/helm/helm_data/configure.in b/helm/helm_data/configure.in deleted file mode 100644 index 635258995..000000000 --- a/helm/helm_data/configure.in +++ /dev/null @@ -1,61 +0,0 @@ -AC_INIT(dtd/cic.dtd) - -PACKAGE=helm_data -MAJOR_VERSION=0 -MINOR_VERSION=0 -MICRO_VERSION=2 -VERSION=$MAJOR_VERSION.$MINOR_VERSION.$MICRO_VERSION - -DEFAULT_HELM_DTD_DIR=/usr/local/share/helm/dtd -DEFAULT_HELM_STYLE_DIR=/usr/local/share/helm/style - -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 $USE_DEFAULTS = auto; then - AC_CHECK_PROG(HAVE_HELM_CONFIG, helm-config, yes, no) - if test $HAVE_HELM_CONFIG = yes; then - HELM_DTD_DIR=`helm-config --dtd-dir` - HELM_STYLE_DIR=`helm-config --style-dir` - else - USE_DEFAULTS=no - fi -fi - -if test $USE_DEFAULTS = no; then - echo - echo "\`helm-config' is not installed (or I can't find it in your path)." - echo "Please, insert the directory where I can find the DTDs for HELM..." - echo - echo -n "[[$DEFAULT_HELM_DTD_DIR]] ? " - read HELM_DTD_DIR - if test "x$HELM_DTD_DIR" = "x"; then - HELM_DTD_DIR=$DEFAULT_HELM_DTD_DIR - fi - echo - echo "Please, insert the directory where I can find the stylesheets for HELM..." - echo - echo -n "[[$DEFAULT_HELM_STYLE_DIR]] ? " - read HELM_STYLE_DIR - if test "x$HELM_STYLE_DIR" = "x"; then - HELM_STYLE_DIR=$DEFAULT_HELM_STYLE_DIR - fi -elif test $USE_DEFAULTS = yes; then - HELM_DTD_DIR=$DEFAULT_HELM_DTD_DIR - HELM_STYLE_DIR=$DEFAULT_HELM_STYLE_DIR -fi - -AC_SUBST(PACKAGE) -AC_SUBST(VERSION) -AC_SUBST(HELM_DTD_DIR) -AC_SUBST(HELM_STYLE_DIR) - -AC_OUTPUT([ - Makefile - helm_data.spec -]) - diff --git a/helm/helm_data/helm_data.spec.in b/helm/helm_data/helm_data.spec.in deleted file mode 100644 index 387a06f4b..000000000 --- a/helm/helm_data/helm_data.spec.in +++ /dev/null @@ -1,34 +0,0 @@ -Summary: The base DTDs and XSLT stylesheets of project HELM -Name: @PACKAGE@ -Version: @VERSION@ -Release: 1 -Copyright: GPL -URL: http://www.cs.unibo.it/helm -Packager: Claudio Sacerdoti Coen -Requires: helm_configuration >= 0.0.2 -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 base DTDs and XSLT stylesheets developed by the members of project -HELM. -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/share/helm/dtd -/usr/local/share/helm/style diff --git a/helm/helmpot/.cvsignore b/helm/helmpot/.cvsignore deleted file mode 100644 index d6cea24b1..000000000 --- a/helm/helmpot/.cvsignore +++ /dev/null @@ -1,18 +0,0 @@ -.emacs.desktop -config.h -config.h.in -config.cache -config.log -config.status -configure -configure.scan -t1lib.log -stamp-h -stamp-h.in -Makefile -Makefile.in -*.gz -aclocal.m4 -*.spec -.deps -helmpot diff --git a/helm/helmpot/AUTHORS b/helm/helmpot/AUTHORS deleted file mode 100644 index fe59f14d6..000000000 --- a/helm/helmpot/AUTHORS +++ /dev/null @@ -1 +0,0 @@ -Luca Padovani diff --git a/helm/helmpot/ChangeLog b/helm/helmpot/ChangeLog deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/helmpot/LICENSE b/helm/helmpot/LICENSE deleted file mode 100644 index eef8774f4..000000000 --- a/helm/helmpot/LICENSE +++ /dev/null @@ -1,23 +0,0 @@ -/* - * Copyright (C) 2000, Luca Padovani . - * - * This file is part of HelmPot, a minimal browser for HELM. - * - * HelmPot 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. - * - * HelmPot 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 HelmPot; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, see the HelmPot World-Wide-Web page, - * http://cs.unibo.it/helm/helmview, or send a mail to - * - */ diff --git a/helm/helmpot/Makefile.am b/helm/helmpot/Makefile.am deleted file mode 100644 index d730de386..000000000 --- a/helm/helmpot/Makefile.am +++ /dev/null @@ -1,26 +0,0 @@ - -CLEANFILES = core t1lib.log helmpot.spec - -bin_PROGRAMS = helmpot - -noinst_HEADERS = guiGTK.h - -helmpot_SOURCES = \ - main.c \ - guiGTK.c - -backup: - tar cvfz ../@PACKAGE@-@VERSION@-`date|tr ' ' '_'|tr ':' '_'`.tar.gz . - -cleanbak: - -rm -f `find . -name "*~"` - -lc: - @( \ - CFILES=`find . -name "*.c"`; \ - HFILES=`find . -name "*.h"`; \ - wc -l $$CFILES $$HFILES | tail -n 1 \ - ) - -INCLUDES = $(GTK_CFLAGS) - diff --git a/helm/helmpot/NEWS b/helm/helmpot/NEWS deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/helmpot/README b/helm/helmpot/README deleted file mode 100644 index 2e7cb0da0..000000000 --- a/helm/helmpot/README +++ /dev/null @@ -1,18 +0,0 @@ - -HELMPoT -------- - -HELMPoT is a small plug-out for Netscape Navigator in order to -browse the HELM library. After installing the binary somewhere -in your hard disk, just configure a new helper application in -Netscape associated to the text/xml MIME type. The command -to be executed should something of the kind: - - helmpot '%s' - -assuming that helmpot is visible in your path. - -Enjoy, - - luca.padovani@cs.unibo.it - diff --git a/helm/helmpot/acconfig.h b/helm/helmpot/acconfig.h deleted file mode 100644 index b65cd2c64..000000000 --- a/helm/helmpot/acconfig.h +++ /dev/null @@ -1,47 +0,0 @@ -/* - * Copyright (C) 2000, Luca Padovani . - * - * This file is part of HelmPot, a minimal browser for HELM. - * - * HelmPot 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. - * - * HelmPot 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 HelmPot; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, see the HelmPot World-Wide-Web page, - * http://cs.unibo.it/helm/helmview, or send a mail to - * - */ - -#ifndef __config_h__ -#define __config_h__ - -#define PRIVATE static - -@TOP@ - -/* If defined the widget will perform a huge amount - * of validity checks while running - */ -#undef ENABLE_CHECKS - -#ifdef ENABLE_CHECKS -#define DEBUG -#else -#define NDEBUG -#define G_DISABLE_ASSERT -#define G_DISABLE_CHECKS -#endif - -@BOTTOM@ - -#endif /* __config_h__ */ diff --git a/helm/helmpot/configure.in b/helm/helmpot/configure.in deleted file mode 100644 index 3d31a0d54..000000000 --- a/helm/helmpot/configure.in +++ /dev/null @@ -1,70 +0,0 @@ -dnl Process this file with autoconf to produce a configure script. -AC_INIT(main.c) - -HELMPOT_MAJOR_VERSION=0 -HELMPOT_MINOR_VERSION=1 -HELMPOT_MICRO_VERSION=0 -HELMPOT_VERSION=$HELMPOT_MAJOR_VERSION.$HELMPOT_MINOR_VERSION.$HELMPOT_MICRO_VERSION -VERSION=$HELMPOT_VERSION - -AC_SUBST(HELMPOT_VERSION) - -AC_ARG_ENABLE( - checks, - [ --enable-checks[=ARG] include debugging checks [default=yes]], - [ - if test $enableval = yes; then - AC_DEFINE(ENABLE_CHECKS) - fi - ], - AC_DEFINE(ENABLE_CHECKS) -) - -dnl Automake configuration -AM_CONFIG_HEADER(config.h) -AM_INIT_AUTOMAKE(helmpot, $HELMPOT_VERSION) - -dnl Checks for programs. -AC_LANG_C -AC_PROG_CC -AC_ISC_POSIX -AC_CHECK_PROG(HAVE_COLORGCC, colorgcc, yes, no) - -dnl Checks for header files. -AC_HEADER_STDC -AC_CHECK_HEADERS(unistd.h) -AC_FUNC_VFORK - -dnl Checks for typedefs, structures, and compiler characteristics. -AC_C_CONST - -dnl Check for iconv with const pointer as second argument -AC_LANG_C - -dnl Checks for libraries -AM_PATH_GTK(1.2.0, gtklib="yes", gtklib="no") - -if test $gtklib = "no"; then - AC_MSG_ERROR(GTK is needed in order to use helmpot) -fi - -CFLAGS="$CFLAGS @GTKMATHVIEW_CFLAGS@" -CXXFLAGS="$CXXFLAGS @GTKMATHVIEW_CFLAGS@" -LIBS="$LIBS @GTKMATHVIEW_LIBS@" - -PKG_CHECK_MODULES(GTKMATHVIEW, gtkmathview >= 0.3.0,, AC_MSG_ERROR(could not find gtkmathview)) -AC_SUBST(GTKMATHVIEW_CFLAGS) -AC_SUBST(GTKMATHVIEW_LIBS) - -if test $HAVE_COLORGCC = "yes"; then - CC=colorgcc - CXX=colorgcc -fi - -CFLAGS="$CFLAGS -W -Wall" -CXXFLAGS="$CXXFLAGS -W -Wall" - -AC_OUTPUT([ -Makefile -helmpot.spec -]) diff --git a/helm/helmpot/debian/changelog b/helm/helmpot/debian/changelog deleted file mode 100644 index 32467c728..000000000 --- a/helm/helmpot/debian/changelog +++ /dev/null @@ -1,42 +0,0 @@ -helmpot (0.1.0-2) unstable; urgency=low - - * debian/control - - bumped standards-version to 3.5.10 - - bumped dependency on debhelper to 4.0.0 - - added ${misc:Depends} - - added build dep on pkg-config - - -- Stefano Zacchiroli Wed, 25 Jun 2003 18:20:33 +0200 - -helmpot (0.1.0-1) unstable; urgency=low - - * New release. - - -- Stefano Zacchiroli Sat, 11 May 2002 11:52:35 +0200 - -helmpot (0.0.4-1) unstable; urgency=low - - * New release. - - -- Stefano Zacchiroli Wed, 14 Nov 2001 14:48:17 +0100 - -helmpot (0.0.3-1) unstable; urgency=low - - * Bug fix related to selection - -- Claudio Sacerdoti Coen Fri, 05 Oct 2001 19:40:06 +0200 - -helmpot (0.0.2-1) unstable; urgency=low - - * Small bug fix related to maction - - -- Claudio Sacerdoti Coen Mon, 27 Aug 2001 19:00:00 +0200 - -helmpot (0.0.1-1) unstable; urgency=low - - * Initial Release. - - -- Luca Padovani Thu, 12 Apr 2001 17:18:05 +0200 - -Local variables: -mode: debian-changelog -End: diff --git a/helm/helmpot/debian/control b/helm/helmpot/debian/control deleted file mode 100644 index 5deb9e0b4..000000000 --- a/helm/helmpot/debian/control +++ /dev/null @@ -1,14 +0,0 @@ -Source: helmpot -Section: misc -Priority: optional -Maintainer: Stefano Zacchiroli -Build-Depends: debhelper (>> 4.0.0), libgtkmathview-dev, pkg-config -Standards-Version: 3.5.10 - -Package: helmpot -Architecture: any -Depends: ${shlibs:Depends}, ${misc:Depends} -Description: A minimal browser for the HELM library. - 'helmpot' is a minimal browser, in the form of a plug-out, for - browsing the HELM library (MathML presentation). - diff --git a/helm/helmpot/debian/copyright b/helm/helmpot/debian/copyright deleted file mode 100644 index e2472b069..000000000 --- a/helm/helmpot/debian/copyright +++ /dev/null @@ -1,30 +0,0 @@ -This package was debianized by Luca Padovani on -Thu, 12 Apr 2001 17:18:05 +0200. - -It was packed from source obtained via cvs, with this CVSROOT: - :pserver:anonymous@phd.cs.unibo.it:/home/lpadovan/PHELM/ - -Author: Luca Padovani - -Copyright: - Copyright (C) 2000, Luca Padovani . - - This file is part of HelmPot, a minimal browser for HELM. - - HelmPot 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. - - HelmPot 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 HelmPot; if not, write to the Free Software - Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - - For details, see the HelmPot World-Wide-Web page, - http://cs.unibo.it/helm/helmpot, or send a mail to - diff --git a/helm/helmpot/debian/docs b/helm/helmpot/debian/docs deleted file mode 100644 index 6f12db508..000000000 --- a/helm/helmpot/debian/docs +++ /dev/null @@ -1,2 +0,0 @@ -AUTHORS -README diff --git a/helm/helmpot/debian/rules b/helm/helmpot/debian/rules deleted file mode 100755 index 75b3d8af5..000000000 --- a/helm/helmpot/debian/rules +++ /dev/null @@ -1,75 +0,0 @@ -#!/usr/bin/make -f -# Sample debian/rules that uses debhelper. -# GNU copyright 1997 to 1999 by Joey Hess. - -# Uncomment this to turn on verbose mode. -#export DH_VERBOSE=1 - -# This is the debhelper compatability version to use. -export DH_COMPAT=2 - -build: build-stamp -build-stamp: - dh_testdir - - ./configure --prefix=/usr --mandir=\$${prefix}/share/man --infodir=\$${prefix}/share/info - # Add here commands to compile the package. - $(MAKE) - - touch build-stamp - -clean: - dh_testdir - dh_testroot - rm -f build-stamp - - # Add here commands to clean up after the build process. - -$(MAKE) distclean - - dh_clean - -install: build - dh_testdir - dh_testroot - dh_clean -k - dh_installdirs - - # Add here commands to install the package into debian/tmp. - $(MAKE) install prefix=$(CURDIR)/debian/helmpot/usr - - -# Build architecture-independent files here. -binary-indep: build install -# We have nothing to do by default. - -# Build architecture-dependent files here. -binary-arch: build install - dh_testdir - dh_testroot -# dh_installdebconf - dh_installdocs -# dh_installexamples -# dh_installmenu -# dh_installemacsen -# dh_installpam -# dh_installinit -# dh_installcron -# dh_installmanpages - dh_installinfo - dh_undocumented - dh_installchangelogs ChangeLog - dh_link - dh_strip - dh_compress - dh_fixperms - # You may want to make some executables suid here. -# dh_makeshlibs - dh_installdeb -# dh_perl - dh_shlibdeps - dh_gencontrol - dh_md5sums - dh_builddeb - -binary: binary-indep binary-arch -.PHONY: build clean binary-indep binary-arch binary install diff --git a/helm/helmpot/guiGTK.c b/helm/helmpot/guiGTK.c deleted file mode 100644 index 906daf2b6..000000000 --- a/helm/helmpot/guiGTK.c +++ /dev/null @@ -1,684 +0,0 @@ -/* - * Copyright (C) 2000-2002, Luca Padovani . - * - * This file is part of HelmPot, a minimal browser for HELM. - * - * HelmPot 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. - * - * HelmPot 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 HelmPot; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, see the HelmPot World-Wide-Web page, - * http://cs.unibo.it/helm/helmview, or send a mail to - * - */ - -#include - -#include -#include -#include -#include -#if HAVE_UNISTD_H -# include -# include -# include -# include -#endif -#include -#include - -#include "gtkmathview.h" -#include "guiGTK.h" - -#define XLINK_NS_URI "http://www.w3.org/1999/xlink" - -#define pot_width 16 -#define pot_height 16 -PRIVATE unsigned char pot_bits[] = { - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x01, 0xc0, 0x07, - 0x00, 0x00, 0xe6, 0x2f, 0x34, 0x5f, 0xdc, 0x5f, 0xf8, 0x3f, 0xf8, 0x3f, - 0xf0, 0x1f, 0xe0, 0x0f, 0x00, 0x00, 0x00, 0x00}; - -#define pot_mask_width 16 -#define pot_mask_height 16 -static unsigned char pot_mask_bits[] = { - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x80, 0x03, 0xe0, 0x0f, 0xe0, 0x0f, - 0xff, 0x7f, 0xff, 0xff, 0xff, 0xff, 0xfe, 0xff, 0xfe, 0xff, 0xfc, 0x7f, - 0xfc, 0x7f, 0xf8, 0x3f, 0xf0, 0x1f, 0x00, 0x00}; - -PRIVATE GtkWidget* window; -PRIVATE GtkWidget* main_area; -PRIVATE GtkWidget* scrolled_area; -PRIVATE GtkWidget* status_bar; -PRIVATE GtkMenuItem* kerning_item; -PRIVATE GtkMenuItem* anti_aliasing_item; -PRIVATE GtkMenuItem* font_size_item; -PRIVATE gchar* file_name = NULL; - -PRIVATE GdkCursor* normal_cursor; -PRIVATE GdkCursor* link_cursor; -PRIVATE GdkCursor* pot_cursor; - -PRIVATE gboolean loading = FALSE; -PRIVATE guint statusbar_context; - -PRIVATE void create_widget_set(void); -PRIVATE GtkWidget* get_main_menu(void); -PRIVATE void options_font_size(GtkWidget*, guint); -PRIVATE void options_font_manager(GtkWidget*, guint); -PRIVATE void options_verbosity(GtkWidget*, guint); -PRIVATE void options_kerning(GtkWidget*, gpointer); -PRIVATE void options_anti_aliasing(GtkWidget*, gpointer); -PRIVATE void help_about(GtkWidget*, gpointer); -PRIVATE void save_as(GtkWidget*); -PRIVATE void export_to_ps(GtkWidget*); - -PRIVATE GtkItemFactoryEntry menu_items[] = { - { "/_File", NULL, NULL, 0, "" }, - { "/File/Save _As...", NULL, save_as, 0, NULL }, - { "/File/_Export to PostScript...", NULL, export_to_ps, 0, NULL }, - { "/File/sep1", NULL, NULL, 0, "" }, - { "/File/_Quit", "Q", gtk_main_quit, 0, NULL }, - - { "/_Options", NULL, NULL, 0, "" }, - { "/Options/Default _Font Size", NULL, NULL, 0, "" }, - { "/Options/Default Font Size/8pt", NULL, options_font_size, 8, "" }, - { "/Options/Default Font Size/10pt", NULL, options_font_size, 10, "/Options/Default Font Size/8pt" }, - { "/Options/Default Font Size/12pt", NULL, options_font_size, 12, "/Options/Default Font Size/8pt" }, - { "/Options/Default Font Size/14pt", NULL, options_font_size, 14, "/Options/Default Font Size/8pt" }, - { "/Options/Default Font Size/18pt", NULL, options_font_size, 18, "/Options/Default Font Size/8pt" }, - { "/Options/Default Font Size/24pt", NULL, options_font_size, 24, "/Options/Default Font Size/8pt" }, - { "/Options/Font Manager", NULL, NULL, 0, "" }, - { "/Options/Font Manager/_GTK", NULL, options_font_manager, 0, "" }, - { "/Options/Font Manager/_Type 1", NULL, options_font_manager, 1, "/Options/Font Manager/GTK" }, - { "/Options/Verbosity", NULL, NULL, 0, "" }, - { "/Options/Verbosity/_Errors", NULL, options_verbosity, 0, "" }, - { "/Options/Verbosity/_Warnings", NULL, options_verbosity, 1, "/Options/Verbosity/Errors" }, - { "/Options/Verbosity/_Info", NULL, options_verbosity, 2, "/Options/Verbosity/Errors" }, - { "/Options/Verbosity/_Debug", NULL, options_verbosity, 3, "/Options/Verbosity/Errors" }, - { "/Options/sep1", NULL, NULL, 0, "" }, - { "/Options/_Kerning", NULL, options_kerning, 0, "" }, - { "/Options/_Anti Aliasing", NULL, options_anti_aliasing, 0, "" }, - - { "/_Help" , NULL, NULL, 0, "" }, - { "/Help/About...", NULL, help_about, 0, NULL } -}; - -PRIVATE void -quick_message(const gchar* msg) -{ - GtkWidget* dialog; - GtkWidget* label; - GtkWidget* okay_button; - - /* Create the widgets */ - - dialog = gtk_dialog_new(); - label = gtk_label_new (msg); - okay_button = gtk_button_new_with_label("OK"); - - gtk_widget_set_usize(dialog, 300, 100); - - /* Ensure that the dialog box is destroyed when the user clicks ok. */ - - gtk_signal_connect_object (GTK_OBJECT (okay_button), "clicked", - GTK_SIGNAL_FUNC (gtk_widget_destroy), GTK_OBJECT(dialog)); - gtk_container_add (GTK_CONTAINER (GTK_DIALOG(dialog)->action_area), - okay_button); - - /* Add the label, and show everything we've added to the dialog. */ - - gtk_container_add (GTK_CONTAINER (GTK_DIALOG(dialog)->vbox), label); - gtk_widget_show_all (dialog); -} - -PRIVATE void -load_error_msg(const gchar* name) -{ - gchar* msg = g_strdup_printf("Could not load\n`%s'", name); - quick_message(msg); - g_free(msg); -} - -PRIVATE void -save_error_msg(const gchar* name) -{ - gchar* msg = g_strdup_printf("Could not save\n`%s'", name); - quick_message(msg); - g_free(msg); -} - -void -GUI_init(gint* argc, gchar*** argv, gchar* title, guint width, guint height, GtkFunction f, guint32 timeout) -{ - GdkPixmap* source; - GdkPixmap* mask; - - GdkColor fg = { 0, 65535, 65535, 65535 }; - GdkColor bg = { 0, 0, 0, 0 }; - - gtk_init(argc, argv); - - window = gtk_window_new(GTK_WINDOW_TOPLEVEL); - gtk_window_set_title(GTK_WINDOW(window), title); - gtk_window_set_default_size(GTK_WINDOW(window), width, height); - gtk_signal_connect(GTK_OBJECT(window), "delete_event", (GtkSignalFunc) gtk_main_quit, NULL); - create_widget_set(); - - gtk_widget_show(window); - - gtk_timeout_add(timeout, f, NULL); - - normal_cursor = gdk_cursor_new(GDK_TOP_LEFT_ARROW); - link_cursor = gdk_cursor_new(GDK_HAND2); - - source = gdk_bitmap_create_from_data (NULL, pot_bits, - pot_width, pot_height); - mask = gdk_bitmap_create_from_data (NULL, pot_mask_bits, - pot_mask_width, pot_mask_height); - pot_cursor = gdk_cursor_new_from_pixmap (source, mask, &fg, &bg, 8, 8); - gdk_pixmap_unref (source); - gdk_pixmap_unref (mask); -} - -void -GUI_uninit() -{ -} - -int -GUI_load_document(const gchar* name) -{ - GtkMathView* math_view; - GtkMathViewClass* klass; - gboolean res; - - g_return_val_if_fail(name != NULL, -1); - g_return_val_if_fail(main_area != NULL, -1); - g_return_val_if_fail(GTK_IS_MATH_VIEW(main_area), -1); - - math_view = GTK_MATH_VIEW(main_area); - g_return_val_if_fail(math_view != NULL, -1); - - klass = (GtkMathViewClass*) gtk_type_class(gtk_math_view_get_type()); - g_return_val_if_fail(klass != NULL, -1); - - res = gtk_math_view_load(math_view, name); - gdk_window_set_cursor(main_area->window, normal_cursor); - loading = FALSE; - - if (!res) { - load_error_msg(name); - return -1; - } - - gtk_statusbar_pop(GTK_STATUSBAR(status_bar), statusbar_context); - if (strlen(name) > 40) name += strlen(name) - 40; - gtk_statusbar_push(GTK_STATUSBAR(status_bar), statusbar_context, name); - - if (file_name != NULL) g_free(file_name); - file_name = g_strdup(name); - - return 0; -} - -void -GUI_unload_document() -{ - GtkMathView* math_view; - - g_return_if_fail(main_area != NULL); - g_return_if_fail(GTK_IS_MATH_VIEW(main_area)); - - math_view = GTK_MATH_VIEW(main_area); - - gtk_math_view_unload(math_view); -} - -void -GUI_run() -{ - gtk_main(); -} - -PRIVATE void -options_font_size(GtkWidget* widget, guint size) -{ - GtkMathView* math_view; - - g_return_if_fail(main_area != NULL); - g_return_if_fail(GTK_IS_MATH_VIEW(main_area)); - - math_view = GTK_MATH_VIEW(main_area); - - gtk_math_view_set_font_size(math_view, size); -} - -PRIVATE void -options_font_manager(GtkWidget* widget, guint id) -{ - GtkMathView* math_view; - - g_return_if_fail(main_area != NULL); - g_return_if_fail(GTK_IS_MATH_VIEW(main_area)); - - math_view = GTK_MATH_VIEW(main_area); - - gtk_math_view_set_font_manager_type(math_view, id); -} - -PRIVATE void -options_anti_aliasing(GtkWidget* widget, gpointer data) -{ - gboolean aa = gtk_math_view_get_anti_aliasing(GTK_MATH_VIEW(main_area)); - gtk_math_view_set_anti_aliasing(GTK_MATH_VIEW(main_area), !aa); -} - -PRIVATE void -options_kerning(GtkWidget* widget, gpointer data) -{ - gboolean k = gtk_math_view_get_kerning(GTK_MATH_VIEW(main_area)); - gtk_math_view_set_kerning(GTK_MATH_VIEW(main_area), !k); -} - -PRIVATE void -options_verbosity(GtkWidget* widget, guint level) -{ - gtk_math_view_set_log_verbosity(GTK_MATH_VIEW(main_area), level); -} - -PRIVATE void -help_about(GtkWidget* widget, gpointer data) -{ - GtkWidget* dialog; - GtkWidget* label; - GtkWidget* ok; - - dialog = gtk_dialog_new(); - label = gtk_label_new("\n HELM PoT \n Copyright (C) 2001-2002 Luca Padovani \n"); - ok = gtk_button_new_with_label("Close"); - - gtk_signal_connect_object (GTK_OBJECT (ok), "clicked", - GTK_SIGNAL_FUNC (gtk_widget_destroy), (gpointer) dialog); - gtk_container_add (GTK_CONTAINER (GTK_DIALOG(dialog)->action_area), - ok); - - gtk_container_add (GTK_CONTAINER (GTK_DIALOG(dialog)->vbox), label); - - gtk_widget_show_all (dialog); -} - -PRIVATE void -export_filename(GtkFileSelection* selector, gpointer user_data) -{ - FILE* f; - GtkMathView* math_view; - gchar* selected_filename; - - selected_filename = gtk_file_selection_get_filename (GTK_FILE_SELECTION(user_data)); - - math_view = GTK_MATH_VIEW(main_area); - - f = fopen(selected_filename, "wt"); - if (f == NULL) { - save_error_msg(selected_filename); - /*g_free(selected_filename);*/ - return; - } - - gtk_math_view_export_to_postscript(math_view, - (21 * SCALED_POINTS_PER_CM) / SCALED_POINTS_PER_PX, - (29 * SCALED_POINTS_PER_CM) / SCALED_POINTS_PER_PX, - SCALED_POINTS_PER_IN / SCALED_POINTS_PER_PX, - SCALED_POINTS_PER_IN / SCALED_POINTS_PER_PX, - FALSE, - f); - - fclose(f); - /*g_free(selected_filename);*/ -} - -PRIVATE void -save_filename(GtkFileSelection* selector, gpointer user_data) -{ - FILE* source; - FILE* dest; - gchar* buffer; - gchar* selected_filename; - - if (file_name == NULL) return; - - source = fopen(file_name, "rt"); - if (source == NULL) { - load_error_msg(file_name); - return; - } - - selected_filename = gtk_file_selection_get_filename (GTK_FILE_SELECTION(user_data)); - if (selected_filename == NULL) return; - - dest = fopen(selected_filename, "wt"); - if (dest == NULL) { - save_error_msg(selected_filename); - /*g_free(selected_filename);*/ - return; - } - - /*g_free(selected_filename);*/ - - buffer = g_new(gchar, 2048); - while (!feof(source)) { - size_t n = fread(buffer, sizeof(gchar), 2048, source); - fwrite(buffer, sizeof(gchar), n, dest); - } - - g_free(buffer); - fclose(source); - fclose(dest); -} - -PRIVATE void -file_dialog(const gchar* title, GtkSignalFunc f) -{ - GtkWidget* fs; - - g_return_if_fail(title != NULL); - g_return_if_fail(f != NULL); - - fs = gtk_file_selection_new(title); - - gtk_signal_connect (GTK_OBJECT (GTK_FILE_SELECTION(fs)->ok_button), - "clicked", f, fs); - - /* Ensure that the dialog box is destroyed when the user clicks a button. */ - - gtk_signal_connect_object (GTK_OBJECT (GTK_FILE_SELECTION(fs)->ok_button), - "clicked", GTK_SIGNAL_FUNC (gtk_widget_destroy), - (gpointer) fs); - - gtk_signal_connect_object (GTK_OBJECT (GTK_FILE_SELECTION(fs)->cancel_button), - "clicked", GTK_SIGNAL_FUNC (gtk_widget_destroy), - (gpointer) fs); - - /* Display that dialog */ - - gtk_widget_show (fs); -} - -PRIVATE void -export_to_ps(GtkWidget* widget) -{ - file_dialog("Export to PostScript", export_filename); -#if 0 - static GList* items = NULL; - - GtkWidget* dialog; - GtkWidget* tmp; - - if (items == NULL) { - items = g_list_append(items, "A4"); - items = g_list_append(items, "A5"); - } - - dialog = gtk_dialog_new(); - tmp = gtk_label_new("Paper size"); - gtk_container_add(GTK_CONTAINER(GTK_DIALOG(dialog)->vbox), tmp); - tmp = gtk_combo_new(); - gtk_combo_set_popdown_strings(GTK_COMBO(tmp), items); - gtk_container_add(GTK_CONTAINER(GTK_DIALOG(dialog)->vbox), tmp); -#if 0 - tmp = gtk_check_button_new_with_label("Disable Colors"); - gtk_container_add(GTK_CONTAINER(GTK_DIALOG(dialog)->vbox), tmp); -#endif - - tmp = gtk_button_new_with_label("OK"); - gtk_signal_connect_object(GTK_OBJECT(tmp), "clicked", GTK_SIGNAL_FUNC(export_to_ps_get_file_name), dialog); - gtk_signal_connect_object(GTK_OBJECT(tmp), "clicked", GTK_SIGNAL_FUNC(gtk_widget_destroy), dialog); - gtk_container_add(GTK_CONTAINER(GTK_DIALOG(dialog)->action_area), tmp); - tmp = gtk_button_new_with_label("Cancel"); - gtk_signal_connect_object(GTK_OBJECT(tmp), "clicked", GTK_SIGNAL_FUNC(gtk_widget_destroy), dialog); - gtk_container_add(GTK_CONTAINER(GTK_DIALOG(dialog)->action_area), tmp); - - gtk_widget_show_all(dialog); -#endif -} - -PRIVATE void -save_as(GtkWidget* widget) -{ - file_dialog("Save As...", save_filename); -} - -PRIVATE void -element_changed(GtkMathView* math_view, GdomeElement* elem) -{ - g_return_if_fail(math_view != NULL); - g_return_if_fail(main_area != NULL); - g_return_if_fail(GTK_IS_MATH_VIEW(math_view)); - /* fprintf(stderr, "node changed: %p %s\n", node, (node != NULL) ? mdom_node_get_name(node) : "-"); */ - - if (!loading) { - GdomeException exc = 0; - GdomeDOMString* namespaceURI = gdome_str_mkref(XLINK_NS_URI); - GdomeDOMString* localName = gdome_str_mkref("href"); - - if (elem != NULL) { - gdome_el_ref(elem, &exc); - g_assert(exc == 0); - } - - while (elem != NULL && !gdome_el_hasAttributeNS(elem, namespaceURI, localName, &exc)) { - GdomeElement* parent = gdome_cast_el(gdome_el_parentNode(elem, &exc)); - g_assert(exc == 0); - gdome_el_unref(elem, &exc); - g_assert(exc == 0); - elem = parent; - } - g_assert(exc == 0); - - gdome_str_unref(namespaceURI); - gdome_str_unref(localName); - - if (elem != NULL) { - gdome_el_unref(elem, &exc); - g_assert(exc == 0); - gdk_window_set_cursor(main_area->window, link_cursor); - } else - gdk_window_set_cursor(main_area->window, normal_cursor); - } -} - -PRIVATE void -selection_changed(GtkMathView* math_view, GdomeElement* elem) -{ - GdomeException exc = 0; - GdomeDOMString* localName = gdome_str_mkref("xref"); - - g_return_if_fail(math_view != NULL); - g_return_if_fail(GTK_IS_MATH_VIEW(math_view)); - - if (elem != NULL) { - gdome_el_ref(elem, &exc); - g_assert(exc == 0); - } - - while (elem != NULL && !gdome_el_hasAttribute(elem, localName, &exc)) { - GdomeElement* parent = gdome_cast_el(gdome_el_parentNode(elem, &exc)); - g_assert(exc == 0); - gdome_el_unref(elem, &exc); - g_assert(exc == 0); - elem = parent; - } - - gdome_str_unref(localName); - - gtk_math_view_set_selection(math_view, elem); - if (elem != NULL) { - gdome_el_unref(elem, &exc); - g_assert(exc == 0); - } -} - -PRIVATE void -jump(GdomeDOMString* href) -{ - pid_t pid; - g_return_if_fail(href != NULL); - - gdk_window_set_cursor(main_area->window, pot_cursor); - loading = TRUE; - pid = fork(); - if (pid == -1) exit(-1); - if (pid == 0) { - gchar* open_url = g_strdup_printf("openURL(%s,cic)", href->str); - gint fd; - - close(0); - close(1); - close(2); - - fd = open("/dev/null", O_RDWR); - dup(fd); - dup(fd); - - execlp("netscape", "netscape", "-noraise", "-remote", open_url, NULL); - perror("exec failed:"); - exit(-1); - } -} - -PRIVATE void -clicked(GtkMathView* math_view, gpointer user_data) -{ - GdomeException exc = 0; - GdomeDOMString* namespaceURI = gdome_str_mkref(XLINK_NS_URI); - GdomeDOMString* localName = gdome_str_mkref("href"); - - GdomeElement* p = gtk_math_view_get_element(math_view); - while (p != NULL && !gdome_el_hasAttributeNS(p, namespaceURI, localName, &exc)) { - GdomeElement* parent = gdome_cast_el(gdome_el_parentNode(p, &exc)); - g_assert(exc == 0); - gdome_el_unref(p, &exc); - g_assert(exc == 0); - p = parent; - } - g_assert(exc == 0); - - if (p != NULL) { - GdomeDOMString* href = gdome_el_getAttributeNS(p, namespaceURI, localName, &exc); - g_assert(exc == 0); - g_assert(href != NULL); - - jump(href); - gdome_str_unref(href); - gdome_el_unref(p, &exc); - g_assert(exc == 0); - } else { - p = gtk_math_view_get_action(math_view); - if (p != NULL) { - gtk_math_view_action_toggle(math_view); - gdome_el_unref(p, &exc); - g_assert(exc == 0); - } - } - - gdome_str_unref(namespaceURI); - gdome_str_unref(localName); -} - -PRIVATE void -create_widget_set() -{ - GtkWidget* main_vbox; - GtkWidget* menu_bar; - - main_vbox = gtk_vbox_new(FALSE, 1); - gtk_container_border_width(GTK_CONTAINER(main_vbox), 1); - gtk_container_add(GTK_CONTAINER(window), main_vbox); - gtk_widget_show(main_vbox); - - menu_bar = get_main_menu(); - gtk_box_pack_start(GTK_BOX(main_vbox), menu_bar, FALSE, TRUE, 0); - gtk_widget_show(menu_bar); - - main_area = gtk_math_view_new(NULL, NULL); - gtk_widget_show(main_area); - - gtk_signal_connect_object (GTK_OBJECT (main_area), - "element_changed", GTK_SIGNAL_FUNC (element_changed), - (gpointer) main_area); - - gtk_signal_connect_object (GTK_OBJECT (main_area), - "selection_changed", GTK_SIGNAL_FUNC (selection_changed), - (gpointer) main_area); - - gtk_signal_connect_object (GTK_OBJECT (main_area), - "clicked", GTK_SIGNAL_FUNC(clicked), - (gpointer) main_area); - - scrolled_area = gtk_scrolled_window_new(NULL, NULL); - gtk_scrolled_window_set_policy(GTK_SCROLLED_WINDOW(scrolled_area), - GTK_POLICY_AUTOMATIC, GTK_POLICY_ALWAYS); - gtk_widget_show(scrolled_area); - gtk_container_add(GTK_CONTAINER(scrolled_area), main_area); - gtk_box_pack_start(GTK_BOX(main_vbox), scrolled_area, TRUE, TRUE, 0); - - status_bar = gtk_statusbar_new(); - gtk_widget_show(status_bar); - gtk_box_pack_start(GTK_BOX(main_vbox), status_bar, FALSE, TRUE, 0); - statusbar_context = gtk_statusbar_get_context_id(GTK_STATUSBAR(status_bar), "filename"); - - gtk_widget_show(main_vbox); - - if (gtk_math_view_get_anti_aliasing(GTK_MATH_VIEW(main_area))) - gtk_menu_item_activate(anti_aliasing_item); - - if (gtk_math_view_get_kerning(GTK_MATH_VIEW(main_area))) - gtk_menu_item_activate(kerning_item); - - gtk_math_view_set_font_size(GTK_MATH_VIEW(main_area), DEFAULT_FONT_SIZE); - gtk_menu_item_activate(font_size_item); -} - -GtkWidget* -get_main_menu() -{ - GtkItemFactory* item_factory; - GtkAccelGroup* accel_group; - GtkWidget* menu_item; - - gint nmenu_items = sizeof(menu_items) / sizeof(menu_items[0]); - - accel_group = gtk_accel_group_new(); - - item_factory = gtk_item_factory_new(GTK_TYPE_MENU_BAR, "
", accel_group); - - gtk_item_factory_create_items(item_factory, nmenu_items, menu_items, NULL); - - gtk_window_add_accel_group(GTK_WINDOW(window), accel_group); - - menu_item = gtk_item_factory_get_widget(item_factory, "/Options/Kerning"); - kerning_item = GTK_MENU_ITEM(menu_item); - - menu_item = gtk_item_factory_get_widget(item_factory, "/Options/Anti Aliasing"); - anti_aliasing_item = GTK_MENU_ITEM(menu_item); - - /* !!!BEWARE!!! the default font size must be kept aligned with the definition - * in defs.h - */ - menu_item = gtk_item_factory_get_widget(item_factory, "/Options/Default Font Size/14pt"); - font_size_item = GTK_MENU_ITEM(menu_item); - - return gtk_item_factory_get_widget(item_factory, "
"); -} - diff --git a/helm/helmpot/guiGTK.h b/helm/helmpot/guiGTK.h deleted file mode 100644 index 83f5f866a..000000000 --- a/helm/helmpot/guiGTK.h +++ /dev/null @@ -1,50 +0,0 @@ -/* - * Copyright (C) 2000, Luca Padovani . - * - * This file is part of HelmPot, a minimal browser for HELM. - * - * HelmPot 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. - * - * HelmPot 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 HelmPot; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, see the HelmPot World-Wide-Web page, - * http://cs.unibo.it/helm/helmview, or send a mail to - * - */ - -#ifndef __guiGTK_h__ -#define __guiGTK_h__ - -#include -#include - -#ifdef __cplusplus -extern "C" { -#endif - - /* initGUI: some initialization stuff, creates the main window, sets it with a title */ - void GUI_init(gint *, gchar ***, gchar *, guint, guint, GtkFunction, guint32); - void GUI_uninit(void); - - int GUI_load_document(const gchar*); - void GUI_unload_document(void); - void GUI_dump_entities(void); - - /* main: this is the main event loop, to be called when the program is ready to run */ - void GUI_run(void); - -#ifdef __cplusplus -} -#endif - -#endif /* __guiGTK_h__ */ diff --git a/helm/helmpot/helmpot.spec.in b/helm/helmpot/helmpot.spec.in deleted file mode 100644 index 641f1849f..000000000 --- a/helm/helmpot/helmpot.spec.in +++ /dev/null @@ -1,24 +0,0 @@ -Summary: A minimal browser for the HELM library -Name: @PACKAGE@ -Version: @VERSION@ -Release: 1 -Copyright: GPL -Group: Development/Libraries -Source: www.cs.unibo.it:/helm/helmpot/@PACKAGE@-@VERSION@.tar.gz -%description -HelmView is a minimal browser for the HELM library. - -%prep -%setup - -%build -./configure -make - -%install -make install - -%files -%doc AUTHORS COPYING ChangeLog INSTALL LICENSE NEWS README TODO - -/usr/local/bin/@PACKAGE@ diff --git a/helm/helmpot/main.c b/helm/helmpot/main.c deleted file mode 100644 index c2abc2d7e..000000000 --- a/helm/helmpot/main.c +++ /dev/null @@ -1,121 +0,0 @@ -/* - * Copyright (C) 2000-2002, Luca Padovani . - * - * This file is part of HelmPot, a minimal browser for HELM. - * - * HelmPot 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. - * - * HelmPot 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 HelmPot; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, see the HelmPot World-Wide-Web page, - * http://cs.unibo.it/helm/helmpot, or send a mail to - * - */ - -#include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include "defs.h" -#include "guiGTK.h" - -#define BUFFER_SIZE 2048 - -PRIVATE gchar app_name[64]; -PRIVATE gint sockfd; -PRIVATE struct sockaddr_in address; - -PRIVATE void -error(const gchar* msg) -{ - g_assert(msg != NULL); - fprintf(stderr, "%s: fatal error: %s\n", app_name, msg); -} - -#if 0 -PRIVATE void -print_version() -{ - printf("%s - written by Luca Padovani (C) 2000.\n", app_name); -#ifdef DEBUG - printf("Compiled %s %s\n", __DATE__, __TIME__); -#endif - exit(0); -} -#endif - -PRIVATE gboolean -timeout(gpointer user_data) -{ - static gchar file_name[BUFFER_SIZE]; - - if (recv(sockfd, file_name, BUFFER_SIZE, 0) < 0) { - if (errno != EAGAIN && errno != EWOULDBLOCK) - error("error receving message"); - } else - GUI_load_document(file_name); - - return TRUE; -} - -int -main(int argc, char *argv[]) -{ - sprintf(app_name, "HELM Pot (Plug-OuT) v%s", VERSION); - - if (argc != 2) { - fprintf(stderr, "%s\n\n", app_name); - fprintf(stderr, "Usage: helmpot URL\n"); - exit(-1); - } - - sockfd = socket(PF_INET, SOCK_DGRAM, 0); - if (sockfd < 0) error("could not create socket"); - - if (inet_aton("127.0.0.1", &address.sin_addr) < 0) - error("could not create address"); - address.sin_port = 8778; - address.sin_family = PF_INET; - - if (bind(sockfd, &address, sizeof(address)) < 0) { - if (sendto(sockfd, argv[1], strlen(argv[1]), 0, &address, sizeof(address)) < 0) - error("could not send message"); - sleep(1); - exit(0); - } - - if (fcntl(sockfd, F_SETFL, O_NONBLOCK) < 0) - error("could not set the socket to non-block mode"); - - GUI_init(&argc, &argv, app_name, 500, 600, timeout, 500); - - GUI_load_document(argv[1]); - - GUI_run(); - GUI_uninit(); - GUI_unload_document(); - - return 0; -} diff --git a/helm/helmpot/pot_mask b/helm/helmpot/pot_mask deleted file mode 100644 index 09f71a6a9..000000000 --- a/helm/helmpot/pot_mask +++ /dev/null @@ -1,6 +0,0 @@ -#define pot_mask_width 16 -#define pot_mask_height 16 -static unsigned char pot_mask_bits[] = { - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x80, 0x03, 0xe0, 0x0f, 0xe0, 0x0f, - 0xff, 0x7f, 0xff, 0xff, 0xff, 0xff, 0xfe, 0xff, 0xfe, 0xff, 0xfc, 0x7f, - 0xfc, 0x7f, 0xf8, 0x3f, 0xf0, 0x1f, 0x00, 0x00}; diff --git a/helm/http_getter/COPYING b/helm/http_getter/COPYING deleted file mode 100644 index d60c31a97..000000000 --- a/helm/http_getter/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/graphs/jsmenu/HM_Arrays.js b/helm/software/daemons/graphs/jsmenu/HM_Arrays.js similarity index 100% rename from helm/graphs/jsmenu/HM_Arrays.js rename to helm/software/daemons/graphs/jsmenu/HM_Arrays.js diff --git a/helm/graphs/jsmenu/HM_Arrays_prova.js b/helm/software/daemons/graphs/jsmenu/HM_Arrays_prova.js similarity index 100% rename from helm/graphs/jsmenu/HM_Arrays_prova.js rename to helm/software/daemons/graphs/jsmenu/HM_Arrays_prova.js diff --git a/helm/graphs/jsmenu/HM_Loader.js b/helm/software/daemons/graphs/jsmenu/HM_Loader.js similarity index 100% rename from helm/graphs/jsmenu/HM_Loader.js rename to helm/software/daemons/graphs/jsmenu/HM_Loader.js diff --git a/helm/graphs/jsmenu/HM_Loader_prova.js b/helm/software/daemons/graphs/jsmenu/HM_Loader_prova.js similarity index 100% rename from helm/graphs/jsmenu/HM_Loader_prova.js rename to helm/software/daemons/graphs/jsmenu/HM_Loader_prova.js diff --git a/helm/graphs/jsmenu/HM_More_black_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_black_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_black_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_black_left.gif diff --git a/helm/graphs/jsmenu/HM_More_black_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_black_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_black_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_black_right.gif diff --git a/helm/graphs/jsmenu/HM_More_blue_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_blue_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_blue_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_blue_left.gif diff --git a/helm/graphs/jsmenu/HM_More_blue_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_blue_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_blue_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_blue_right.gif diff --git a/helm/graphs/jsmenu/HM_More_cyan_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_cyan_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_cyan_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_cyan_left.gif diff --git a/helm/graphs/jsmenu/HM_More_cyan_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_cyan_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_cyan_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_cyan_right.gif diff --git a/helm/graphs/jsmenu/HM_More_green_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_green_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_green_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_green_left.gif diff --git a/helm/graphs/jsmenu/HM_More_green_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_green_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_green_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_green_right.gif diff --git a/helm/graphs/jsmenu/HM_More_magenta_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_magenta_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_magenta_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_magenta_left.gif diff --git a/helm/graphs/jsmenu/HM_More_magenta_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_magenta_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_magenta_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_magenta_right.gif diff --git a/helm/graphs/jsmenu/HM_More_red_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_red_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_red_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_red_left.gif diff --git a/helm/graphs/jsmenu/HM_More_red_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_red_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_red_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_red_right.gif diff --git a/helm/graphs/jsmenu/HM_More_white_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_white_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_white_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_white_left.gif diff --git a/helm/graphs/jsmenu/HM_More_white_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_white_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_white_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_white_right.gif diff --git a/helm/graphs/jsmenu/HM_More_yellow_left.gif b/helm/software/daemons/graphs/jsmenu/HM_More_yellow_left.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_yellow_left.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_yellow_left.gif diff --git a/helm/graphs/jsmenu/HM_More_yellow_right.gif b/helm/software/daemons/graphs/jsmenu/HM_More_yellow_right.gif similarity index 100% rename from helm/graphs/jsmenu/HM_More_yellow_right.gif rename to helm/software/daemons/graphs/jsmenu/HM_More_yellow_right.gif diff --git a/helm/graphs/jsmenu/HM_ScriptDOM.js b/helm/software/daemons/graphs/jsmenu/HM_ScriptDOM.js similarity index 100% rename from helm/graphs/jsmenu/HM_ScriptDOM.js rename to helm/software/daemons/graphs/jsmenu/HM_ScriptDOM.js diff --git a/helm/graphs/jsmenu/HM_ScriptIE4.js b/helm/software/daemons/graphs/jsmenu/HM_ScriptIE4.js similarity index 100% rename from helm/graphs/jsmenu/HM_ScriptIE4.js rename to helm/software/daemons/graphs/jsmenu/HM_ScriptIE4.js diff --git a/helm/graphs/jsmenu/HM_ScriptNS4.js b/helm/software/daemons/graphs/jsmenu/HM_ScriptNS4.js similarity index 100% rename from helm/graphs/jsmenu/HM_ScriptNS4.js rename to helm/software/daemons/graphs/jsmenu/HM_ScriptNS4.js diff --git a/helm/graphs/jsmenu/LoadMe.html b/helm/software/daemons/graphs/jsmenu/LoadMe.html similarity index 100% rename from helm/graphs/jsmenu/LoadMe.html rename to helm/software/daemons/graphs/jsmenu/LoadMe.html diff --git a/helm/graphs/jsmenu/prova.gif b/helm/software/daemons/graphs/jsmenu/prova.gif similarity index 100% rename from helm/graphs/jsmenu/prova.gif rename to helm/software/daemons/graphs/jsmenu/prova.gif diff --git a/helm/graphs/jsmenu/prova.html b/helm/software/daemons/graphs/jsmenu/prova.html similarity index 100% rename from helm/graphs/jsmenu/prova.html rename to helm/software/daemons/graphs/jsmenu/prova.html diff --git a/helm/graphs/tools/.cvsignore b/helm/software/daemons/graphs/tools/.cvsignore similarity index 100% rename from helm/graphs/tools/.cvsignore rename to helm/software/daemons/graphs/tools/.cvsignore diff --git a/helm/graphs/tools/Makefile b/helm/software/daemons/graphs/tools/Makefile similarity index 100% rename from helm/graphs/tools/Makefile rename to helm/software/daemons/graphs/tools/Makefile diff --git a/helm/graphs/tools/drawGraph.conf.xml.sample b/helm/software/daemons/graphs/tools/drawGraph.conf.xml.sample similarity index 100% rename from helm/graphs/tools/drawGraph.conf.xml.sample rename to helm/software/daemons/graphs/tools/drawGraph.conf.xml.sample diff --git a/helm/graphs/tools/drawGraph.ml b/helm/software/daemons/graphs/tools/drawGraph.ml similarity index 100% rename from helm/graphs/tools/drawGraph.ml rename to helm/software/daemons/graphs/tools/drawGraph.ml diff --git a/helm/graphs/tools/mk_html.pl b/helm/software/daemons/graphs/tools/mk_html.pl similarity index 100% rename from helm/graphs/tools/mk_html.pl rename to helm/software/daemons/graphs/tools/mk_html.pl diff --git a/helm/graphs/tools/simplify_deps/.cvsignore b/helm/software/daemons/graphs/tools/simplify_deps/.cvsignore similarity index 100% rename from helm/graphs/tools/simplify_deps/.cvsignore rename to helm/software/daemons/graphs/tools/simplify_deps/.cvsignore diff --git a/helm/graphs/tools/simplify_deps/Makefile b/helm/software/daemons/graphs/tools/simplify_deps/Makefile similarity index 100% rename from helm/graphs/tools/simplify_deps/Makefile rename to helm/software/daemons/graphs/tools/simplify_deps/Makefile diff --git a/helm/graphs/tools/simplify_deps/simplify_deps.ml b/helm/software/daemons/graphs/tools/simplify_deps/simplify_deps.ml similarity index 100% rename from helm/graphs/tools/simplify_deps/simplify_deps.ml rename to helm/software/daemons/graphs/tools/simplify_deps/simplify_deps.ml diff --git a/helm/graphs/tools/uriSetQueue.conf.xml.sample b/helm/software/daemons/graphs/tools/uriSetQueue.conf.xml.sample similarity index 100% rename from helm/graphs/tools/uriSetQueue.conf.xml.sample rename to helm/software/daemons/graphs/tools/uriSetQueue.conf.xml.sample diff --git a/helm/graphs/tools/uriSetQueue.ml b/helm/software/daemons/graphs/tools/uriSetQueue.ml similarity index 100% rename from helm/graphs/tools/uriSetQueue.ml rename to helm/software/daemons/graphs/tools/uriSetQueue.ml diff --git a/helm/http_getter/.cvsignore b/helm/software/daemons/http_getter/.cvsignore similarity index 100% rename from helm/http_getter/.cvsignore rename to helm/software/daemons/http_getter/.cvsignore diff --git a/helm/http_getter/AUTHORS b/helm/software/daemons/http_getter/AUTHORS similarity index 100% rename from helm/http_getter/AUTHORS rename to helm/software/daemons/http_getter/AUTHORS diff --git a/helm/http_getter/BUGS b/helm/software/daemons/http_getter/BUGS similarity index 100% rename from helm/http_getter/BUGS rename to helm/software/daemons/http_getter/BUGS diff --git a/helm/helm_data/COPYING b/helm/software/daemons/http_getter/COPYING similarity index 100% rename from helm/helm_data/COPYING rename to helm/software/daemons/http_getter/COPYING diff --git a/helm/http_getter/ChangeLog b/helm/software/daemons/http_getter/ChangeLog similarity index 100% rename from helm/http_getter/ChangeLog rename to helm/software/daemons/http_getter/ChangeLog diff --git a/helm/http_getter/Makefile b/helm/software/daemons/http_getter/Makefile similarity index 100% rename from helm/http_getter/Makefile rename to helm/software/daemons/http_getter/Makefile diff --git a/helm/http_getter/Makefile.overrides b/helm/software/daemons/http_getter/Makefile.overrides similarity index 100% rename from helm/http_getter/Makefile.overrides rename to helm/software/daemons/http_getter/Makefile.overrides diff --git a/helm/http_getter/NEWS b/helm/software/daemons/http_getter/NEWS similarity index 100% rename from helm/http_getter/NEWS rename to helm/software/daemons/http_getter/NEWS diff --git a/helm/http_getter/README b/helm/software/daemons/http_getter/README similarity index 100% rename from helm/http_getter/README rename to helm/software/daemons/http_getter/README diff --git a/helm/http_getter/buildTimeOpts.ml.in b/helm/software/daemons/http_getter/buildTimeOpts.ml.in similarity index 100% rename from helm/http_getter/buildTimeOpts.ml.in rename to helm/software/daemons/http_getter/buildTimeOpts.ml.in diff --git a/helm/http_getter/configure.ac b/helm/software/daemons/http_getter/configure.ac similarity index 100% rename from helm/http_getter/configure.ac rename to helm/software/daemons/http_getter/configure.ac diff --git a/helm/http_getter/http_getter.conf.xml.sample b/helm/software/daemons/http_getter/http_getter.conf.xml.sample similarity index 100% rename from helm/http_getter/http_getter.conf.xml.sample rename to helm/software/daemons/http_getter/http_getter.conf.xml.sample diff --git a/helm/http_getter/main.ml b/helm/software/daemons/http_getter/main.ml similarity index 100% rename from helm/http_getter/main.ml rename to helm/software/daemons/http_getter/main.ml diff --git a/helm/http_getter/panel/.cvsignore b/helm/software/daemons/http_getter/panel/.cvsignore similarity index 100% rename from helm/http_getter/panel/.cvsignore rename to helm/software/daemons/http_getter/panel/.cvsignore diff --git a/helm/http_getter/panel/Makefile b/helm/software/daemons/http_getter/panel/Makefile similarity index 100% rename from helm/http_getter/panel/Makefile rename to helm/software/daemons/http_getter/panel/Makefile diff --git a/helm/http_getter/panel/control.html b/helm/software/daemons/http_getter/panel/control.html similarity index 100% rename from helm/http_getter/panel/control.html rename to helm/software/daemons/http_getter/panel/control.html diff --git a/helm/http_getter/panel/control.js b/helm/software/daemons/http_getter/panel/control.js similarity index 100% rename from helm/http_getter/panel/control.js rename to helm/software/daemons/http_getter/panel/control.js diff --git a/helm/DEVEL/profile-manager/index.html b/helm/software/daemons/http_getter/panel/index.html similarity index 100% rename from helm/DEVEL/profile-manager/index.html rename to helm/software/daemons/http_getter/panel/index.html diff --git a/helm/DEVEL/profile-manager/welcome.html b/helm/software/daemons/http_getter/panel/welcome.html similarity index 100% rename from helm/DEVEL/profile-manager/welcome.html rename to helm/software/daemons/http_getter/panel/welcome.html diff --git a/helm/http_getter/tools/dump_db.ml b/helm/software/daemons/http_getter/tools/dump_db.ml similarity index 100% rename from helm/http_getter/tools/dump_db.ml rename to helm/software/daemons/http_getter/tools/dump_db.ml diff --git a/helm/http_getter/tools/dump_db.pl b/helm/software/daemons/http_getter/tools/dump_db.pl similarity index 100% rename from helm/http_getter/tools/dump_db.pl rename to helm/software/daemons/http_getter/tools/dump_db.pl diff --git a/helm/http_getter/tools/uri_escape.pl b/helm/software/daemons/http_getter/tools/uri_escape.pl similarity index 100% rename from helm/http_getter/tools/uri_escape.pl rename to helm/software/daemons/http_getter/tools/uri_escape.pl diff --git a/helm/http_getter/tools/uri_unescape.pl b/helm/software/daemons/http_getter/tools/uri_unescape.pl similarity index 100% rename from helm/http_getter/tools/uri_unescape.pl rename to helm/software/daemons/http_getter/tools/uri_unescape.pl diff --git a/helm/proofChecker/.cvsignore b/helm/software/daemons/proofChecker/.cvsignore similarity index 100% rename from helm/proofChecker/.cvsignore rename to helm/software/daemons/proofChecker/.cvsignore diff --git a/helm/proofChecker/.depend b/helm/software/daemons/proofChecker/.depend similarity index 100% rename from helm/proofChecker/.depend rename to helm/software/daemons/proofChecker/.depend diff --git a/helm/proofChecker/Makefile b/helm/software/daemons/proofChecker/Makefile similarity index 100% rename from helm/proofChecker/Makefile rename to helm/software/daemons/proofChecker/Makefile diff --git a/helm/proofChecker/proofChecker.conf.xml.sample b/helm/software/daemons/proofChecker/proofChecker.conf.xml.sample similarity index 100% rename from helm/proofChecker/proofChecker.conf.xml.sample rename to helm/software/daemons/proofChecker/proofChecker.conf.xml.sample diff --git a/helm/proofChecker/proofChecker.ml b/helm/software/daemons/proofChecker/proofChecker.ml similarity index 100% rename from helm/proofChecker/proofChecker.ml rename to helm/software/daemons/proofChecker/proofChecker.ml diff --git a/helm/DEVEL/rdfly/.cvsignore b/helm/software/daemons/rdfly/.cvsignore similarity index 100% rename from helm/DEVEL/rdfly/.cvsignore rename to helm/software/daemons/rdfly/.cvsignore diff --git a/helm/DEVEL/rdfly/Makefile b/helm/software/daemons/rdfly/Makefile similarity index 100% rename from helm/DEVEL/rdfly/Makefile rename to helm/software/daemons/rdfly/Makefile diff --git a/helm/DEVEL/rdfly/rdfly.conf.xml.sample b/helm/software/daemons/rdfly/rdfly.conf.xml.sample similarity index 100% rename from helm/DEVEL/rdfly/rdfly.conf.xml.sample rename to helm/software/daemons/rdfly/rdfly.conf.xml.sample diff --git a/helm/DEVEL/rdfly/rdfly.ml b/helm/software/daemons/rdfly/rdfly.ml similarity index 100% rename from helm/DEVEL/rdfly/rdfly.ml rename to helm/software/daemons/rdfly/rdfly.ml diff --git a/helm/uwobo/.cvsignore b/helm/software/daemons/uwobo/.cvsignore similarity index 100% rename from helm/uwobo/.cvsignore rename to helm/software/daemons/uwobo/.cvsignore diff --git a/helm/uwobo/.depend b/helm/software/daemons/uwobo/.depend similarity index 100% rename from helm/uwobo/.depend rename to helm/software/daemons/uwobo/.depend diff --git a/helm/uwobo/Makefile b/helm/software/daemons/uwobo/Makefile similarity index 100% rename from helm/uwobo/Makefile rename to helm/software/daemons/uwobo/Makefile diff --git a/helm/uwobo/doc/uwobo.tex b/helm/software/daemons/uwobo/doc/uwobo.tex similarity index 100% rename from helm/uwobo/doc/uwobo.tex rename to helm/software/daemons/uwobo/doc/uwobo.tex diff --git a/helm/uwobo/log/.cvsignore b/helm/software/daemons/uwobo/log/.cvsignore similarity index 100% rename from helm/uwobo/log/.cvsignore rename to helm/software/daemons/uwobo/log/.cvsignore diff --git a/helm/uwobo-panel/.cvsignore b/helm/software/daemons/uwobo/panel/.cvsignore similarity index 100% rename from helm/uwobo-panel/.cvsignore rename to helm/software/daemons/uwobo/panel/.cvsignore diff --git a/helm/uwobo-panel/Makefile b/helm/software/daemons/uwobo/panel/Makefile similarity index 100% rename from helm/uwobo-panel/Makefile rename to helm/software/daemons/uwobo/panel/Makefile diff --git a/helm/uwobo-panel/control.html b/helm/software/daemons/uwobo/panel/control.html similarity index 100% rename from helm/uwobo-panel/control.html rename to helm/software/daemons/uwobo/panel/control.html diff --git a/helm/uwobo-panel/control.js b/helm/software/daemons/uwobo/panel/control.js similarity index 100% rename from helm/uwobo-panel/control.js rename to helm/software/daemons/uwobo/panel/control.js diff --git a/helm/http_getter/panel/index.html b/helm/software/daemons/uwobo/panel/index.html similarity index 100% rename from helm/http_getter/panel/index.html rename to helm/software/daemons/uwobo/panel/index.html diff --git a/helm/http_getter/panel/welcome.html b/helm/software/daemons/uwobo/panel/welcome.html similarity index 100% rename from helm/http_getter/panel/welcome.html rename to helm/software/daemons/uwobo/panel/welcome.html diff --git a/helm/uwobo/uwobo.conf.xml.sample b/helm/software/daemons/uwobo/uwobo.conf.xml.sample similarity index 100% rename from helm/uwobo/uwobo.conf.xml.sample rename to helm/software/daemons/uwobo/uwobo.conf.xml.sample diff --git a/helm/uwobo/uwobo.ml b/helm/software/daemons/uwobo/uwobo.ml similarity index 100% rename from helm/uwobo/uwobo.ml rename to helm/software/daemons/uwobo/uwobo.ml diff --git a/helm/uwobo/uwobo_common.ml b/helm/software/daemons/uwobo/uwobo_common.ml similarity index 100% rename from helm/uwobo/uwobo_common.ml rename to helm/software/daemons/uwobo/uwobo_common.ml diff --git a/helm/uwobo/uwobo_common.mli b/helm/software/daemons/uwobo/uwobo_common.mli similarity index 100% rename from helm/uwobo/uwobo_common.mli rename to helm/software/daemons/uwobo/uwobo_common.mli diff --git a/helm/uwobo/uwobo_engine.ml b/helm/software/daemons/uwobo/uwobo_engine.ml similarity index 100% rename from helm/uwobo/uwobo_engine.ml rename to helm/software/daemons/uwobo/uwobo_engine.ml diff --git a/helm/uwobo/uwobo_engine.mli b/helm/software/daemons/uwobo/uwobo_engine.mli similarity index 100% rename from helm/uwobo/uwobo_engine.mli rename to helm/software/daemons/uwobo/uwobo_engine.mli diff --git a/helm/uwobo/uwobo_logger.ml b/helm/software/daemons/uwobo/uwobo_logger.ml similarity index 100% rename from helm/uwobo/uwobo_logger.ml rename to helm/software/daemons/uwobo/uwobo_logger.ml diff --git a/helm/uwobo/uwobo_logger.mli b/helm/software/daemons/uwobo/uwobo_logger.mli similarity index 100% rename from helm/uwobo/uwobo_logger.mli rename to helm/software/daemons/uwobo/uwobo_logger.mli diff --git a/helm/uwobo/uwobo_profiles.ml b/helm/software/daemons/uwobo/uwobo_profiles.ml similarity index 100% rename from helm/uwobo/uwobo_profiles.ml rename to helm/software/daemons/uwobo/uwobo_profiles.ml diff --git a/helm/uwobo/uwobo_profiles.mli b/helm/software/daemons/uwobo/uwobo_profiles.mli similarity index 100% rename from helm/uwobo/uwobo_profiles.mli rename to helm/software/daemons/uwobo/uwobo_profiles.mli diff --git a/helm/uwobo/uwobo_styles.ml b/helm/software/daemons/uwobo/uwobo_styles.ml similarity index 100% rename from helm/uwobo/uwobo_styles.ml rename to helm/software/daemons/uwobo/uwobo_styles.ml diff --git a/helm/uwobo/uwobo_styles.mli b/helm/software/daemons/uwobo/uwobo_styles.mli similarity index 100% rename from helm/uwobo/uwobo_styles.mli rename to helm/software/daemons/uwobo/uwobo_styles.mli diff --git a/helm/searchEngine/.cvsignore b/helm/software/daemons/whelp/.cvsignore similarity index 100% rename from helm/searchEngine/.cvsignore rename to helm/software/daemons/whelp/.cvsignore diff --git a/helm/searchEngine/.depend b/helm/software/daemons/whelp/.depend similarity index 100% rename from helm/searchEngine/.depend rename to helm/software/daemons/whelp/.depend diff --git a/helm/searchEngine/Makefile b/helm/software/daemons/whelp/Makefile similarity index 100% rename from helm/searchEngine/Makefile rename to helm/software/daemons/whelp/Makefile diff --git a/helm/searchEngine/html/Makefile b/helm/software/daemons/whelp/html/Makefile similarity index 100% rename from helm/searchEngine/html/Makefile rename to helm/software/daemons/whelp/html/Makefile diff --git a/helm/searchEngine/html/includes.xsl b/helm/software/daemons/whelp/html/includes.xsl similarity index 100% rename from helm/searchEngine/html/includes.xsl rename to helm/software/daemons/whelp/html/includes.xsl diff --git a/helm/searchEngine/html/manual/alias.jpg b/helm/software/daemons/whelp/html/manual/alias.jpg similarity index 100% rename from helm/searchEngine/html/manual/alias.jpg rename to helm/software/daemons/whelp/html/manual/alias.jpg diff --git a/helm/searchEngine/html/manual/ex1.jpg b/helm/software/daemons/whelp/html/manual/ex1.jpg similarity index 100% rename from helm/searchEngine/html/manual/ex1.jpg rename to helm/software/daemons/whelp/html/manual/ex1.jpg diff --git a/helm/searchEngine/html/manual/frames.jpg b/helm/software/daemons/whelp/html/manual/frames.jpg similarity index 100% rename from helm/searchEngine/html/manual/frames.jpg rename to helm/software/daemons/whelp/html/manual/frames.jpg diff --git a/helm/searchEngine/html/manual/index.html b/helm/software/daemons/whelp/html/manual/index.html similarity index 100% rename from helm/searchEngine/html/manual/index.html rename to helm/software/daemons/whelp/html/manual/index.html diff --git a/helm/searchEngine/html/moogle.html.src b/helm/software/daemons/whelp/html/moogle.html.src similarity index 100% rename from helm/searchEngine/html/moogle.html.src rename to helm/software/daemons/whelp/html/moogle.html.src diff --git a/helm/searchEngine/html/moogle.png b/helm/software/daemons/whelp/html/moogle.png similarity index 100% rename from helm/searchEngine/html/moogle.png rename to helm/software/daemons/whelp/html/moogle.png diff --git a/helm/searchEngine/html/moogle_chat.html.src b/helm/software/daemons/whelp/html/moogle_chat.html.src similarity index 100% rename from helm/searchEngine/html/moogle_chat.html.src rename to helm/software/daemons/whelp/html/moogle_chat.html.src diff --git a/helm/searchEngine/html/moogle_form.html.src b/helm/software/daemons/whelp/html/moogle_form.html.src similarity index 100% rename from helm/searchEngine/html/moogle_form.html.src rename to helm/software/daemons/whelp/html/moogle_form.html.src diff --git a/helm/searchEngine/html/moogle_header.html.src b/helm/software/daemons/whelp/html/moogle_header.html.src similarity index 100% rename from helm/searchEngine/html/moogle_header.html.src rename to helm/software/daemons/whelp/html/moogle_header.html.src diff --git a/helm/searchEngine/html/moogle_help.html b/helm/software/daemons/whelp/html/moogle_help.html similarity index 100% rename from helm/searchEngine/html/moogle_help.html rename to helm/software/daemons/whelp/html/moogle_help.html diff --git a/helm/searchEngine/html/moogle_init.html b/helm/software/daemons/whelp/html/moogle_init.html similarity index 100% rename from helm/searchEngine/html/moogle_init.html rename to helm/software/daemons/whelp/html/moogle_init.html diff --git a/helm/searchEngine/html/moogle_querybar.html.src b/helm/software/daemons/whelp/html/moogle_querybar.html.src similarity index 100% rename from helm/searchEngine/html/moogle_querybar.html.src rename to helm/software/daemons/whelp/html/moogle_querybar.html.src diff --git a/helm/searchEngine/html/moogle_small.png b/helm/software/daemons/whelp/html/moogle_small.png similarity index 100% rename from helm/searchEngine/html/moogle_small.png rename to helm/software/daemons/whelp/html/moogle_small.png diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/software/daemons/whelp/html/moogle_syntax.html similarity index 100% rename from helm/searchEngine/html/moogle_syntax.html rename to helm/software/daemons/whelp/html/moogle_syntax.html diff --git a/helm/searchEngine/html/moogle_trailer.html.src b/helm/software/daemons/whelp/html/moogle_trailer.html.src similarity index 100% rename from helm/searchEngine/html/moogle_trailer.html.src rename to helm/software/daemons/whelp/html/moogle_trailer.html.src diff --git a/helm/searchEngine/html/whelp.png b/helm/software/daemons/whelp/html/whelp.png similarity index 100% rename from helm/searchEngine/html/whelp.png rename to helm/software/daemons/whelp/html/whelp.png diff --git a/helm/searchEngine/html/whelp.svg b/helm/software/daemons/whelp/html/whelp.svg similarity index 100% rename from helm/searchEngine/html/whelp.svg rename to helm/software/daemons/whelp/html/whelp.svg diff --git a/helm/searchEngine/html/whelp_small.png b/helm/software/daemons/whelp/html/whelp_small.png similarity index 100% rename from helm/searchEngine/html/whelp_small.png rename to helm/software/daemons/whelp/html/whelp_small.png diff --git a/helm/searchEngine/mooglePp.ml b/helm/software/daemons/whelp/mooglePp.ml similarity index 100% rename from helm/searchEngine/mooglePp.ml rename to helm/software/daemons/whelp/mooglePp.ml diff --git a/helm/searchEngine/mooglePp.mli b/helm/software/daemons/whelp/mooglePp.mli similarity index 100% rename from helm/searchEngine/mooglePp.mli rename to helm/software/daemons/whelp/mooglePp.mli diff --git a/helm/searchEngine/preloaded_uris.txt b/helm/software/daemons/whelp/preloaded_uris.txt similarity index 100% rename from helm/searchEngine/preloaded_uris.txt rename to helm/software/daemons/whelp/preloaded_uris.txt diff --git a/helm/searchEngine/searchEngine.conf.xml.sample b/helm/software/daemons/whelp/searchEngine.conf.xml.sample similarity index 100% rename from helm/searchEngine/searchEngine.conf.xml.sample rename to helm/software/daemons/whelp/searchEngine.conf.xml.sample diff --git a/helm/searchEngine/searchEngine.ml b/helm/software/daemons/whelp/searchEngine.ml similarity index 100% rename from helm/searchEngine/searchEngine.ml rename to helm/software/daemons/whelp/searchEngine.ml diff --git a/helm/uwobo-panel/index.html b/helm/uwobo-panel/index.html deleted file mode 100644 index caeebcf24..000000000 --- a/helm/uwobo-panel/index.html +++ /dev/null @@ -1,8 +0,0 @@ - - - - - - - - diff --git a/helm/uwobo-panel/welcome.html b/helm/uwobo-panel/welcome.html deleted file mode 100644 index f6fbed438..000000000 --- a/helm/uwobo-panel/welcome.html +++ /dev/null @@ -1,6 +0,0 @@ - - - - - - diff --git a/helm/xmltheory/Coq_v2theoryxml/.cvsignore b/helm/xmltheory/Coq_v2theoryxml/.cvsignore deleted file mode 100644 index e4a3d5419..000000000 --- a/helm/xmltheory/Coq_v2theoryxml/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -coq_v2theoryxml *.cmi *.cmo diff --git a/helm/xmltheory/Coq_v2theoryxml/.depend b/helm/xmltheory/Coq_v2theoryxml/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/xmltheory/Coq_v2theoryxml/Makefile b/helm/xmltheory/Coq_v2theoryxml/Makefile deleted file mode 100644 index 1f9fae538..000000000 --- a/helm/xmltheory/Coq_v2theoryxml/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -COQTOP=/home/projects/helm/EXPORT/V7 -OCAMLC=ocamlc -I $(COQTOP)/config -I $(COQTOP)/toplevel - -COQV2THEORYXMLOBJS= \ - $(COQTOP)/config/coq_config.cmo \ - $(COQTOP)/toplevel/usage.cmo \ - coq_v2theoryxml.cmo - -coq_v2theoryxml: $(COQV2THEORYXMLOBJS) - $(OCAMLC) -o $@ unix.cma $(COQV2THEORYXMLOBJS) - -coq_v2theoryxml.cmo: coq_v2theoryxml.ml - $(OCAMLC) -c $< - -.PHONY: clean -clean: - rm -f coq_v2theoryxml *.cmo *.cmi diff --git a/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml b/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml deleted file mode 100644 index b1e856e1a..000000000 --- a/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml +++ /dev/null @@ -1,176 +0,0 @@ -(* environment *) - -let environment = Unix.environment () - -let bindir = ref Coq_config.bindir -let binary = "coqtop.byte" -let image = ref "" -let xml_theory_library_root = ref ( - try - Sys.getenv "XML_THEORY_LIBRARY_ROOT" - with Not_found -> "" -) - -(* the $COQBIN environment variable has priority over the Coq_config value *) -let _ = - try - let c = Sys.getenv "COQBIN" in - if c <> "" then bindir := c - with Not_found -> () - -(* coq_v2theoryxml options *) - -let keep = ref false - -(* Verifies that a string do not contains others caracters than letters, - digits, or `_` *) - -let check_module_name s = - let err () = - output_string stderr - "Modules names must only contain letters, digits, or underscores\n"; - output_string stderr - "and must begin with a letter\n"; - exit 1 - in - match String.get s 0 with - | 'a' .. 'z' | 'A' .. 'Z' -> - for i = 1 to (String.length s)-1 do - match String.get s i with - | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> () - | _ -> err () - done - | _ -> err () - - (* compilation of a file [file] with command [command] and args [args] *) - -let compile command args file = - let dirname = Filename.dirname file in - let basename = Filename.basename file in - let modulename = - if Filename.check_suffix basename ".vo" then - Filename.chop_suffix basename ".vo" - else - basename - in - check_module_name modulename; - let tmpfile = Filename.temp_file "coq_v2theoryxml" ".v" in - let args' = - command :: "-batch" :: "-silent" :: "-is" :: "barestate" :: args - @ ["-load-vernac-source"; tmpfile] in - let devnull = - if Sys.os_type = "Unix" then - Unix.openfile "/dev/null" [] 0o777 - else - Unix.stdin - in - let oc = open_out tmpfile in - Printf.fprintf oc "Require XmlTheory.\n" ; - Printf.fprintf oc "XmlTheory Begin %s \"%s\".\n" modulename - !xml_theory_library_root ; - Printf.fprintf oc "Load %s.\n" modulename; - Printf.fprintf oc "XmlTheory End.\n" ; - flush oc; - close_out oc; - try - let pid = - Unix.create_process_env command - (Array.of_list args') environment devnull Unix.stdout Unix.stderr in - let status = Unix.waitpid [] pid in - if not !keep then Sys.remove tmpfile ; - match status with - | _, Unix.WEXITED 0 -> () - | _, Unix.WEXITED 127 -> - Printf.printf "Cannot execute %s\n" command; - exit 1 - | _, Unix.WEXITED c -> exit c - | _ -> exit 1 - with _ -> - if not !keep then Sys.remove tmpfile; exit 1 - -(* parsing of the command line - * - * special treatment for -bindir and -i. - * other options are passed to coqtop *) - -let usage () = - Usage.print_usage - "Usage: coq_v2theoryxml module...\n -options are: - -xml-theory-library-root d specify the path to the root of the XML library - (overrides $XML_THEORY_LIBRARY_ROOT) - -image f specify an alternative executable for Coq - -t keep temporary files\n\n" ; - flush stderr ; - exit 1 - -let parse_args () = - let rec parse (cfiles,args) = function - | [] -> - List.rev cfiles, List.rev args - | "-xml-theory-library-root" :: v :: rem -> - xml_theory_library_root := v ; parse (cfiles,args) rem - | "-t" :: rem -> - keep := true ; parse (cfiles,args) rem - | "-boot" :: rem -> - bindir:= Filename.concat Coq_config.coqtop "bin"; - parse (cfiles, "-boot"::args) rem - | "-bindir" :: d :: rem -> - bindir := d ; parse (cfiles,args) rem - | "-bindir" :: [] -> - usage () - | "-byte" :: rem -> - parse (cfiles,args) rem - | "-opt" :: rem -> - raise (Failure "To load ML modules, only -byte is allowed") - | "-image" :: f :: rem -> - image := f; parse (cfiles,args) rem - | "-image" :: [] -> - usage () - | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-libdir"|"-outputstate"|"-I"|"-include" - |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" - |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" - |"-init-file" as o) :: rem -> - begin - match rem with - | s :: rem' -> parse (cfiles,s::o::args) rem' - | [] -> usage () - end - | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem - | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" - |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m" as o) :: rem -> - parse (cfiles,o::args) rem - | ("-v"|"--version") :: _ -> - Usage.version () - | "-where" :: _ -> - print_endline Coq_config.coqlib; exit 0 - | f :: rem -> parse (f::cfiles,args) rem - in - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - -(* main: we parse the command line, define the command to compile files - * and then call the compilation on each file *) - -let main () = - let cfiles, args = parse_args () in - if cfiles = [] then begin - prerr_endline "coq_v2theoryxml: too few arguments" ; - usage () - end; - let coqtopname = - if !image <> "" then !image else Filename.concat !bindir (binary ^ Coq_config.exec_extension) - in - if !xml_theory_library_root = "" then - begin - prerr_endline "coq_v2theoryxml: you must either set $XML_THEORY_LIBRARY_ROOT or use -xml-theory-library-root"; - usage () - end - else - List.iter (compile coqtopname args) cfiles ; - prerr_endline - ("\nWARNING: all the URIs in the generated XML files are broken." ^ - "\n See the README in the XML contrib to learn how to fix them.\n") - -let _ = Printexc.print main (); exit 0 diff --git a/helm/xmltheory/FakeCoq_vo2xml/README b/helm/xmltheory/FakeCoq_vo2xml/README deleted file mode 100644 index 4accfcafc..000000000 --- a/helm/xmltheory/FakeCoq_vo2xml/README +++ /dev/null @@ -1,3 +0,0 @@ -# This coq_vo2xml must be put in PATH before the real coq_vo2xml. -# It's aim is to run coq_v2theoryxml instead of coq_vo2xml -# Remember to set $XML_THEORY_LIBRARY_ROOT before starting this coq_vo2xml diff --git a/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml b/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml deleted file mode 100755 index 34e44a0a4..000000000 --- a/helm/xmltheory/FakeCoq_vo2xml/coq_vo2xml +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash - -BASEDIR=/home/projects/helm/EXPORT/xmltheory -$BASEDIR/Coq_v2theoryxml/coq_v2theoryxml -R $BASEDIR/XmlTheory Bologna.XmlTheory $@ diff --git a/helm/xmltheory/XmlTheory/.cvsignore b/helm/xmltheory/XmlTheory/.cvsignore deleted file mode 100644 index 1921ec2e1..000000000 --- a/helm/xmltheory/XmlTheory/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cmi *.cmo *.vo diff --git a/helm/xmltheory/XmlTheory/.depend b/helm/xmltheory/XmlTheory/.depend deleted file mode 100644 index 2b814a941..000000000 --- a/helm/xmltheory/XmlTheory/.depend +++ /dev/null @@ -1,8 +0,0 @@ -xmltheoryentries.cmo: xmltheoryentries.ml iXml.cmi -xmltheoryentries.cmx: xmltheoryentries.ml iXml.cmx -iXml.cmo: iXml.ml iXml.cmi -iXml.cmx: iXml.ml iXml.cmi -iXml.cmi: iXml.mli -XmlTheory.vo: XmlTheory.v iXml.cmo xmltheoryentries.cmo -XmlTheory.vi: XmlTheory.v iXml.cmo xmltheoryentries.cmo -XmlTheory.html: XmlTheory.v iXml.cmo xmltheoryentries.cmo diff --git a/helm/xmltheory/XmlTheory/COME_COMPILARE b/helm/xmltheory/XmlTheory/COME_COMPILARE deleted file mode 100644 index f1389cc35..000000000 --- a/helm/xmltheory/XmlTheory/COME_COMPILARE +++ /dev/null @@ -1,5 +0,0 @@ -# Settare - -OPT=-byte # Nota: questo andrebbe fatto nel Make, ma un bug di coq_makefile - # lo impedisce -COQTOP=... diff --git a/helm/xmltheory/XmlTheory/Make b/helm/xmltheory/XmlTheory/Make deleted file mode 100644 index a927b6345..000000000 --- a/helm/xmltheory/XmlTheory/Make +++ /dev/null @@ -1,5 +0,0 @@ --R . Bologna.XmlTheory --I $(COQTOP)/contrib/xml -XmlTheory.v -iXml.ml -xmltheoryentries.ml diff --git a/helm/xmltheory/XmlTheory/Makefile b/helm/xmltheory/XmlTheory/Makefile deleted file mode 100644 index 1dc9d35c4..000000000 --- a/helm/xmltheory/XmlTheory/Makefile +++ /dev/null @@ -1,165 +0,0 @@ -############################################################################## -## The Calculus of Inductive Constructions ## -## ## -## Projet Coq ## -## ## -## INRIA ENS-CNRS ## -## Rocquencourt Lyon ## -## ## -## Coq V7 ## -## ## -## ## -############################################################################## - -# WARNING -# -# This Makefile has been automagically generated by coq_makefile -# Edit at your own risks ! -# -# END OF WARNING - -# -# This Makefile was generated by the command line : -# coq_makefile -f Make -o Makefile -# - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLP4LIB=`camlp4 -where` -MAKE=make "COQBIN=$(COQBIN)" "OPT=$(OPT)" -COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \ - -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \ - -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \ - -I $(COQTOP)/toplevel -I $(CAMLP4LIB) -ZFLAGS=$(OCAMLLIBS) $(COQSRC) -COQFLAGS=-q $(OPT) $(COQLIBS) -COQC=$(COQBIN)coqc -COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(COQLIBS) -GALLINA=gallina -COQ2HTML=coq2html -COQ2LATEX=coq2latex -CAMLC=ocamlc -c -CAMLOPTC=ocamlopt -c -CAMLLINK=ocamlc -CAMLOPTLINK=ocamlopt -COQDEP=$(COQBIN)coqdep -c -COQVO2XML=coq_vo2xml - -######################### -# # -# Libraries definition. # -# # -######################### - -OCAMLLIBS=-I .\ - -I $(COQTOP)/contrib/xml -COQLIBS=-I .\ - -R . Bologna.XmlTheory\ - -I $(COQTOP)/contrib/xml - -################################### -# # -# Definition of the "all" target. # -# # -################################### - -all: XmlTheory.vo\ - iXml.cmo\ - xmltheoryentries.cmo - -spec: XmlTheory.vi - -gallina: XmlTheory.g - -html: XmlTheory.html - -tex: XmlTheory.tex - -gallinatex: XmlTheory.g.tex - -gallinahtml: XmlTheory.g.html - -xml: .xml_time_stamp -.xml_time_stamp: XmlTheory.vo - $(COQVO2XML) $(COQFLAGS) $(?:%.o=%) - touch .xml_time_stamp - -#################### -# # -# Special targets. # -# # -#################### - -.PHONY: all opt byte archclean clean install depend xml - -.SUFFIXES: .mli .ml .cmo .cmi .cmx .v .vo .vi .g .html .tex .g.tex .g.html - -.mli.cmi: - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -.ml.cmo: - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -.ml.cmx: - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< - -.v.vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -.v.vi: - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -.v.g: - $(GALLINA) $< - -.v.html: - $(COQ2HTML) $< - -.v.tex: - $(COQ2LATEX) $< -latex -o $@ - -.v.g.html: - $(GALLINA) -stdout $< | $(COQ2HTML) -f > $@ - -.v.g.tex: - $(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@ - -byte: - $(MAKE) all "OPT=" - -opt: - $(MAKE) all "OPT=-opt" - -include .depend - -depend: - rm .depend - $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend - $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend - -install: - @if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi - cp -f *.vo $(TARGETDIR) - cp -f *.cmo $(TARGETDIR) - -Makefile: Make - mv -f Makefile Makefile.bak - $(COQBIN)coq_makefile -f Make -o Makefile - -clean: - rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~ - -archclean: - rm -f *.cmx *.o - -# WARNING -# -# This Makefile has been automagically generated by coq_makefile -# Edit at your own risks ! -# -# END OF WARNING - diff --git a/helm/xmltheory/XmlTheory/README b/helm/xmltheory/XmlTheory/README deleted file mode 100644 index ce4c86c98..000000000 --- a/helm/xmltheory/XmlTheory/README +++ /dev/null @@ -1,78 +0,0 @@ -Here we show the procedure to follow to add the recognition of -a new syntactical form. - -Form to recognize in the model: - -Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}. - -1. cd V7 ; grep "Lemma" */*.ml4 - the result should be one or a few files. In this case the - only file is parsing/g_vernac.ml4. In the case of many files, - only one is the good one. -2. open the file and search for Lemma: - thm_tok: - [ [ "Theorem" -> <:ast< "THEOREM" >> - | IDENT "Lemma" -> <:ast< "LEMMA" >> - | IDENT "Fact" -> <:ast< "FACT" >> - | IDENT "Remark" -> <:ast< "REMARK" >> - | IDENT "Decl" -> <:ast< "DECL" >> ] ] - - so a Lemma is mapped into an ast of phylum thm_tok. - Let's search for thm_tok. Many occurrences are found, - but the only one that matches the form to recognize is - - gallina: - (* Definition, Goal *) - [ [ thm = thm_tok; id = identarg; ":"; c = constrarg -> - <:ast< (StartProof $thm $id $c) >> - - So the ast created is tagged StartProof -3. grep "StartProof" */*.ml (usually toplevel/...) - Open the file and search for StartProof. - This is found: - let _ = - add "StartProof" - (function - | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] -> - ... -4. edit xmltheoryentries.ml and copy the entry for another rule, - substituting StartProof as the parameter for set_hook and - using the above match (with V. added where appropriate) after function: - -let module V = Vernacinterp in - set_hook "StartProof" - (function - [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] -> - ??? - | _ -> fail () - ) -;; - - Finally, write OCaml code to print to XML the availables interesting - infos. In our case the code becomes - -let module V = Vernacinterp in - set_hook "StartProof" - (function - [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] -> - IXml.output - (Xml.xml_empty - "THEOREM" - ["uri", Names.string_of_id s ^ ".con"; "as",kind] - ) - | _ -> fail () - ) -;; - - IXml.output should always be present and the code inside - (that is simply XML written in OCaml form) should be changed. - The syntax is - Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"] - to create an empty element name with attributes att1 ... attn. - To create a non-empty element, use - Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"] - stream - where stream is an OCaml stream of other XML elements, as: - * another Xml.xml_nempty - * an Xml.xml_empty - * [< stream1 ; ... ; streamk >] diff --git a/helm/xmltheory/XmlTheory/XmlTheory.v b/helm/xmltheory/XmlTheory/XmlTheory.v deleted file mode 100644 index 54fdf82e6..000000000 --- a/helm/xmltheory/XmlTheory/XmlTheory.v +++ /dev/null @@ -1,15 +0,0 @@ -Declare ML Module "iXml" "xmltheoryentries". - -(*Vecchio, ma funzionante -Grammar vernac vernac : ast := - xml_theory_begin [ "XmlTheory" "Begin" stringarg($s) stringarg($f) "." ] -> - [(XMLTHEORYBEGIN $s $f)] -| xml_theory_end [ "XmlTheory" "End" "." ] -> - [(XMLTHEORYEND)]. -*) - -Grammar vernac vernac : ast := - xml_theory_begin [ "XmlTheory" "Begin" identarg($s) stringarg($f) "." ] -> - [(XMLTHEORYBEGIN $s $f)] -| xml_theory_end [ "XmlTheory" "End" "." ] -> - [(XMLTHEORYEND)]. diff --git a/helm/xmltheory/XmlTheory/iXml.ml b/helm/xmltheory/XmlTheory/iXml.ml deleted file mode 100644 index 98fb186d8..000000000 --- a/helm/xmltheory/XmlTheory/iXml.ml +++ /dev/null @@ -1,53 +0,0 @@ -exception NoOpenNonEmptyElements - -type sectionTree = - Leaf of Xml.token Stream.t - | Node of string * (string * string) list * sectionTree list ref -;; - -let rec token_stream_of_section_tree_list = - function - he::tl -> - [< token_stream_of_section_tree_list tl; token_stream_of_section_tree he >] - | [] -> [<>] -and token_stream_of_section_tree = - function - Leaf t -> [< t >] - | Node (elem_name, attr_list, section_tree) -> - Xml.xml_nempty elem_name attr_list - (token_stream_of_section_tree_list !section_tree) -;; - -let section_stack = ref [];; -let xmloutput = ref (ref []);; -let filename = ref "";; - -let reset_output fname = - filename := fname ; - xmloutput := ref [] ; - section_stack := [] -;; - -let output n = - let xmloutput = !xmloutput in - xmloutput := (Leaf n) :: !xmloutput -;; - -let open_non_empty_element elem_name attr_list = - let newxmloutput = ref [] in - !xmloutput := (Node (elem_name, attr_list, newxmloutput)) :: !(!xmloutput) ; - section_stack := !xmloutput :: !section_stack ; - xmloutput := newxmloutput -;; - -let close_non_empty_element () = - match !section_stack with - oldxmloutput::oldsection_stack -> - xmloutput := oldxmloutput ; - section_stack := oldsection_stack - | _ -> raise NoOpenNonEmptyElements -;; - -let print_output () = - Xml.pp (token_stream_of_section_tree_list !(!xmloutput)) (Some !filename) -;; diff --git a/helm/xmltheory/XmlTheory/iXml.mli b/helm/xmltheory/XmlTheory/iXml.mli deleted file mode 100644 index 11fad8202..000000000 --- a/helm/xmltheory/XmlTheory/iXml.mli +++ /dev/null @@ -1,7 +0,0 @@ -exception NoOpenNonEmptyElements - -val reset_output : string -> unit -val output : Xml.token Stream.t -> unit -val open_non_empty_element : string -> (string * string) list -> unit -val close_non_empty_element : unit -> unit -val print_output : unit -> unit diff --git a/helm/xmltheory/XmlTheory/xmltheoryentries.ml b/helm/xmltheory/XmlTheory/xmltheoryentries.ml deleted file mode 100644 index de3c5030a..000000000 --- a/helm/xmltheory/XmlTheory/xmltheoryentries.ml +++ /dev/null @@ -1,371 +0,0 @@ -(*********************) -(* Utility functions *) -(*********************) - -let fail () = - Pp.warning "XmlTheory: AST not recognized" -;; - -(* name is the name of the function to hook *) -(* hook is an hook partial-function to recognize particular inputs *) -let set_hook name hook = - let module V = Vernacinterp in - let old = V.vinterp_map name in - V.vinterp_add name - (fun l () -> - old l () ; - hook l - ) -;; - - -(*****************************************************) -(* Vernacular administrative commands for the module *) -(*****************************************************) - -let header = -"\n" ^ -"\n" -;; - -(*Vecchio, ma funzionante -let module V = Vernacinterp in - V.vinterp_add "XMLTHEORYBEGIN" - (function - [V.VARG_STRING curi ; V.VARG_STRING filename] -> - fun () -> - IXml.reset_output filename ; - IXml.output (Xml.xml_cdata header) ; - IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi] - | _ -> V.bad_vernac_args "XMLTHEORYBEGIN" - ) -;; -*) - -let module V = Vernacinterp in -let module L = Library in -let module S = System in -let module N = Names in - V.vinterp_add "XMLTHEORYBEGIN" - (function - [V.VARG_IDENTIFIER id ; V.VARG_STRING root_dir] -> - fun () -> - let s = N.string_of_id id in - let lpe,_ = - S.find_file_in_path (L.get_load_path ()) (s^".v") - in - let curi = "/" ^ String.concat "/" lpe.S.coq_dirpath in - let dirname = root_dir ^ curi in - Unix.system ("mkdir -p " ^ dirname) ; - let filename = dirname ^ "/" ^ s ^ ".theory" in - IXml.reset_output filename ; - IXml.output (Xml.xml_cdata header) ; - IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi ^ "/" ^ s] - | _ -> V.bad_vernac_args "XMLTHEORYBEGIN" - ) -;; - -let module V = Vernacinterp in - V.vinterp_add "XMLTHEORYEND" - (function - [] -> - fun () -> - IXml.close_non_empty_element () ; - IXml.print_output () - | _ -> V.bad_vernac_args "XMLTHEORYEND" - ) -;; - - -(**********************************************************) -(* All the vernacular commands on which one is interested *) -(* should be overridden here *) -(**********************************************************) - -let module V = Vernacinterp in -let module N = Names in -let module S = System in -let module L = Library in - set_hook "Require" - (function - [V.VARG_STRING import; V.VARG_STRING specif; V.VARG_IDENTIFIER id] -> - (* id is the identifier of the module, but we need the absolute *) - (* identifier as an URI. *) - (* E.g.: Logic ==> theory:/Coq/Init/Logic.theory *) - let name = N.string_of_id id in - let ({S.coq_dirpath = coq_dirpath},_) = L.module_filename name in - let uri = - "theory:/" ^ (String.concat "/" coq_dirpath) ^ "/" ^ name ^ ".theory" - in - IXml.output - (Xml.xml_nempty "vernacular" [] - (Xml.xml_empty - "Require" - ["import",import; "specif",specif; "uri",uri] - ) - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in -let module T = Nametab in -let module N = Names in - set_hook "HintsResolve" - (function - (V.VARG_VARGLIST l)::lh -> - IXml.output - (Xml.xml_nempty "vernacular" [] - (Xml.xml_nempty - "HintsResolve" [] - [< Xml.xml_nempty "dbs" [] - (List.fold_right - (function - (V.VARG_IDENTIFIER x) -> - (function i -> - [< Xml.xml_empty "db" ["name",N.string_of_id x]; - i - >] - ) - | _ -> Vernacinterp.bad_vernac_args "HintsResolve" - ) - l [<>]) ; - Xml.xml_nempty "hints" [] - (List.fold_right - (function - (V.VARG_QUALID x) -> - (function i -> - [< Xml.xml_empty "hint" ["name",T.string_of_qualid x]; - i - >] - ) - | _ -> Vernacinterp.bad_vernac_args "HintsResolve" - ) - lh [<>] - ) - >] - ) - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "IMPLICIT_ARGS_ON" - (function - [] -> - IXml.output - (Xml.xml_nempty "vernacular" [] - (Xml.xml_empty - "ImplicitArguments" - ["status","ON"] - ) - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "DEFINITION" - (function - (* Coq anomaly: a Local definition is a Definition at the syntax *) - (* level but a Variable at the logical level. Here we have to *) - (* recognize the two cases and treat them differently *) - (V.VARG_STRING "LOCAL":: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c:: rest) -> - IXml.output - (Xml.xml_nempty "VARIABLES" ["as","LOCAL"] - (Xml.xml_empty - "VARIABLE" - ["uri",Names.string_of_id id ^ ".var"] - ) - ) - | (V.VARG_STRING kind:: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c :: rest) -> - IXml.output - (Xml.xml_empty - "DEFINITION" - ["uri", Names.string_of_id id ^ ".con" ; "as",kind] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "BeginSection" - (function - [V.VARG_IDENTIFIER id] -> - IXml.open_non_empty_element "SECTION" ["uri", Names.string_of_id id] - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "EndSection" - (function - [V.VARG_IDENTIFIER id] -> - IXml.close_non_empty_element () - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "StartProof" - (function - [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] -> - IXml.output - (Xml.xml_empty - "THEOREM" - ["uri", Names.string_of_id s ^ ".con"; "as",kind] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "MUTUALINDUCTIVE" - (function - [V.VARG_STRING f; V.VARG_VARGLIST indl] -> - (* we need the name of the first inductive defined *) - (* type in the block to get the URI *) - let name = - match indl with - (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name - | _ -> assert false - in - IXml.output - (Xml.xml_empty - "DEFINITION" - ["uri", Names.string_of_id name ^ ".ind"; "as",f] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "VARIABLE" - (function - [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] -> - (* here we need all the names *) - let names = - List.flatten (List.map fst slcl) - in - IXml.output - (Xml.xml_nempty "VARIABLES" ["as",kind] - (List.fold_right - (fun name s -> - [< (Xml.xml_empty - "VARIABLE" - ["uri",Names.string_of_id name ^ ".var"] - ) ; s - >] - ) names [<>] - ) - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in -let module T = Nametab in -let module N = Names in - set_hook "COERCION" - (function - [V.VARG_STRING kind; V.VARG_STRING identity; V.VARG_QUALID qid; - V.VARG_QUALID qids; V.VARG_QUALID qidt] -> - (* let's substitute empty strings with non-empty strings *) - (* to get a stricter DTD *) - let remove_empty_string s = if s = "" then "UNSPECIFIED" else s in - let kind = remove_empty_string kind in - let identity = remove_empty_string identity in - IXml.output - (Xml.xml_nempty "vernacular" [] - (Xml.xml_empty - "Coercion" - ["kind",kind; "identity",identity ; "name",T.string_of_qualid qid ; - "source",T.string_of_qualid qids;"target",T.string_of_qualid qidt] - ) - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "MUTUALRECURSIVE" - (function - [V.VARG_VARGLIST lmi] -> - (* we need the name of the first inductive defined *) - (* type in the block to get the URI *) - let name = - match lmi with - (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name - | _ -> assert false - in - IXml.output - (Xml.xml_empty - "DEFINITION" - ["uri", Names.string_of_id name ^ ".con" ; "as","Fixpoint"] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "MUTUALCORECURSIVE" - (function - [V.VARG_VARGLIST lmi] -> - (* we need the name of the first inductive defined *) - (* type in the block to get the URI *) - let name = - match lmi with - (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name - | _ -> assert false - in - IXml.output - (Xml.xml_empty - "DEFINITION" - ["uri", Names.string_of_id name ^ ".con" ; "as","CoFixpoint"] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "RECORD" - (function - [V.VARG_STRING coe; - V.VARG_IDENTIFIER struc; - V.VARG_BINDERLIST binders; - V.VARG_CONSTR sort; - V.VARG_VARGLIST namec; - V.VARG_VARGLIST cfs] -> - IXml.output - (Xml.xml_empty - "DEFINITION" - ["uri", Names.string_of_id struc ^ ".ind" ; "as","Record"] - ) - | _ -> fail () - ) -;; - -let module V = Vernacinterp in - set_hook "PARAMETER" - (function - [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] -> - (* here we need all the names *) - let names = - List.flatten (List.map fst slcl) - in - IXml.output - (Xml.xml_nempty "AXIOMS" ["as",kind] - (List.fold_right - (fun name s -> - [< (Xml.xml_empty - "AXIOM" - ["uri",Names.string_of_id name ^ ".con"] - ) ; s - >] - ) names [<>] - ) - ) - | _ -> fail () - ) -;; diff --git a/helm/xmltheory/maththeory.dtd b/helm/xmltheory/maththeory.dtd deleted file mode 100644 index f010b6500..000000000 --- a/helm/xmltheory/maththeory.dtd +++ /dev/null @@ -1,78 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- 2.39.5