<subst:CICURI/>

From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 18:49:29 +0000 (+0000) Subject: (dis)organized web stuff X-Git-Tag: 0.4.95@7852~1737 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4633c8734ded3d203fb292aec78d614a8b70ed7;p=helm.git (dis)organized web stuff --- diff --git a/daemons/on-line/html/cic/control.html b/daemons/on-line/html/cic/control.html new file mode 100644 index 000000000..8e6aeaf1f --- /dev/null +++ b/daemons/on-line/html/cic/control.html @@ -0,0 +1,189 @@ + + + + + + + + + + + +

+ + User: + +
+ [HELM home] + + +

+

+

+ +

+ +

+

+ +

+ View + +
+ +
+ +
+ +
+ Analyse dependencies +
- + +
- + +
- + +
- + +
+

+

+

Download +
- + +
- + +
- + +
- + +
+
+ Download metadata +
- + +
- + +
- + +
+

+ + diff --git a/daemons/on-line/html/cic/index.html b/daemons/on-line/html/cic/index.html new file mode 100644 index 000000000..ff3b7ba20 --- /dev/null +++ b/daemons/on-line/html/cic/index.html @@ -0,0 +1,25 @@ + + + + <subst:CICURI/> + + + diff --git a/daemons/on-line/html/configuration.html b/daemons/on-line/html/configuration.html new file mode 100644 index 000000000..f183ed118 --- /dev/null +++ b/daemons/on-line/html/configuration.html @@ -0,0 +1,373 @@ + + + + + +Configuration + + + + + + + + + + + +

HELM Library Configuration

+
+When you are done with the changes, please do not forget to click on the Save button at the +bottom of the page. +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

Profile
+ + + +	+ + + + +	+ (changing the profile will update all the fields below) +
UWOBO URL +
+ + + +	+ + + +	+ + + + [UWOBO panel] + +
Getter URL +
+ + + +	+ + + +	+ + + + [Getter panel] + +
URI-Set URL
+ + + +	+ + + +	+ + + +
Graph Drawer URL
+ + + +	+ + + +	+ + + +
Proof-Checker URL
+ + + +	+ + + +	+ + + +
Search Engine URL
+ + + +	+ + + +	+ + + +
RDFly URL
+ + + +	+ + + +	+ + + +
Interface URL
+ + + +	+ + + +

+
+ + + + + + + + + +

Natural language rendering	+ + + +
Maximum size of dependency graph	+ + + +

+
+ + + + + + + + + + + + + +

Browser
+ Only new browsers support UNICODE, that is needed to render + mathematical documents. Some old browsers, though, can render + the most common symbols through the "symbol" font. +
+ To make us understand what kind of browser you have, please + select below the symbol for "not belongs to". If both options + do not show that symbol, then you will be only able to use + the MathML mode with an external plug-out for MathML presentation. +
+ + Where do you see the "not belongs to" symbol? + + Ï + + ∉ + +

+ + + + diff --git a/daemons/on-line/html/folder/control.html b/daemons/on-line/html/folder/control.html new file mode 100644 index 000000000..32c5d71ed --- /dev/null +++ b/daemons/on-line/html/folder/control.html @@ -0,0 +1,64 @@ + + + + + + + + + + + + +

+ + User: + +
+ [HELM home] + + +

+

+

+ +

+ +

+ + + diff --git a/daemons/on-line/html/folder/index.html b/daemons/on-line/html/folder/index.html new file mode 100644 index 000000000..428a3ed0c --- /dev/null +++ b/daemons/on-line/html/folder/index.html @@ -0,0 +1,25 @@ + + + + <subst:CICURI/> + + + diff --git a/daemons/on-line/html/theory/control.html b/daemons/on-line/html/theory/control.html new file mode 100644 index 000000000..b855a6a84 --- /dev/null +++ b/daemons/on-line/html/theory/control.html @@ -0,0 +1,64 @@ + + + + + + + + + + + + +

+ + User: + +
+ [HELM home] + + +

+

+

+ +

+ +

+ + + diff --git a/daemons/on-line/html/theory/index.html b/daemons/on-line/html/theory/index.html new file mode 100644 index 000000000..6627247d2 --- /dev/null +++ b/daemons/on-line/html/theory/index.html @@ -0,0 +1,25 @@ + + + + <subst:CICURI/> + + + diff --git a/daemons/on-line/icons/folder.png b/daemons/on-line/icons/folder.png new file mode 100644 index 000000000..ec0cc0839 Binary files /dev/null and b/daemons/on-line/icons/folder.png differ diff --git a/daemons/on-line/icons/object.png b/daemons/on-line/icons/object.png new file mode 100644 index 000000000..fe89a30e8 Binary files /dev/null and b/daemons/on-line/icons/object.png differ diff --git a/daemons/on-line/icons/theory.png b/daemons/on-line/icons/theory.png new file mode 100644 index 000000000..389152ef3 Binary files /dev/null and b/daemons/on-line/icons/theory.png differ diff --git a/daemons/on-line/javascript/.cvsignore b/daemons/on-line/javascript/.cvsignore new file mode 100644 index 000000000..e268d4aeb --- /dev/null +++ b/daemons/on-line/javascript/.cvsignore @@ -0,0 +1 @@ +*.js_xml diff --git a/daemons/on-line/javascript/Makefile b/daemons/on-line/javascript/Makefile new file mode 100644 index 000000000..874bf8674 --- /dev/null +++ b/daemons/on-line/javascript/Makefile @@ -0,0 +1,19 @@ + +TARGETS = helmjsmenu.js_xml + +.SUFFIXES: +.SUFFIXES: .js .js_xml + +.js.js_xml: + @echo "" >$@ + @echo "" >>$@ + +all: $(TARGETS) + +clean: + rm -rf $(TARGETS) + diff --git a/daemons/on-line/javascript/helmjsmenu.js b/daemons/on-line/javascript/helmjsmenu.js new file mode 100644 index 000000000..0d7654315 --- /dev/null +++ b/daemons/on-line/javascript/helmjsmenu.js @@ -0,0 +1,58 @@ +// Global variables. +var HJMmenu; + +function initializeMenu() { + HJMmenu = + document.getElementById ? + // A DOM browser + document.getElementById("HJMmenu").style + : // Probably Netscape Navigator 4.0 + document.HJMmenu; + HJMmenu.visibility="hidden"; +} + +function showMenu() { + HJMmenu.visibility="visible"; +} + +function hideMenu() { + HJMmenu.visibility="hidden"; +} + +function moveMenu(x,y) { + var y2 = y - 25; + var x2 = x - 25; + if (document.getElementById) { + // Not Netscape Navigator 4.0 + HJMmenu.left = x2 + "px"; + HJMmenu.top = y2 + "px"; + } else { + // Probably Netscape Navigator 4.0 + HJMmenu.left = x2; + HJMmenu.top = y2; + } +} + +function getX(event) { + if(!event.pageX) + // Probably Internet Explorer + return event.clientX + document.body.scrollLeft; + else + // Probably Netscape Navigator + return event.pageX; +} + +function getY(event) { + if(!event.pageY) + // Probably Internet Explorer + return event.clientY + document.body.scrollTop; + else + // Probably Netscape Navigator + return event.pageY; +} + +if (!document.getElementById) { + // Probably Netscape Navigator + document.captureEvents(Event.MOUSEDOWN); + document.onmousedown = hideMenu; +} diff --git a/daemons/on-line/javascript/prelude.js b/daemons/on-line/javascript/prelude.js new file mode 100644 index 000000000..d89ae566d --- /dev/null +++ b/daemons/on-line/javascript/prelude.js @@ -0,0 +1,178 @@ +function getProfileId() +{ + return document.profile.elements[0].value; +} + +function getUwoboURL() +{ + return document.uwoboURL.elements[0].value; +} + +function getGetterURL() +{ + return document.getterURL.elements[0].value; +} + +function getProofCheckerURL() +{ + return document.proofcheckerURL.elements[0].value; +} + +function getSearchEngineURL() +{ + return document.searchengineURL.elements[0].value; +} + +function getDrawGraphURL() +{ + return document.draw_graphURL.elements[0].value; +} + +function getURISetQueueURL() +{ + return document.uri_set_queueURL.elements[0].value; +} + +function getRdflyURL() +{ + return document.rdflyURL.elements[0].value; +} + +function getInterfaceURL() +{ + return document.interfaceURL.elements[0].value; +} + +function getUNICODEvsSYMBOL() +{ + if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked) + return 'symbol'; + else + return 'unicode'; +} + +function getNaturalLanguage() +{ + if (document.naturalLanguage.elements[0].checked) + return 'yes'; + else + return 'no'; +} + +function getMaxGraphSize() +{ + return document.maxGraphSize.elements[0].value; +} + +function getUpdateURL() +{ + return '¶m.processorURL=' + escape(getUwoboURL()) + + '¶m.getterURL=' + escape(getGetterURL()) + + '¶m.uri_set_queueURL=' + escape(getURISetQueueURL()) + + '¶m.draw_graphURL=' + escape(getDrawGraphURL()) + + '¶m.proofcheckerURL=' + escape(getProofCheckerURL()) + + '¶m.searchengineURL=' + escape(getSearchEngineURL()) + + '¶m.rdflyURL=' + escape(getRdflyURL()) + + '¶m.interfaceURL=' + escape(getInterfaceURL()) + + '¶m.naturalLanguage=' + escape(getNaturalLanguage()) + + '¶m.uri_set_size=' + escape(getMaxGraphSize()) + + '¶m.UNICODEvsSYMBOL=' + escape(getUNICODEvsSYMBOL()); +} + +function selectUwoboURL(ss) +{ + if (ss.selectedIndex == 0) { + document.uwoboURL.elements[0].value = ""; + } else { + document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/"; + } +} + +function selectGetterURL(ss) +{ + if (ss.selectedIndex == 0) { + document.getterURL.elements[0].value = ""; + } else { + document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58081/"; + } +} + +function selectProofCheckerURL(ss) +{ + if (ss.selectedIndex == 0) { + document.proofcheckerURL.elements[0].value = ""; + } else { + document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58084/"; + } +} + +function selectSearchEngineURL(ss) +{ + if (ss.selectedIndex == 0) { + document.searchengineURL.elements[0].value = ""; + } else { + document.searchengineURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58085/"; + } +} + +function selectDrawGraphURL(ss) +{ + if (ss.selectedIndex == 0) { + document.draw_graphURL.elements[0].value = ""; + } else { + document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58083/"; + } +} + +function selectURISetQueueURL(ss) +{ + if (ss.selectedIndex == 0) { + document.uri_set_queueURL.elements[0].value = ""; + } else { + document.uri_set_queueURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58082/"; + } +} + +function selectRdflyURL(ss) +{ + if (ss.selectedIndex == 0) { + document.rdflyURL.elements[0].value = ""; + } else { + document.rdflyURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58086/"; + } +} + +function selectInterfaceURL(ss) +{ + if (ss.selectedIndex == 0) { + document.interfaceURL.elements[0].value = ""; + } else { + document.interfaceURL.elements[0].value = "http://helm.cs.unibo.it/helm"; + } +} + +function selectProfile(ss, interfaceURL) +{ + location = getUwoboURL() + + 'apply?keys=SPK¶m.processorURL=' + escape(getUwoboURL()) + + '¶m.profile=' + escape(ss.options[ss.selectedIndex].value) + + '&xmluri=' + escape(interfaceURL + 'html/configuration.html'); +} + +function saveProfile(origProfileId) +{ + var profileId = getProfileId(); + var exists = false; + var i; + var options = document.profileList.elements[0]; + for (i = 0; i < options.length; i++) + if (profileId == options[i].value) exists = true; + if (exists) { + if (confirm('Update the profile \'' + profileId + '\'?')) + location = getUwoboURL() + 'setparams?id=' + profileId + getUpdateURL(); + } else { + if (confirm('Create a new profile \'' + profileId + '\' with the current settings?')) + location = getUwoboURL() + 'createprofile?id=' + profileId + '&orig=' + origProfileId + getUpdateURL(); + } +} + diff --git a/daemons/on-line/xslt/getParam.xsl b/daemons/on-line/xslt/getParam.xsl new file mode 100644 index 000000000..0ec71a869 --- /dev/null +++ b/daemons/on-line/xslt/getParam.xsl @@ -0,0 +1,28 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/ls2theory.xsl b/daemons/on-line/xslt/ls2theory.xsl new file mode 100644 index 000000000..86eb20849 --- /dev/null +++ b/daemons/on-line/xslt/ls2theory.xsl @@ -0,0 +1,85 @@ + + + + + + + + + + + + + + + +

+ + + + + + + +

+ + + + + +

+ + + + / +

+ + + + + +

+ + +

+ + + + + diff --git a/daemons/on-line/xslt/makeGraphLinks.xsl b/daemons/on-line/xslt/makeGraphLinks.xsl new file mode 100644 index 000000000..4ee9dcc24 --- /dev/null +++ b/daemons/on-line/xslt/makeGraphLinks.xsl @@ -0,0 +1,138 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + hideMenu(); + + +

+ + + + +

+ + + + +

Objects this one depends on.

Render this object.

Objects depending on this one.

+

+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + lastX = getX(event); lastY = getY(event); selectedURI=''; selectedCICURL=''; selectedForwardURL=''; selectedBackwardURL=''; + javascript:moveMenu(lastX,lastY); showMenu(); + + + + + + diff --git a/daemons/on-line/xslt/metadataControl.xsl b/daemons/on-line/xslt/metadataControl.xsl new file mode 100644 index 000000000..059c0dbe5 --- /dev/null +++ b/daemons/on-line/xslt/metadataControl.xsl @@ -0,0 +1,44 @@ + + + + + + + + + + + + + + + + + Metadata of <xsl:value-of select="$CICURI"/> + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/resolve_topurl.xsl b/daemons/on-line/xslt/resolve_topurl.xsl new file mode 100644 index 000000000..c7f664374 --- /dev/null +++ b/daemons/on-line/xslt/resolve_topurl.xsl @@ -0,0 +1,285 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + # + .theory + .con + .ind + .var + .con.body + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/search.xsl b/daemons/on-line/xslt/search.xsl new file mode 100644 index 000000000..17fbee744 --- /dev/null +++ b/daemons/on-line/xslt/search.xsl @@ -0,0 +1,88 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/substKey.xsl b/daemons/on-line/xslt/substKey.xsl new file mode 100644 index 000000000..a5acc094d --- /dev/null +++ b/daemons/on-line/xslt/substKey.xsl @@ -0,0 +1,94 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/toplevel_header.xsl b/daemons/on-line/xslt/toplevel_header.xsl new file mode 100644 index 000000000..88650a5a7 --- /dev/null +++ b/daemons/on-line/xslt/toplevel_header.xsl @@ -0,0 +1,87 @@ + + + + + + + + + + + + + + + + + / + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + / + + + + + + + + + + + + + + + [search] + + + + + + + + + + + diff --git a/daemons/on-line/xslt/utils.xsl b/daemons/on-line/xslt/utils.xsl new file mode 100644 index 000000000..9213c2436 --- /dev/null +++ b/daemons/on-line/xslt/utils.xsl @@ -0,0 +1,41 @@ + + + + + + + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/daemons/on-line/xslt/xslt_index.txt b/daemons/on-line/xslt/xslt_index.txt new file mode 100644 index 000000000..94ee0c595 --- /dev/null +++ b/daemons/on-line/xslt/xslt_index.txt @@ -0,0 +1,9 @@ +getParam.xsl +ls2theory.xsl +makeGraphLinks.xsl +metadataControl.xsl +resolve_topurl.xsl +substKey.xsl +toplevel_header.xsl +utils.xsl +search.xsl diff --git a/daemons/scripts/init.d/daemon_respawner.sh b/daemons/scripts/init.d/daemon_respawner.sh new file mode 100755 index 000000000..7bbe47a10 --- /dev/null +++ b/daemons/scripts/init.d/daemon_respawner.sh @@ -0,0 +1,147 @@ +#!/bin/bash +# +# Generic respawner for daemon processes. +# +# Created: Fri, 16 Apr 2004 17:40:36 +0200 zacchiro +# Last-Modified: Fri, 16 Apr 2004 17:40:36 +0200 zacchiro +# +# by --Zack +# +# Test to see if a daemon process (run via /etc/init.d/script) if still alive, +# if not it respawns it using the corresponding init script. In order to check +# if the daemon is still alive different predicates could be used: +# 1) "ps" check with its pid +# 2) http request to its url (if it's a web services) +# all the available predicated can be enable or not (command line choice), all +# the enabled predicates are ANDed. It's enough that one of them fails to +# trigger daemon respawning. +# +# This respawner is supposed to be executed by "start" target of daemon's init.d +# script. +# +# Sample /etc/init.d/foo script: +# +# DAEMON="/usr/sbin/foo" +# PIDFILE="/var/run/$DAEMON.pid" +# start) +# echo -n "Starting $DAEMON" +# start-stop-daemon \ +# --start --background --pidfile $PIDFILE --make-pidfile --exec $DAEMON +# echo "." +# echo -n "Starting $DAEMON respawner" +# /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ +# -r http://localhost:9999/help -d `basename $0` & +# echo "." +# ;; +# stop) +# echo -n "Stopping $DAEMON respawner" +# /etc/init.d/daemon_respawner.sh -d `basename $0` -s +# echo "." +# echo -n "Stopping $DAEMON" +# start-stop-daemon --stop --pidfile $PIDFILE +# rm -f $PIDFILE +# echo "." +# ;; +# ... +# + +# parse arguments +TEMP=`getopt -o p:r:d:i:m:s --long pidfile:request:daemon:interval:mailto:stop -- "$@"` +if [ $? != 0 ]; then + echo "Usage: ./daemon_respawner [-p|--pidfile ] [-r|--request ] [-i|--interval ] [-m|--mailto ] -d|--daemon " + echo " ./daemon_respawner -d|--daemon -s|--stop" + exit 1 +fi +PIDFILE="" +REQUEST="" +DAEMON="" +INTERVAL="60" +MAILTO="" +STOP="" +eval set -- "$TEMP" +while true ; do + case "$1" in + -p|--pidfile) PIDFILE="$2"; shift 2 ;; + -r|--request) REQUEST="$2"; shift 2 ;; + -d|--daemon) DAEMON="$2"; shift 2 ;; + -i|--interval) INTERVAL="$2"; shift 2 ;; + -m|--mailto) MAILTO="$2"; shift 2 ;; + -s|--stop) STOP="yes"; shift ;; + --) shift; break ;; + esac +done +if [ -z "$DAEMON" ]; then + echo "No daemon provided: aborting." + exit 2 +fi +MYPIDFILE="/var/run/$DAEMON""_respawner.pid" +if ! [ -z "$STOP" ]; then # stop an active respawner and exit + if [ -r "$MYPIDFILE" ]; then + kill `cat "$MYPIDFILE"` + fi + rm -f "$MYPIDFILE" + exit 0 +fi +if [ -z "$PIDFILE" -a -z "$REQUEST" ]; then + echo "Neither pidfile nor request URL was provided: aborting." + exit 2 +fi + +TIMEOUT="5" # timeout for http requests + +# usage: alert +alert () +{ + if [ -z "$MAILTO" ]; then + echo "ALERT: $1" + echo "ALERT: $2" + echo + else + echo "$2" | mail -s "$1" $MAILTO + fi +} + +# check if daemon is still alive +daemon_is_alive () +{ + IS_DEAD="" + if ! [ -z "$PIDFILE" ]; then # pid check enabled + if ! (ps `cat $PIDFILE` &> /dev/null); then # pid is no longer alive + IS_DEAD="true" + fi + fi + if ! [ -z "$REQUEST" ]; then # request check enabled + if ! (wget -T $TIMEOUT -O /dev/null "$REQUEST" &> /dev/null); then + # no answer + IS_DEAD="true" + fi + fi + test -z "$IS_DEAD" +} + +# respawn daemon +start_daemon () +{ + rm -f "$MYPIDFILE" + invoke-rc.d $DAEMON stop + invoke-rc.d $DAEMON start & + exit 0 # the respawner will be restarted by daemon's init.d script +} + +# first check +sleep 1 +if ! daemon_is_alive; then + alert "$DAEMON failed to start :-((" "$DAEMON died during initialization :-((, enjoy debugging! :-P. Cheers." + exit 3 +fi +# save pid +echo $$ > "$MYPIDFILE" +# continuous checks +while true; do + sleep $INTERVAL + if ! daemon_is_alive; then + alert "$DAEMON died :-(, restarting it ..." "$DAEMON died miserably :-(. I'm going to try restarting it, you will receive an additional mail in case of failure. Cheers." + start_daemon # performed in background + fi +done + diff --git a/daemons/scripts/init.d/etc_default_helm b/daemons/scripts/init.d/etc_default_helm new file mode 100644 index 000000000..b284b5dd3 --- /dev/null +++ b/daemons/scripts/init.d/etc_default_helm @@ -0,0 +1,35 @@ +# Configuration for helm daemons + + # DAEMONS started/stopped/ecc. by /etc/init.d/helm, name listed here + # must correspond to scripts located in /etc/init.d +DAEMONS=" + helm-http-getter + helm-proof-checker + helm-uri-set-queue + helm-draw-graph + helm-search-engine + helm-uwobo + helm-rdfly +" + + # script used to load/unload uwobo predefined scripts +UWOBO_INIT_SCRIPT="/projects/helm/etc/init.d/loadPredefinedStylesheets.pl" + + # http getter cache dirs that need to be created at boot time +HTTP_GETTER_CACHE_DIRS=" + /tmp/helm + /tmp/helm/cache + /tmp/helm/cache/cic_library + /tmp/helm/cache/rdf_library + /tmp/helm/cache/nuprl_library +" + + # user which will own the daemons and the cache directories +OWNER="sacerdot:helm" + +export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081 +export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:58080 +UWOBO_PANEL_CONF=/projects/helm/public_html/uwobo/panel/control.html +NUPRL_UWOBO_PANEL_CONF="/projects/helm/nuprl/NuPRL/uwobo-panel/control.html" + +# vim: set ft=sh: diff --git a/daemons/scripts/init.d/helm b/daemons/scripts/init.d/helm new file mode 100755 index 000000000..c58a15d50 --- /dev/null +++ b/daemons/scripts/init.d/helm @@ -0,0 +1,37 @@ +#!/bin/sh +# +# init.d script for HELM daemons +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Tue, 8 Oct 2002 17:18:17 +0200 + +DAEMONS="" +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +case "$1" in + + start|stop|restart|force-reload|reload) + for d in $DAEMONS; do + /etc/init.d/$d $1 + done + ;; + + *) + echo + echo "Usage: /etc/init.d/helm { start | stop | restart | force-reload | reload }" >&2 + echo + if [ -z "$DAEMONS" ]; then + echo "Actually, no daemons are considered!" + else + echo "Actually, considered daemons are: $DAEMONS" + fi + echo "to change this setting see /etc/default/helm" + echo + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-bootmisc.sh b/daemons/scripts/init.d/helm-bootmisc.sh new file mode 100755 index 000000000..37decf723 --- /dev/null +++ b/daemons/scripts/init.d/helm-bootmisc.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +HTTP_GETTER_CACHE_DIRS="" +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +# create http_getter cache dirs +for d in $HTTP_GETTER_CACHE_DIRS; do + if ! [ -d $d ]; then + mkdir -m 2775 $d + OWNER=`echo -n $OWNER | sed -e 's/:/./'` + chown $OWNER $d + fi +done + diff --git a/daemons/scripts/init.d/helm-draw-graph b/daemons/scripts/init.d/helm-draw-graph new file mode 100755 index 000000000..70859c08d --- /dev/null +++ b/daemons/scripts/init.d/helm-draw-graph @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for HELM draw_graph.cgi +# +# by --Zack +# Created: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 + +DAEMON=/projects/helm/daemons/graphs/tools/drawGraph.opt +USAGE="Usage: /etc/init.d/helm-draw-graph { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/"$NAME".pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-http-getter b/daemons/scripts/init.d/helm-http-getter new file mode 100755 index 000000000..a6c18ae46 --- /dev/null +++ b/daemons/scripts/init.d/helm-http-getter @@ -0,0 +1,62 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Fri, 16 Apr 2004 18:21:30 +0200 + +DAEMON="/projects/helm/daemons/http_getter/http_getter.opt" +USAGE="Usage: /etc/init.d/helm-http-getter { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo -n "Starting $DAEMON" + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON + echo "done!" + echo -n "Starting $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ + -r http://localhost:58081/help -d `basename $0` & + echo "." +} + +do_stop () { + echo -n "Stopping $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -d `basename $0` -s + echo "." + echo -n "Stopping $DAEMON" + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) + echo "." +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-proof-checker b/daemons/scripts/init.d/helm-proof-checker new file mode 100755 index 000000000..9ea0eaffc --- /dev/null +++ b/daemons/scripts/init.d/helm-proof-checker @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for HELM proof checker +# +# by --Zack +# Created: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 13 Nov 2002 18:30:39 +0100 + +DAEMON=/projects/helm/daemons/proofChecker/proofChecker.opt +USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-rdfly b/daemons/scripts/init.d/helm-rdfly new file mode 100755 index 000000000..ef17cd239 --- /dev/null +++ b/daemons/scripts/init.d/helm-rdfly @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 8 Jan 2003 12:09:41 +0100 + +DAEMON="/projects/helm/daemons/rdfly/rdfly.opt" +USAGE="Usage: /etc/init.d/helm-rdfly { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-search-engine b/daemons/scripts/init.d/helm-search-engine new file mode 100755 index 000000000..cda415fdd --- /dev/null +++ b/daemons/scripts/init.d/helm-search-engine @@ -0,0 +1,62 @@ +#!/bin/sh +# +# init.d script for HELM searchEngine +# +# by --Zack +# Created: Fri, 22 Nov 2002 15:51:25 +0100 +# Last-Modified: Thu, 6 Mar 2003 17:40:16 +0100 + +DAEMON="/projects/helm/daemons/searchEngine/searchEngine.opt" +USAGE="Usage: /etc/init.d/helm-search-engine { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo -n "Starting $DAEMON" + start-stop-daemon \ + --start --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --background --exec $DAEMON + echo "." + echo -n "Starting $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ + -r http://localhost:58085/help -d `basename $0` & + echo "." +} + +do_stop () { + echo -n "Stopping $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -d `basename $0` -s + echo "." + echo -n "Stopping $DAEMON" + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) + echo "." +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-uri-set-queue b/daemons/scripts/init.d/helm-uri-set-queue new file mode 100755 index 000000000..415abdee6 --- /dev/null +++ b/daemons/scripts/init.d/helm-uri-set-queue @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for HELM uri_set_queue.cgi +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 20 Nov 2002 10:50:25 +0100 + +DAEMON=/projects/helm/daemons/graphs/tools/uriSetQueue.opt +USAGE="Usage: /etc/init.d/helm-uri-set-queue { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo "Starting $DAEMON ..." + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON +} + +do_stop () { + echo "Stopping $DAEMON ..." + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-uwobo b/daemons/scripts/init.d/helm-uwobo new file mode 100755 index 000000000..a5ab6c76a --- /dev/null +++ b/daemons/scripts/init.d/helm-uwobo @@ -0,0 +1,67 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Wed, 15 Jan 2003 15:14:07 +0100 +# Last-Modified: Fri, 16 Apr 2004 17:54:54 +0200 + +DAEMON="/projects/helm/daemons/uwobo/uwobo.opt" +USAGE="Usage: /etc/init.d/helm-uwobo { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +# Warning: $PIDFILE value is shared by UWOBO respawner, change at your own risk +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo -n "Starting $DAEMON" + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON + echo "." + echo -n "Waiting for UWOBO to startup (2 seconds) ... " + sleep 2 + echo "done!" + /etc/init.d/helm-uwobo-stylesheets start + echo -n "Starting $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ + -r http://localhost:58080/help -d `basename $0` & + echo "." +} + +do_stop () { + echo -n "Stopping $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -d `basename $0` -s + echo "." + echo -n "Stopping $DAEMON ... " + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) + echo "done!" +} + +case "$1" in + + start) + do_start + ;; + + stop) + do_stop + ;; + + restart) + do_stop + do_start + ;; + + *) + echo "$USAGE" >&2 + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/helm-uwobo-stylesheets b/daemons/scripts/init.d/helm-uwobo-stylesheets new file mode 100755 index 000000000..9c0201446 --- /dev/null +++ b/daemons/scripts/init.d/helm-uwobo-stylesheets @@ -0,0 +1,51 @@ +#!/bin/sh +# +# init.d script for HELM daemons +# +# by --Zack +# Created: Wed, 9 Oct 2002 14:26:27 +0200 +# Last-Modified: Wed, 9 Oct 2002 14:26:27 +0200 + +UWOBO_INIT_SCRIPT="" +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi +test -x "$UWOBO_INIT_SCRIPT" || exit 0 + +case "$1" in + + start) + echo -n "Loading UWOBO stylesheets (mowgli) ... " + $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null + echo "done!" + echo -n "Loading UWOBO stylesheets (mowgli NuPRL) ... " + $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null + echo "done!" + ;; + + stop) + $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + reload) + $UWOBO_INIT_SCRIPT --reload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --reload $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + restart) + $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + *) + echo + echo "Usage: /etc/init.d/helm-uwobo-stylesheets { start | stop | restart | reload }" >&2 + echo + exit 1 + ;; + +esac + diff --git a/daemons/scripts/init.d/loadPredefinedStylesheets.pl b/daemons/scripts/init.d/loadPredefinedStylesheets.pl new file mode 100755 index 000000000..700cf68f5 --- /dev/null +++ b/daemons/scripts/init.d/loadPredefinedStylesheets.pl @@ -0,0 +1,98 @@ +#!/usr/bin/perl -w +use strict; + +use LWP::UserAgent; +use URI::Escape; + +my $usage = <) { + chomp($l); + if (not $inForm) { + if ($l =~ /

/) { + $inForm = 1; + } + } else { # in form + if ($l =~ /<\/form>/) { + $inForm = 0; + } elsif ($l =~ /