--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<head>
+
+<style type="text/css">
+#normal { background-color: #e6e6fa; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+ul.control { padding-left: 1em; list-style: none; }
+ul.control2 { font-size: small; padding-left: 2em; }
+div.center { text-align: center }
+h2.uri { margin-top: 0ex; margin-bottom: 0ex }
+</style>
+
+<script>
+ var annotations="<subst:annotations/>";
+ var CICURI="<subst:CICURI/>";
+ var cleanCICURI="<subst:cleanCICURI/>";
+ var CICURL = "<subst:CICURL/>";
+ var DCRDFURL = "<subst:DCRDFURL/>";
+ var DirectRDFURL = "<subst:DirectRDFURL/>";
+ var getterURL = "<subst:getterURL/>";
+ var HTMLURL = "<subst:HTMLURL/>";
+ var ProofTreeURL = "<subst:makeProofTreeURL/>";
+ var InverseRDFURL = "<subst:InverseRDFURL/>";
+ var MathMLContentURL = "<subst:MathMLContentURL/>";
+ var MathMLPresentationURL = "<subst:MathMLPresentationURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
+ var mkDirDepURL = "<subst:makeDirectDependencyURL/>";
+ var mkInvDepURL = "<subst:makeInverseDirectDependencyURL/>";
+ var mkInvRecDepURL = "<subst:makeInverseRecDependencyURL/>";
+ var mkRecDepURL = "<subst:makeRecDependencyURL/>";
+ var processorURL = "<subst:processorURL/>";
+ var profile = "<subst:profile/>";
+ var proofcheckerURL = "<subst:proofcheckerURL/>";
+ var url = "<subst:url/>";
+</script>
+</head>
+
+<body id="normal">
+ <div class="center">
+ <small>
+ User:
+ <uwobo:profileCtrlOptionList xmlns:uwobo="http://helm.cs.unibo.it/uwobo"
+ type="cic"/>
+ <br />
+ [<a href="http://helm.cs.unibo.it" target="_top">HELM home</a>]
+ <script>
+ document.write('[<a target="_top" href="' + processorURL +
+ 'apply?keys=SPK&param.processorURL=' + escape(processorURL) +
+ '&param.profile=' + escape(profile) +
+ '&xmluri=' + interfaceURL + 'html/configuration.html' +
+ '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
+ <div class="center">
+ <script>
+ document.write('<a target="result" style="color:black; text-decoration:none" href="' + url + '">');
+ document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/object.png" />');
+ </script>
+ <h2 class="uri"><subst:base_CICURI/></h2>
+ <script>document.write('</a>');</script>
+ </div>
+ <hr />
+<!--
+ [Annotations are <script>if (annotations) == 'no') document.write('off'); else document.write('on')</script>]
+-->
+<ul class="control">
+<!--
+ <li>
+ <script>
+ var url = "<subst:url/>";
+ document.write('<a href="' + url + '" target="_blank">Open object in new window</a>');
+ </script>
+ </li>
+-->
+ <li>
+ View
+ <script>
+ document.write('[ <a href="' + HTMLURL + '&param.toplevel=true" target="result"><small>HTML</small></a>');
+ document.write(' | ');
+ document.write('<a href="' + MathMLPresentationURL + '&param.toplevel=true" target="result"><small>MathML</small></a> ]');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a href="' + ProofTreeURL + '&param.toplevel=true" target="result">View proof tree</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ var url = processorURL + "apply?keys=MC%2CRT%2CL&xmluri=" +
+ getterURL + "getxml%3Furi%3D" + cleanCICURI +
+ "&prop.media-type=text/html&prop.encoding=iso-8859-1" +
+ "&param.CICURI=" + cleanCICURI + "&param.profile=" + profile +
+ "&profile=" + profile;
+ document.write(
+ '<a target="result" href="' + url + '">View metadata</a>'
+ );
+ </script>
+ </li>
+ <li>
+ <script>
+ url = proofcheckerURL + "proofCheck?uri=" + cleanCICURI;
+ document.write(
+ '<a target="result" href="' + url + '">Proof check</a>'
+ );
+ </script>
+ </li>
+ <li>
+ Analyse dependencies
+ <ul class="control2">
+ <li>
+ <script>
+ document.write('<a target="result" href="' + mkDirDepURL + '">direct</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a target="result" href="' + mkInvDepURL + '">inverse</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a target="result" href="' + mkRecDepURL + '">recursive direct</a> (graph)');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a target="result" href="' + mkInvRecDepURL + '">recursive inverse</a> (graph)');
+ </script>
+ </li>
+ </ul>
+ </li>
+</ul>
+<hr />
+<ul class="control">
+ <li> Download
+ <ul class="control2">
+ <li>
+ <script>
+ document.write('<a href="' + CICURL + '" target="result">CIC XML</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a href="' + MathMLContentURL + '" target="result">MathML Content</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a href="' + MathMLPresentationURL + '" target="result">MathML Presentation</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a href="' + HTMLURL + '" target="result">HTML</a>');
+ </script>
+ </li>
+ </ul>
+ </li>
+ <li>
+ Download metadata
+ <ul class="control2">
+ <li>
+ <script>
+ document.write('<a target="result" href="' + DirectRDFURL + '">direct dependencies</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a target="result" href="' + InverseRDFURL + '">inverse dependencies</a>');
+ </script>
+ </li>
+ <li>
+ <script>
+ document.write('<a target="result" href="' + DCRDFURL + '">Dublin Core</a>');
+ </script>
+ </li>
+ </ul>
+ </li>
+</ul>
+</body>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+<head>
+ <title><subst:CICURI/></title>
+</head>
+<script>
+ var processorURL = "<subst:processorURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
+ var profile = "<subst:profile/>";
+ var CICURI = "<subst:CICURI/>";
+ var annotations = "<subst:annotations/>";
+ var url = "<subst:makeURL/>";
+<![CDATA[
+ document.write('<frameset cols="20%,*" border="1">');
+ document.write('<frame src="' + processorURL +
+ 'apply?keys=SPK%2CRT&profile=' + profile + '¶m.profile=' + profile +
+ '¶m.annotations=' + annotations + '¶m.CICURI=' +
+ CICURI + '¶m.url=' + escape(url) + '&xmluri=' +
+ escape(interfaceURL + 'html/cic/control.html') +'"/>');
+ document.write('<frame src="' + url + '¶m.toplevel=true" name="result"/>');
+ document.write('</frameset>');
+]]>
+</script>
+</html>
--- /dev/null
+<?xml version="1.0"?>
+
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:uwobo="http://helm.cs.unibo.it/uwobo">
+
+<head>
+<title>Configuration</title>
+<style type="text/css">
+#normal { background-color: white; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+#centered { text-align: center }
+div.center { text-align: center }
+</style>
+
+<script language="JavaScript" src="http://helm.cs.unibo.it/helm/javascript/defaults.js">
+ 
+</script>
+<script language="JavaScript" src="http://helm.cs.unibo.it/helm/javascript/prelude.js">
+ 
+</script>
+
+</head>
+
+<body id="normal">
+<a name="top"/>
+<table border="0" width="100%" cellpadding="4">
+<tr><td class="head" align="center"><big><big>HELM Library Configuration</big></big></td></tr>
+</table>
+
+<div id="indent">
+<br />
+When you are done with the changes, please <em>do not forget to click on the Save button</em> at the
+bottom of the page.
+<br />
+<table border="0">
+ <tr>
+ <th colspan="2" align="left">Profile</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="profile">
+ <script>
+ var defaultValue = '<uwobo:profile/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form name="profileList">
+ <script>
+ var interfaceURL = '<uwobo:key name="interfaceURL"/>';
+ </script>
+ <select onChange="selectProfile(this, interfaceURL)">
+ <option value="">---</option>
+ <uwobo:profileOptionList/>
+ </select>
+ </form>
+ </td>
+ <td>
+ (changing the profile will update all the fields below)
+ </td>
+ </tr>
+ <tr>
+ <td colspan="2" align="left"><b>UWOBO URL</b>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form name="uwoboURL">
+ <script>
+ var defaultValue = '<uwobo:key name="processorURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectUwoboURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getUwoboURL() + 'help')"/>
+   
+ [<a href="http://www.cs.unibo.it/helm/uwobo/panel/index.html">UWOBO panel</a>]
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <td colspan="2" align="left"><b>Getter URL</b>
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form name="getterURL">
+ <script>
+ var defaultValue = '<uwobo:key name="getterURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectGetterURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getGetterURL() + 'help')"/>
+   
+ [<a href="http://www.cs.unibo.it/helm/getter/panel/index.html">Getter panel</a>]
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">URI-Set URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="uri_set_queueURL">
+ <script>
+ var defaultValue = '<uwobo:key name="uri_set_queueURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectURISetQueueURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getURISetQueueURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">Graph Drawer URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="draw_graphURL">
+ <script>
+ var defaultValue = '<uwobo:key name="draw_graphURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectDrawGraphURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getDrawGraphURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">Proof-Checker URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="proofcheckerURL">
+ <script>
+ var defaultValue = '<uwobo:key name="proofcheckerURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectProofCheckerURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getProofCheckerURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">Search Engine URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="searchengineURL">
+ <script>
+ var defaultValue = '<uwobo:key name="searchengineURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectSearchEngineURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getSearchEngineURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">RDFly URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="rdflyURL">
+ <script>
+ var defaultValue = '<uwobo:key name="rdflyURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectRdflyURL(this)">
+ <option value="">---</option>
+ <option value="localhost">localhost</option>
+ <option value="mowgli.cs.unibo.it">mowgli</option>
+ <option value="marcello.cs.unibo.it">marcello</option>
+ </select>
+ </form>
+ </td>
+ <td>
+ <form>
+ <input type="button" value="Check" onClick="window.open(getRdflyURL() + 'help')"/>
+ </form>
+ </td>
+ </tr>
+ <tr>
+ <th colspan="2" align="left">Interface URL</th>
+ </tr>
+ <tr>
+ <td>
+ <form name="interfaceURL">
+ <script>
+ var defaultValue = '<uwobo:key name="interfaceURL"/>';
+ document.write('<input type="text" value="' + defaultValue + '" size="50"/>');
+ </script>
+ </form>
+ </td>
+ <td>
+ <form>
+ <select onChange="selectInterfaceURL(this)">
+ <option value="">---</option>
+ <option value="mowgli">helm</option>
+ </select>
+ </form>
+ </td>
+ </tr>
+</table>
+<br />
+<table border="0">
+<tr>
+<td><b style="padding-right: 2em">Natural language rendering</b></td>
+<td>
+<form name="naturalLanguage">
+<script>
+var defaultValue = '<uwobo:key name="naturalLanguage"/>';
+if (defaultValue == 'yes')
+ document.write('<input type="checkbox" checked="1" />');
+else
+ document.write('<input type="checkbox" />');
+</script>
+</form>
+</td>
+</tr>
+<tr>
+<td><b style="padding-right: 2em">Maximum size of dependency graph</b></td>
+<td>
+<form name="maxGraphSize">
+<script>
+var defaultValue = '<uwobo:key name="uri_set_size"/>';
+document.write('<input type="text" value="' + defaultValue + '" size="3" maxlength="3" />');
+</script>
+</form>
+</td>
+</tr>
+</table>
+<br />
+<table border="0">
+ <tr>
+ <th colspan="2" align="left">Browser</th>
+ </tr>
+ <tr>
+ <td>
+ 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.
+ </td>
+ </tr>
+ <tr>
+ <td>
+ 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.
+ </td>
+ </tr>
+ <tr>
+ <td>
+ <form name="UNICODEvsSYMBOL">
+ <b>Where do you see the "not belongs to" symbol?</b>
+ <script>
+ var defaultValue = '<uwobo:key name="UNICODEvsSYMBOL"/>';
+ if (defaultValue == 'symbol')
+ document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="symbol" checked="" />');
+ else
+ document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="symbol" />');
+ </script>
+ <font face="symbol">Ï</font>
+ <script>
+ var defaultValue = '<uwobo:key name="UNICODEvsSYMBOL"/>';
+ if (defaultValue == 'unicode')
+ document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="unicode" checked="" />');
+ else
+ document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="unicode" />');
+ </script>
+ ∉
+ </form>
+ </td>
+ </tr>
+</table>
+</div>
+
+<div class="center">
+ <form name="submit">
+ <script>
+ var origProfileId = '<uwobo:profile/>';
+ </script>
+ <input type="button" value="Save" onClick="saveProfile(origProfileId)"/>
+ </form>
+</div>
+
+</body>
+</html>
+
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<head>
+
+<style type="text/css">
+#normal { background-color: #e6e6fa; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+#centered { text-align: center }
+li { padding-bottom: 1ex }
+div.center { text-align: center }
+h2.uri { margin-top: 0ex; margin-bottom: 0ex }
+</style>
+
+<script>
+ var interfaceURL = "<subst:interfaceURL/>";
+ var processorURL = "<subst:processorURL/>";
+ var profile = "<subst:profile/>";
+ var url = "<subst:url/>";
+</script>
+
+</head>
+
+<body id="normal">
+ <div class="center">
+ <small>
+ User:
+ <uwobo:profileCtrlOptionList xmlns:uwobo="http://helm.cs.unibo.it/uwobo"
+ type="folder"/>
+ <br />
+ [<a href="http://helm.cs.unibo.it" target="_top">HELM home</a>]
+ <script>
+ document.write('[<a target="_top" href="' + processorURL +
+ 'apply?keys=SPK&param.processorURL=' + escape(processorURL) +
+ '&param.profile=' + escape(profile) +
+ '&xmluri=' + interfaceURL + 'html/configuration.html' +
+ '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
+ <div class="center">
+ <script>
+ document.write('<a target="result" style="color:black; text-decoration:none" href="' + url + '">');
+ document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/folder.png" />');
+ </script>
+ <h2 class="uri"><subst:base_CICURI/></h2>
+ <script>document.write('</a>');</script>
+ </div>
+<!--
+ <ul>
+ <li>
+ <script>
+ var url = "<subst:url/>";
+ document.write('<a href="' + url + '" target="_blank">Open theory in new window</a>');
+ </script>
+ </li>
+ </ul>
+-->
+</body>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+<head>
+ <title><subst:CICURI/></title>
+</head>
+<script>
+ var processorURL = "<subst:processorURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
+ var profile = "<subst:profile/>";
+ var CICURI = "<subst:cleanCICURI/>";
+ var annotations = "<subst:annotations/>";
+ var url = "<subst:makeTheoryURL/>";
+<![CDATA[
+ document.write('<frameset cols="20%,*" border="1" >');
+ document.write('<frame src="' + processorURL +
+ 'apply?keys=SPK%2CRT&profile=' + profile + '¶m.profile=' + profile +
+ '¶m.annotations=' + annotations + '¶m.CICURI=' + CICURI +
+ '¶m.url=' + escape(url) + '&xmluri=' +
+ escape(interfaceURL + 'html/folder/control.html') +'"/>');
+ document.write('<frame src="' + url + '¶m.toplevel=true" name="result"/>');
+ document.write('</frameset>');
+]]>
+</script>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<head>
+
+<style type="text/css">
+#normal { background-color: #e6e6fa; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+#centered { text-align: center }
+li { padding-bottom: 1ex }
+div.center { text-align: center }
+h2.uri { margin-top: 0ex; margin-bottom: 0ex }
+</style>
+
+<script>
+ var interfaceURL = "<subst:interfaceURL/>";
+ var processorURL = "<subst:processorURL/>";
+ var profile = "<subst:profile/>";
+ var url = "<subst:url/>";
+</script>
+
+</head>
+
+<body id="normal">
+ <div class="center">
+ <small>
+ User:
+ <uwobo:profileCtrlOptionList xmlns:uwobo="http://helm.cs.unibo.it/uwobo"
+ type="theory"/>
+ <br />
+ [<a href="http://helm.cs.unibo.it" target="_top">HELM home</a>]
+ <script>
+ document.write('[<a target="_top" href="' + processorURL +
+ 'apply?keys=SPK&param.processorURL=' + escape(processorURL) +
+ '&param.profile=' + escape(profile) +
+ '&xmluri=' + interfaceURL + 'html/configuration.html' +
+ '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
+ <div class="center">
+ <script>
+ document.write('<a target="result" style="color:black; text-decoration:none" href="' + url + '&param.toplevel=true">');
+ document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/theory.png" />');
+ </script>
+ <h2 class="uri"><subst:base_CICURI/></h2>
+ <script>document.write('</a>');</script>
+ </div>
+<!--
+ <ul>
+ <li>
+ <script>
+ var url = "<subst:url/>";
+ document.write('<a href="' + url + '" target="_blank">Open theory in new window</a>');
+ </script>
+ </li>
+ </ul>
+-->
+</body>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+<head>
+ <title><subst:CICURI/></title>
+</head>
+<script>
+ var processorURL = "<subst:processorURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
+ var profile = "<subst:profile/>";
+ var CICURI = "<subst:cleanCICURI/>";
+ var annotations = "<subst:annotations/>";
+ var url = "<subst:makeTheoryURL/>";
+<![CDATA[
+ document.write('<frameset cols="20%,*" border="1" >');
+ document.write('<frame src="' + processorURL +
+ 'apply?keys=SPK%2CRT&profile=' + profile + '¶m.profile=' + profile +
+ '¶m.annotations=' + annotations + '¶m.CICURI=' + CICURI +
+ '¶m.url=' + escape(url) + '&xmluri=' +
+ escape(interfaceURL + 'html/theory/control.html') +'"/>');
+ document.write('<frame src="' + url + '" name="result"/>');
+ document.write('</frameset>');
+]]>
+</script>
+</html>
--- /dev/null
+
+TARGETS = helmjsmenu.js_xml
+
+.SUFFIXES:
+.SUFFIXES: .js .js_xml
+
+.js.js_xml:
+ @echo "<?xml version='1.0'?>" >$@
+ @echo "<script>" >>$@
+ @echo "<![CDATA[" >>$@
+ @cat $< >>$@
+ @echo "]]>" >>$@
+ @echo "</script>" >>$@
+
+all: $(TARGETS)
+
+clean:
+ rm -rf $(TARGETS)
+
--- /dev/null
+// 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;
+}
--- /dev/null
+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();
+ }
+}
+
--- /dev/null
+<?xml version="1.0"?>
+
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:output
+ method="xml"
+ encoding="iso-8859-1"
+ media-type="text/html"
+ doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
+ doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
+
+<xsl:param name="uri" select="''"/>
+
+<xsl:template match="helm:getParam">
+ <xsl:value-of select="$uri"/>
+</xsl:template>
+
+<xsl:template match = "/|*">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:helm="http://www.cs.unibo.it/helm"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+ <xsl:output method="html" encoding="iso-8859-1"/>
+
+ <xsl:param name="CICURI" select="''" />
+ <xsl:param name="interfaceURL" select="''" />
+
+ <xsl:template match="ls">
+ <html>
+ <head>
+ <style>
+ li.theory {
+ list-style-image:
+ url(<xsl:value-of select="$interfaceURL"/>/icons/theory.png)
+ }
+ li.folder {
+ list-style-image:
+ url(<xsl:value-of select="$interfaceURL"/>/icons/folder.png)
+ }
+ li.object {
+ list-style-image:
+ url(<xsl:value-of select="$interfaceURL"/>/icons/object.png)
+ }
+ a.theory { text-decoration: none; }
+ a.folder { text-decoration: none; }
+ a.object { text-decoration: none; }
+ </style>
+ </head>
+ <body>
+ <ul>
+ <xsl:apply-templates select="object[@name='index.theory']"/>
+ <!-- sorting: folders interleaved with theories, then objects-->
+ <xsl:apply-templates
+ select="section|object[substring-after(@name,'.')='theory' and
+ not(@name='index.theory')]">
+ <xsl:sort select="translate(concat(@name,string(.)),'abcdefghijklmnopqrstuvwxyz','ABCDEFGHIJKLMNOPQRSTUVWXYZ')" />
+ </xsl:apply-templates>
+ <xsl:apply-templates
+ select="object[not(substring-after(@name,'.')='theory')]" >
+ <xsl:sort select="translate(concat(@name,string(.)),'abcdefghijklmnopqrstuvwxyz','ABCDEFGHIJKLMNOPQRSTUVWXYZ')" />
+ </xsl:apply-templates>
+ </ul>
+ </body>
+ </html>
+ </xsl:template>
+
+ <xsl:template match="section">
+ <li class="folder">
+ <a class="folder" href="{concat($CICURI, text(), '/')}"
+ helm:helm_link="href">
+ <xsl:value-of select="text()" />
+ </a>
+ <xsl:text>/</xsl:text>
+ </li>
+ </xsl:template>
+
+ <xsl:template match="object">
+ <xsl:choose>
+ <xsl:when test="substring-after(@name, '.')='theory'">
+ <li class="theory">
+ <a class="theory" href="{concat($CICURI, @name)}"
+ helm:helm_link="href">
+ <xsl:value-of select="@name" />
+ </a>
+ </li>
+ </xsl:when>
+ <xsl:otherwise>
+ <li class="object">
+ <a class="object"
+ href="{concat('cic:', substring-after($CICURI, ':'), @name)}"
+ helm:helm_link="href">
+ <xsl:value-of select="@name" />
+ </a>
+ </li>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.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/. -->
+
+<xsl:stylesheet version="1.0"
+ xmlns="http://www.w3.org/1999/xhtml"
+ xmlns:html="http://www.w3.org/1999/xhtml"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<xsl:import href="utils.xsl"/>
+<xsl:import href="links_library.xsl"/>
+
+<!--CSC: code cut & pasted also in metadataLib.xsl -->
+<xsl:param name="uri_set_size" select="''"/>
+<!--CSC: end of cut & paste also in metadataLib.xsl -->
+
+<xsl:output method="html" encoding="iso-8859-1"/>
+
+<xsl:template match="/|*">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template match="html:head">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <subst:script language="JavaScript" src="/javascript/helmjsmenu.js"/>
+ <script>
+ var lastX, lastY;
+ var selectedURI;
+ var selectedCICURL;
+ var selectedForwardURL;
+ var selectedBackwardURL;
+ </script>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template match="html:body">
+ <!--CSC: end of cut & paste also in metadataLib.xsl -->
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:attribute name="onClick">hideMenu();</xsl:attribute>
+ <!--CSC: end of cut & paste also in metadataLib.xsl -->
+ <xsl:apply-templates/>
+ <div style="position: absolute" id="HJMmenu">
+ <!-- The two nested tables are for NS 4.0 where every -->
+ <!-- layer has a default transparent background color -->
+ <table bgColor="green" id="pippo">
+ <tr><td>
+ <table bgColor="cyan" border="2">
+ <tr><td><a href="javascript: location = selectedForwardURL">Objects this one depends on.</a></td></tr>
+ <tr><td><a href="javascript: var _ = window.open(selectedCICURL,'_top')">Render this object.</a></td></tr>
+ <tr><td><a href="javascript: location = selectedBackwardURL">Objects depending on this one.</a></td></tr>
+ </table>
+ </td></tr>
+ </table>
+ </div>
+ <script>initializeMenu()</script>
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template match="html:area">
+ <xsl:variable name="quoteduri">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="@href"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="cicurl">
+ <xsl:call-template name="makeURL">
+ <xsl:with-param name="uri" select="@href"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedcicurl">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$cicurl"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="forwardURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="@href"/>
+ <xsl:with-param name="keys" select="'MDG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedForwardURL">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$forwardURL"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="backwardURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="@href"/>
+ <xsl:with-param name="keys" select="'MMG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:variable name="quotedBackwardURL">
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="$backwardURL"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:if test="starts-with(@href,"cic:")">
+ <xsl:attribute name="onMouseOver">lastX = getX(event); lastY = getY(event); selectedURI='<xsl:value-of select="$quoteduri"/>'; selectedCICURL='<xsl:value-of select="$quotedcicurl"/>'; selectedForwardURL='<xsl:value-of select="$quotedForwardURL"/>'; selectedBackwardURL='<xsl:value-of select="$quotedBackwardURL"/>';</xsl:attribute>
+ <xsl:attribute name="href">javascript:moveMenu(lastX,lastY); showMenu();</xsl:attribute>
+ </xsl:if>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst"
+ xmlns="http://www.w3.org/1999/xhtml">
+
+<xsl:import href="utils.xsl"/>
+<xsl:import href="show_dc.xsl"/>
+<xsl:import href="links_library.xsl"/>
+<xsl:import href="toplevel_header.xsl"/>
+
+<xsl:output
+ method="xml"
+ encoding="iso-8859-1"
+ media-type="text/html"
+ doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
+ doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
+
+<xsl:param name="CICURI" select="''"/>
+
+<xsl:template match="/">
+ <html>
+ <head>
+ <title>Metadata of <xsl:value-of select="$CICURI"/></title>
+ </head>
+ <body onLoad="window.focus()" bgColor="white">
+ <xsl:call-template name="add_breadcrumb_trail" >
+ <xsl:with-param name="CICURI" select="$CICURI"/>
+ </xsl:call-template>
+ <xsl:variable name="CICURL">
+ <xsl:call-template name="makeURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+ </xsl:variable>
+ <xsl:apply-templates select="*"/>
+ <xsl:call-template name="loop_show_dc">
+ <xsl:with-param name="CICURI" select="$CICURI"/>
+ </xsl:call-template>
+ </body>
+ </html>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:helm="http://www.cs.unibo.it/helm"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<xsl:import href="links_library.xsl"/>
+<xsl:import href="params.xsl"/>
+
+<xsl:output
+ method="html"
+ encoding="ISO-8859-1"
+ media-type="text/html" />
+
+<xsl:param name="proofcheckerURL" select="''"/>
+<xsl:param name="interfaceURL" select="''"/>
+<xsl:param name="processorURL" select="''"/>
+<xsl:param name="getterURL" select="''"/>
+<xsl:param name="draw_graphURL" select="''"/>
+<xsl:param name="profile" select="''"/>
+<xsl:param name="url" select="''"/>
+<xsl:param name="CICURI" select="''"/>
+<xsl:param name="annotations" select="''"/>
+
+<xsl:template match="subst:script">
+ <xsl:copy-of select="document(concat($interfaceURL,@src,'_xml'))" />
+</xsl:template>
+
+<xsl:template match="subst:proofcheckerURL">
+ <xsl:value-of select="$proofcheckerURL"/>
+</xsl:template>
+
+<xsl:template match="subst:interfaceURL">
+ <xsl:value-of select="$interfaceURL"/>
+</xsl:template>
+
+<xsl:template match="subst:processorURL">
+ <xsl:value-of select="$processorURL"/>
+</xsl:template>
+
+<xsl:template match="subst:getterURL">
+ <xsl:value-of select="$getterURL"/>
+</xsl:template>
+
+<xsl:template match="subst:draw_graphURL">
+ <xsl:value-of select="$draw_graphURL"/>
+</xsl:template>
+
+<xsl:template match="subst:profile">
+ <xsl:value-of select="$profile"/>
+</xsl:template>
+
+<xsl:template match="subst:url">
+ <xsl:value-of select="$url"/>
+</xsl:template>
+
+<xsl:template match="subst:CICURL">
+ <xsl:call-template name="makeCICURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:HTMLURL">
+ <xsl:call-template name="makeHTMLURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:MathMLPresentationURL">
+ <xsl:call-template name="makeMathMLPresentationURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:MathMLContentURL">
+ <xsl:call-template name="makeMathMLContentURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:DirectRDFURL">
+ <xsl:call-template name="makeDirectRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:InverseRDFURL">
+ <xsl:call-template name="makeInverseRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:DCRDFURL">
+ <xsl:call-template name="makeDCRDFURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:CICURI">
+ <xsl:value-of select="$CICURI"/>
+</xsl:template>
+
+<xsl:template match="subst:cleanCICURI">
+ <xsl:variable name="uri" select="$CICURI"/>
+ <xsl:variable name="uri_before_body" select="substring-before($uri,'.body')"/>
+ <xsl:choose>
+ <xsl:when test="$uri_before_body = ''">
+ <xsl:variable name="uri_before_sharp" select="substring-before($uri,'#')"/>
+ <xsl:choose>
+ <xsl:when test="$uri_before_sharp = ''">
+ <xsl:value-of select="$uri"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$uri_before_sharp"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$uri_before_body"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="subst:base_CICURI">
+ <xsl:variable name="len" select="string-length($CICURI)" />
+ <xsl:variable name="extension">
+ <xsl:choose>
+ <xsl:when test="substring($CICURI,$len)='/'">#</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 6)='.theory'">.theory</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.con'">.con</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.ind'">.ind</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.var'">.var</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 8)='.con.body'">.con.body</xsl:when>
+ <xsl:otherwise>
+<!--
+ <xsl:message terminate="no">
+ resolve_topurl.xsl: assertion failed
+ </xsl:message>
+-->
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <xsl:call-template name="name_of_uri">
+ <xsl:with-param name="uri">
+ <xsl:choose>
+ <xsl:when test="substring($CICURI,$len)='/'">
+ <xsl:value-of select="concat(substring($CICURI,1,$len - 1),'#')" />
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$CICURI" />
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:with-param>
+ <xsl:with-param name="extension" select="$extension" />
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:annotations">
+ <xsl:value-of select="$annotations"/>
+</xsl:template>
+
+<xsl:template match="subst:makeURL">
+ <xsl:call-template name="makeURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeProofTreeURL">
+ <xsl:call-template name="makeProofTreeURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeHTMLURLwithProfile">
+ <xsl:call-template name="makeHTMLURLwithProfile">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="profile" select="@profile"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeTheoryURL">
+ <xsl:call-template name="makeTheoryURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeTheoryURLwithProfile">
+ <xsl:call-template name="makeTheoryURLwithProfile">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="true()"/>
+ <xsl:with-param name="profile" select="@profile"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeDirectDependencyURL">
+ <xsl:call-template name="makeDirectDependenciesURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeRecDependencyURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="keys" select="'MDG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeInverseDirectDependencyURL">
+ <xsl:call-template name="makeInverseDirectDependenciesURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:makeInverseRecDependencyURL">
+ <xsl:call-template name="makeGraphURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="keys" select="'MMG'"/>
+ <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
+ </xsl:call-template>
+</xsl:template>
+
+<!-- used by moogle -->
+
+<xsl:template match="helm:uwobo_form">
+ <form action="{concat($processorURL,'apply?')}" method="get">
+ <xsl:apply-templates select="*"/>
+ </form>
+</xsl:template>
+
+<xsl:template match = "helm:hidden_params">
+ <xsl:call-template name="hidden_params"/>
+</xsl:template>
+
+<xsl:template match = "helm:j_params">
+ <xsl:call-template name="j_params"/>
+</xsl:template>
+
+<xsl:template name="hidden_params">
+ <input type="hidden" name="xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="param.profile" value="{$profile}"/>
+ <input type="hidden" name="profile" value="{$profile}"/>
+ <input type="hidden" name="param.keys" value="{$keys}"/>
+ <input type="hidden" name="param.embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="param.thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="param.prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="param.media-type" value="{$media-type}"/>
+ <input type="hidden" name="param.thmedia-type" select="{$thmedia-type}"/>
+ <input type="hidden" name="prooftreemedia-type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="param.doctype-public" select="{$doctype-public}"/>
+ <input type="hidden" name="param.encoding" select="{$encoding}"/>
+ <input type="hidden" name="param.thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="param.prooftreeencoding" select="{$prooftreeencoding}"/>
+</xsl:template>
+
+<xsl:template name="j_params">
+ <input type="hidden" name="j_xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="j_processorURL" value="{$processorURL}"/>
+ <input type="hidden" name="j_profile" value="{$profile}"/>
+ <input type="hidden" name="j_keys" value="{$keys}"/>
+ <input type="hidden" name="j_embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="j_thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="j_prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="j_media_type" value="{$media-type}"/>
+ <input type="hidden" name="j_thmedia_type" select="{$thmedia-type}"/>
+ <input type="hidden" name="j_prooftreemedia_type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="j_doctype_public" select="{$doctype-public}"/>
+ <input type="hidden" name="j_encoding" select="{$encoding}"/>
+ <input type="hidden" name="j_thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="j_prooftreeencoding" select="{$prooftreeencoding}"/>
+</xsl:template>
+
+<xsl:template match="/|*">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates/>
+ </xsl:copy>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.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/. -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:m="http://www.w3.org/1998/Math/MathML"
+ xmlns:helm="http://www.cs.unibo.it/helm"
+ xmlns:xlink="http://www.w3.org/1999/xlink">
+
+<!--***********************************************************************-->
+<!-- From MathML presentation or HTML to themselves with links -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!-- First draft: March 16 2001, Andrea Asperti -->
+<!--***********************************************************************-->
+
+<xsl:param name="action" select="''"/>
+<xsl:param name="expression" select="''"/>
+<xsl:param name="advanced" select="no"/>
+<xsl:param name="choices" select="''"/>
+<xsl:param name="interp" select="''"/>
+<xsl:param name="constraints" select="''"/>
+<xsl:param name="searchengineURL" select="''"/>
+<xsl:param name="url" select="''"/>
+
+<xsl:include href="links_library.xsl"/>
+
+<xsl:variable name="quoted_expression">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$expression"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:variable name="quoted_url">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$url"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:variable name="quoted_choices">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$choices"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:variable name="quoted_constraints">
+ <xsl:call-template name="quote">
+ <xsl:with-param name="s" select="$constraints"/>
+ </xsl:call-template>
+</xsl:variable>
+
+<xsl:variable name="param_constraints">
+ <xsl:choose>
+ <xsl:when test="$constraints=''">
+ <xsl:value-of select="''"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="concat('&constraints=',$quoted_constraints)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:variable>
+
+<xsl:template match="/">
+ <xsl:copy-of select="document(concat($searchengineURL,$action,'?expression=',$quoted_expression,'&advanced=',$advanced,'&choices=',$quoted_choices,'&interpretation_choices=',$interp,$param_constraints,'&url=',$quoted_url,'&preprocess=true'))"/>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:uwobo="http://helm.cs.unibo.it/uwobo"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst"
+>
+
+<xsl:output
+ method="html"
+ encoding="ISO-8859-1"
+ media-type="text/html" />
+<!--
+<xsl:output
+ method="xml"
+ encoding="iso-8859-1"
+ media-type="text/xml"
+ doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
+ doctype-system="DTD/xhtml1-transitional.dtd" />
+-->
+
+<xsl:param name="processorURL" select="''"/>
+<xsl:param name="profile" select="''"/>
+
+<xsl:variable name="params" select="document(concat($processorURL, 'getparams?id=', $profile))"/>
+<xsl:variable name="profiles" select="document(concat($processorURL, 'listprofiles'))//li"/>
+
+<xsl:template match="node()">
+ <xsl:copy>
+ <xsl:copy-of select="@*"/>
+ <xsl:apply-templates />
+ </xsl:copy>
+</xsl:template>
+
+<xsl:template match="uwobo:key">
+ <xsl:variable name="name" select="@name"/>
+ <xsl:value-of select="string($params/html/body/ul/li[string(key)=$name]/value)"/>
+</xsl:template>
+
+<xsl:template match="uwobo:profile">
+ <xsl:value-of select="$profile"/>
+</xsl:template>
+
+<xsl:template match="uwobo:profileOptionList">
+ <xsl:apply-templates select="$profiles" mode="make_form_option"/>
+</xsl:template>
+
+<xsl:template match="uwobo:profileCtrlOptionList">
+ <script>
+ var cicurls = new Array();
+ </script>
+ <select onChange="window.open(cicurls[selectedIndex],'_top')">
+ <xsl:apply-templates select="$profiles" mode="make_ctrl_form_option">
+ <xsl:with-param name="type" select="@type"/>
+ </xsl:apply-templates>
+ </select>
+</xsl:template>
+
+<xsl:template match="li" mode="make_form_option">
+ <xsl:variable name="tmp" select="string(.)" />
+ <option value="{$tmp}">
+ <xsl:if test="$tmp=$profile">
+ <xsl:attribute name="selected">1</xsl:attribute>
+ </xsl:if>
+ <xsl:value-of select="$tmp"/>
+ </option>
+</xsl:template>
+
+<xsl:template match="li" mode="make_ctrl_form_option">
+ <xsl:param name="type" select="''"/>
+ <script>
+ <xsl:text>cicurls[</xsl:text>
+ <xsl:value-of select="position()-1" />
+ <xsl:text>] = "</xsl:text>
+ <xsl:choose>
+ <xsl:when test="$type = 'cic'">
+ <subst:makeHTMLURLwithProfile profile="{string(.)}"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <subst:makeTheoryURLwithProfile profile="{string(.)}"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:text>";</xsl:text>
+ </script><xsl:text>
+ </xsl:text>
+ <option value="{position()}">
+ <xsl:if test="string(.)=$profile">
+ <xsl:attribute name="selected">1</xsl:attribute>
+ </xsl:if>
+ <xsl:value-of select="string(.)"/>
+ </option>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory"
+ xmlns:helm="http://www.cs.unibo.it/helm"
+ xmlns:html="http://www.w3.org/1999/xhtml">
+
+<xsl:include href="links_library.xsl" />
+
+<!-- add theory's breadcrumb trail -->
+<xsl:template name="breadcrumb_trail">
+ <xsl:param name="path" select="''" />
+ <xsl:param name="acc" select="''" />
+ <xsl:choose>
+ <xsl:when test="contains($path, '/')">
+ <xsl:variable name="segment" select="substring-before($path,'/')" />
+ <xsl:variable name="newacc" select="concat($acc, $segment, '/')" />
+ <html:a style="text-decoration: none"
+ href="{$newacc}" helm:helm_link="href">
+ <xsl:value-of select="$segment" />
+ </html:a>
+ <xsl:text>/</xsl:text>
+ <xsl:call-template name="breadcrumb_trail">
+ <xsl:with-param name="path" select="substring-after($path,'/')" />
+ <xsl:with-param name="acc" select="$newacc" />
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="path_before_body" select="substring-before($path,'.body')"/>
+ <xsl:variable name="cleanpath">
+ <xsl:choose>
+ <xsl:when test="$path_before_body = ''">
+ <xsl:value-of select="$path"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$path_before_body"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <xsl:value-of select="$cleanpath" />
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="add_breadcrumb_trail">
+ <xsl:param name="CICURI" select="''"/>
+ <xsl:variable name="prefix" select="substring-before($CICURI, ':')" />
+ <html:table width="100%"><xsl:text>
+ </xsl:text>
+ <html:tr><xsl:text>
+ </xsl:text>
+ <html:td><xsl:text>
+ </xsl:text>
+ <html:span
+ style="font-family: sans-serif; font-weight: bold; font-size: 120%">
+ <html:a style="text-decoration: none"
+ href="{concat($prefix, ':/')}" helm:helm_link="href">
+ <xsl:value-of select="concat($prefix, ':')" />
+ </html:a>
+ <xsl:text>/</xsl:text>
+ <xsl:call-template name="breadcrumb_trail">
+ <xsl:with-param name="path"
+ select="substring($CICURI, string-length($prefix)+3)" />
+ <xsl:with-param name="acc" select="concat($prefix, ':/')" />
+ </xsl:call-template>
+ </html:span><xsl:text>
+ </xsl:text>
+ </html:td><xsl:text>
+ </xsl:text>
+ <html:td style="text-align:right"><xsl:text>
+ </xsl:text>
+ <html:span style="font-family:sans-serif">
+ <xsl:variable name="searchLinkURL">
+ <xsl:call-template name="makeSearchLinkURL" />
+ </xsl:variable>
+ [<html:a href="{$searchLinkURL}" target="_top">search</html:a>]
+ </html:span><xsl:text>
+ </xsl:text>
+ </html:td><xsl:text>
+ </xsl:text>
+ </html:tr>
+ </html:table><xsl:text>
+ </xsl:text>
+ <html:hr />
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<!-- Next function to quote strings for JavaScript (i.e. ' ==> \' -->
+<xsl:template name="jsquote">
+ <xsl:param name="s" select="''"/>
+ <xsl:param name="news" select="''"/>
+ <xsl:param name="times" select="1"/>
+ <xsl:choose>
+ <xsl:when test="$s = ''"><xsl:value-of select="$news"/></xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="char" select="substring($s,1,1)"/>
+ <xsl:choose>
+ <xsl:when test='$char = "'" and $times = 1'>
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="substring($s,2)"/>
+ <xsl:with-param name="news" select='concat($news,"\'")'/>
+ <xsl:with-param name="times" select="$times"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:when test='$char = "'" and $times = 2'>
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="substring($s,2)"/>
+ <xsl:with-param name="news" select='concat($news,"\\\'")'/>
+ <xsl:with-param name="times" select="$times"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="jsquote">
+ <xsl:with-param name="s" select="substring($s,2)"/>
+ <xsl:with-param name="news" select="concat($news,$char)"/>
+ <xsl:with-param name="times" select="$times"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+getParam.xsl
+ls2theory.xsl
+makeGraphLinks.xsl
+metadataControl.xsl
+resolve_topurl.xsl
+substKey.xsl
+toplevel_header.xsl
+utils.xsl
+search.xsl
--- /dev/null
+#!/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 <zack@cs.unibo.it>
+#
+# 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 <pidfile>] [-r|--request <url>] [-i|--interval <interval>] [-m|--mailto <mail>] -d|--daemon <daemon>"
+ echo " ./daemon_respawner -d|--daemon <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 <subject> <body>
+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
+
--- /dev/null
+# 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:
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM daemons
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM draw_graph.cgi
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM proof checker
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM searchEngine
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM uri_set_queue.cgi
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM daemons
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /dev/null
+#!/usr/bin/perl -w
+use strict;
+
+use LWP::UserAgent;
+use URI::Escape;
+
+my $usage = <<EOHELP;
+loadPredefinedStylesheets.pl [ uwobo_panel_conf_file ]
+loadPredefinedStylesheets.pl { -u | --unload } [ uwobo_panel_conf_file ]
+loadPredefinedStylesheets.pl { -r | --reload } [ uwobo_panel_conf_file ]
+loadPredefinedStylesheets.pl { -h | --help } [ uwobo_panel_conf_file ]
+
+If uwobo_panel_conf_file is provided, it's used as HTML file from which
+parse XSLT stylesheets, otherwise UWOBO_PANEL_CONF environment variable
+is used.
+EOHELP
+
+sub getPredefinedStylesheets ($) {
+ my $confile = shift;
+ my %stylesconf;
+ my $inForm = 0; # currenlty inside 'predefinedStylesheets' form
+ open(CONF, "< $confile") || die "Can't open $confile";
+ while(my $l = <CONF>) {
+ chomp($l);
+ if (not $inForm) {
+ if ($l =~ /<form name="predefinedStylesheets">/) {
+ $inForm = 1;
+ }
+ } else { # in form
+ if ($l =~ /<\/form>/) {
+ $inForm = 0;
+ } elsif ($l =~ /<option value="[^"]+">/) {
+ my $val = $l;
+ $val =~ s/.*<option value="([^"]+)".*>/$1/;
+ my ($key, $ur, $use_getter) = split /,/, $val;
+ $stylesconf{$key}[0] = $ur;
+ if ($use_getter =~ /true/) {
+ $use_getter = 1;
+ } elsif ($use_getter =~ /false/) {
+ $use_getter = 0;
+ } else {
+ die "Unknown value '$use_getter' for 'use_getter' field.";
+ }
+ $stylesconf{$key}[1] = $use_getter;
+ }
+ }
+ }
+ close(CONF);
+ return %stylesconf;
+}
+
+my $action = "load";
+my $opt = shift || "";
+die $usage if (($opt eq "-h") or ($opt eq "--help"));
+if (($opt eq "-u") or ($opt eq "--unload")) {
+ $action = "unload";
+} elsif (($opt eq "-r") or ($opt eq "--reload")) {
+ $action = "reload";
+} else {
+ unshift (@ARGV, $opt);
+}
+my $confile =
+ shift || $ENV{"UWOBO_PANEL_CONF"} || die "UWOBO_PANEL_CONF not defined";
+my $getter_url = $ENV{"HELM_GETTER_URL"} || die "HELM_GETTER_URL not defined";
+my $uwobo_url = $ENV{"HELM_UWOBO_URL"} || die "HELM_UWOBO_URL not defined";
+my %styles = getPredefinedStylesheets($confile);
+my $request_url = "";
+
+if ($action eq "load") { # load predefined stylesheets
+ foreach my $k (keys %styles) {
+ $request_url .= "&" unless ($request_url eq "");
+ my $ur = $styles{$k}[0];
+ my $use_getter = $styles{$k}[1];
+ $request_url .= "bind=$k,";
+ my $tmp = "";
+ if ($use_getter) {
+ $tmp .= $getter_url . "/getxslt?uri="
+ }
+ $tmp .= $ur;
+ $request_url .= uri_escape($tmp);
+ }
+ $request_url = $uwobo_url . "/add?$request_url";
+
+} elsif ($action eq "unload") { # unload predefined stylesheets
+ $request_url = $uwobo_url . "/remove?keys=" . join(',', keys %styles);
+
+} elsif ($action eq "reload") { # reload predefined stylesheets
+ $request_url = $uwobo_url . "/reload?keys=" . join(',', keys %styles);
+
+} else { # unknown action
+ die "Unknown action '$action'";
+}
+
+my $agent = LWP::UserAgent->new();
+my $response = $agent->get($request_url);
+print $response->as_string();
+# print "$request_url\n";
+
projects / helm.git / commitdiff
