+++ /dev/null
-<html>
-
-<head>
-<title>On-Line Library 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 }
-</style>
-
-<script language="JavaScript" src="../javascript/defaults.js"></script>
-<script language="JavaScript" src="../javascript/prelude.js"></script>
-
-</head>
-
-<body id="normal" onLoad="refreshLinks()">
-<a name="top"/>
-<table border="0" width="100%" cellpadding="4">
-<tr><td class="head" align="center"><big><big>On-Line Library Configuration</big></big></td></tr>
-</table>
-
-<br />
-
-<div id="indent">
-The on-line interface will use a
-<a href="http://www.cs.unibo.it/helm/getter" target="_top">Getter</a> to locate and
-download documents and an
-<a href="http://www.cs.unibo.it/helm/uwobo" target="_top">UWOBO</a> to apply transformations
-to them.
-
-
-<br /><br />
-
-Here you can choose the Getter and the UWOBO to use, providing valid URLs
-to instances of them.
-
-<br /><br />
-
-To control the behaviour of them, use the apposite
-<a onClick="refreshLinks();" href="http://www.cs.unibo.it/helm/getter/panel/index.html" target="_top">Getter panel</a>
-and
-<a onClick="refreshLinks();" href="http://www.cs.unibo.it/helm/uwobo/panel/index.html" target="_top">UWOBO panel</a>.
-
-<br /><br />
-
-<table border="0">
- <tr>
- <th colspan="2" align="left">UWOBO URL</th>
- </tr>
- <tr>
- <td>
- <form name="uwoboURL">
- <script>
- document.write('<input type="text" value="' + getInitialProcessorURL() + '" 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>
- <option value="phd.cs.unibo.it">phd</option>
- <option value="eolo.cs.unibo.it">eolo</option>
- </select>
- </form>
- </td>
- <td>
- <form>
- <input type="button" value="Check" onClick="top.result.location = getUwoboURL() + 'help'"/>
- </form>
- </td>
- </tr>
-</table>
-
-<br />
-
-<table border="0">
- <tr>
- <th colspan="2" align="left">Getter URL</th>
- </tr>
- <tr>
- <td>
- <form name="getterURL">
- <script>
- document.write('<input type="text" value="' + getInitialGetterURL() + '" 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>
- <option value="phd.cs.unibo.it">phd</option>
- <option value="eolo.cs.unibo.it">eolo</option>
- </select>
- </form>
- </td>
- <td>
- <form>
- <input type="button" value="Check" onClick="top.result.location = getGetterURL() + 'help'"/>
- </form>
- </td>
- </tr>
-</table>
-
-<br />
-
-<table border="0">
- <tr>
- <th colspan="2" align="left">URI-Set URL</th>
- </tr>
- <tr>
- <td>
- <form name="uri_set_queueURL">
- <script>
- document.write('<input type="text" value="' + getInitialURISetQueueURL() + '" 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>
- <option value="phd.cs.unibo.it">phd</option>
- <option value="eolo.cs.unibo.it">eolo</option>
- </select>
- </form>
- </td>
- <td>
- <form>
- <input type="button" value="Check" onClick="top.result.location = getURISetQueueURL() + 'help'"/>
- </form>
- </td>
- </tr>
-</table>
-
-<br />
-
-<table border="0">
- <tr>
- <th colspan="2" align="left">Graph Drawer URL</th>
- </tr>
- <tr>
- <td>
- <form name="draw_graphURL">
- <script>
- document.write('<input type="text" value="' + getInitialDrawGraphURL() + '" 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>
- <option value="phd.cs.unibo.it">phd</option>
- <option value="eolo.cs.unibo.it">eolo</option>
- </select>
- </form>
- </td>
- <td>
- <form>
- <input type="button" value="Check" onClick="top.result.location = getDrawGraphURL() + 'help'"/>
- </form>
- </td>
- </tr>
-</table>
-
-<br />
-
-<table border="0">
- <tr>
- <th colspan="2" align="left">Proof-Checker URL</th>
- </tr>
- <tr>
- <td>
- <form name="proofcheckerURL">
- <script>
- document.write('<input type="text" value="' + getInitialProofCheckerURL() + '" 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>
- <option value="phd.cs.unibo.it">phd</option>
- <option value="eolo.cs.unibo.it">eolo</option>
- </select>
- </form>
- </td>
- <td>
- <form>
- <input type="button" value="Check" onClick="top.result.location = getProofCheckerURL() + 'help'"/>
- </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>
- document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="symbol" ' + getInitialUNICODEvsSYMBOLsymbol() + ' />');
- </script>
- <font face="symbol">Ï</font>
-
- <script>
- document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="unicode" ' + getInitialUNICODEvsSYMBOLunicode() + ' />');
- </script>
- ∉
- </td>
- </tr>
-</table>
-</div>
-
-
-<div id="centered">
-<h1><a onClick="refreshLinks();" href="" target="_top"><script>if (top.location.search == '') document.write('ENTER THE LIBRARY'); else document.write('RETURN TO THE LIBRARY');</script></a></h1>
-</div>
-</body>
-</html>
-
+++ /dev/null
-<html>
-
-<frameset rows="75%,*">
- <frame src="control.html" name="control"/>
- <frame src="welcome.html" name="result"/>
-</frameset>
-
-</html>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<!--
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
--->
-
-<html xmlns:subst="http://www.cs.unibo.it/helm/subst">
-<head>
-<title>Control panel</title>
-<!-- Note: <subst:script/> are substitued by the stylesheet with <script /> -->
-<!-- after changing @src in the concatenation of the interface URL with @src -->
-<subst:script language="JavaScript" src="/javascript/defaults.js" />
-<subst:script language="JavaScript" src="/javascript/utils.js" />
-<subst:script language="JavaScript" src="/javascript/control.js" />
-</head>
-<body bgcolor="#ffffff" text="#000000">
-<form>
-<table>
- <tr>
- <td>
- <b>Format</b>:
- </td>
- <td>
- <select name="output" onChange="updateOutput(this,document.forms[0].format)">
- <script>
- var mode = getParam2('mode');
- var mode_list = mode.split(',');
- outputOption(document, "processed", "Processed", mode_list[0]);
- outputOption(document, "raw", "Raw", mode_list[0]);
- </script>
- </select>
- </td>
- <td>
- <select name="format" onChange="updateFormat(this)">
- <script>
- var mode = getParam2('mode');
- var mode_list = mode.split(',');
- if (mode_list[0] == "raw") {
- outputOption(document, "cic", "CIC", mode_list[1]);
- outputOption(document, "types", "TYPES", mode_list[1]);
- outputOption(document, "ann", "ANN", mode_list[1]);
- outputOption(document, "fwd", "RDF: Forward pointers", mode_list[1]);
- outputOption(document, "bwd", "RDF: Backward pointers", mode_list[1]);
- } else {
- outputOption(document, "html", "HTML", mode_list[2]);
- outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
- outputOption(document, "mml_pres", "MathML Presentation", mode_list[2]);
- }
- </script>
- </select>
- </td>
- <td>
- <script>
- var processorURL = '<subst:processorURL/>';
- var interfaceURL = '<subst:interfaceURL/>';
- var profile = '<subst:profile/>';
-<![CDATA[
- document.write('<a target="_top" href="" ' +
- 'onClick="refreshReload(profile,processorURL,interfaceURL)">Reload</a>');
-]]>
- </script>
- <br />
- (do it also before attempting to take a link to the current page)
- <script>
-<![CDATA[
- top.mode = getParam2('mode');
- top.cicuri = getParam2('cicuri');
- top.theoryuri = getParam2('theoryuri');
-]]>
- </script>
- </td>
- </tr>
- <tr>
- <td colspan="3">
- <script>
-<![CDATA[
- var mode = getParam2('mode');
- var mode_list = mode.split(',');
- if (mode_list[0] == "raw") {
- outputCheckbox(document, "updateCompressed(this)",
- " Compressed", mode_list[5] == "gz");
- outputCheckbox(document, "updateDTDPatched(this)",
- " Resolve DTD URL", mode_list[6] == "yes");
- } else {
- outputCheckbox(document, "updateNatural(this)",
- " Natural Language", mode_list[3] == "yes");
- outputCheckbox(document, "updateAnnotations(this)",
- " Annotations", mode_list[4] == "yes");
- }
-]]>
- </script>
- </td>
- <td>
- <script>
-<![CDATA[
- document.write('<a target="_top" href=""' +
- ' onClick="refreshReload(profile,processorURL,interfaceURL)">Configuration Panel</a>');
-]]>
- </script>
- <br />
- </td>
- </tr>
-</table>
-</form>
-</body>
-</html>
+++ /dev/null
-<!--
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
--->
-<html xmlns:helm="http://www.cs.unibo.it/helm">
-<head>
-<title>Control panel</title>
-</head>
-<body bgcolor="#ffffff" text="#000000">
-<table width="100%">
-<tr>
- <td width="50%">
- <font size="+3" face="Helvetica,Arial,sans-serif"><b>Index of <helm:getParam name="uri"/></b></font>
- <hr noshade="yes" align="left" width="80%"/>
- </td>
-</tr>
-</table>
-</body>
-</html>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-<!--
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
--->
-
-<html xmlns:subst="http://www.cs.unibo.it/helm/subst">
-<head>
-<!-- Note: <subst:script/> are substitued by the stylesheet with <script /> -->
-<!-- after changing @src in the concatenation of the interface URL with @src -->
-<subst:script language="JavaScript" src="/javascript/defaults.js" />
-<subst:script language="JavaScript" src="/javascript/utils.js" />
-<title>Index</title>
-</head>
-<script>
- var topurl = "<subst:interfaceURL/>";
- var getterURL = "<subst:getterURL/>";
- var processorURL = "<subst:processorURL/>";
- var profile = "<subst:profile/>";
-<![CDATA[
- document.write('<frameset rows="18%,*" border="0" scrolling="no">');
- var control_frame_URL=
- topurl + '/html/library/control.html' +
- '?topurl=' + topurl +
- '&mode=' + getParam2('mode') +
- '&cicuri=' + getParam2('cicuri') +
- '&theoryuri=' + getParam2('theoryuri');
- var escaped_control_frame_URL = escape(control_frame_URL);
- document.write('<frame src="' +
- processorURL + 'apply' +
- '?keys=RT' +
- '&profile=' + profile +
- '¶m.profile=' + profile +
- '¶m.topurl=' + topurl +
- '&xmluri=' + escaped_control_frame_URL + '" name="control"/>');
- document.write('<frameset cols="50%,50%" border="0" scrolling="no">');
- document.write('<frameset rows="11%,*" border="0" scrolling="no">');
- document.write('<frame src="' +
- processorURL + 'apply' +
- '?keys=GP' +
- '&profile=' + profile +
- '¶m.profile=' + profile +
- '&xmluri=' + topurl + '/html/library/header.html' +
- '¶m.uri=' + getParam2('theoryuri') +
- '" name="theoryheader"/>');
- document.write('<frame src="' +
- processorURL + 'apply' +
- '?keys=L2H' +
- '&profile=' + profile +
- '¶m.profile=' + profile +
- '&xmluri=' + escape(getterURL + 'ls?format=xml&baseuri=' + getParam2('theoryuri')) +
- '¶m.keys=L2H' +
- '¶m.uri=' + getParam2('theoryuri') +
- '¶m.target=theory' +
- '" name="theoryresult"/>');
- document.write('</frameset>');
- document.write('<frameset rows="11%,*" border="0" scrolling="no">');
- document.write('<frame src="' +
- processorURL + 'apply' +
- '?keys=GP' +
- '&profile=' + profile +
- '¶m.profile=' + profile +
- '&xmluri=' + topurl + '/html/library/header.html' +
- '¶m.uri=' + getParam2('cicuri') +
- '" name="cicheader"/>');
- document.write('<frame src="' +
- processorURL + 'apply' +
- '?keys=L2H' +
- '&profile=' + profile +
- '¶m.profile=' + profile +
- '&xmluri=' + escape(getterURL + 'ls?format=xml&baseuri=' + getParam2('cicuri')) +
- '¶m.keys=L2H' +
- '¶m.uri=' + getParam2('cicuri') +
- '¶m.target=cic' +
- '" name="cicresult"/>');
- document.write('</frameset>');
- document.write('</frameset>');
- document.write('</frameset>');
-]]>
-</script>
-
-</html>
+++ /dev/null
-<html>
-
-<body bgcolor="white">
-</body>
-
-</html>
+++ /dev/null
-<?xml version="1.0"?>
-
-
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-
-<xsl:import href="utils.xsl"/>
-
-<xsl:output method="html" encoding="iso-8859-1"/>
-
-<!-- uri must end with '/' -->
-<xsl:param name="uri" select="''"/>
-<xsl:param name="keys" select="''"/>
-<xsl:param name="processorURL" select="''"/>
-<xsl:param name="getterURL" select="''"/>
-<xsl:param name="interfaceURL" select="''"/>
-<xsl:param name="target" select="''"/>
-<xsl:param name="profile" select="''"/>
-
-<xsl:template name="chop">
- <xsl:param name="uri" select="''"/>
- <xsl:param name="prefix" select="''"/>
- <xsl:variable name="newprefix" select="substring-before($uri,'/')"/>
- <xsl:choose>
- <xsl:when test="$newprefix = ''"><xsl:value-of select="$prefix"/></xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="chop">
- <xsl:with-param name="uri" select="substring-after($uri,'/')"/>
- <xsl:with-param name="prefix" select="concat($prefix,$newprefix,'/')"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:variable name="uridotdot">
- <xsl:call-template name="chop">
- <xsl:with-param name="uri" select="substring($uri,1,string-length($uri)-1)"/>
- </xsl:call-template>
-</xsl:variable>
-
-<xsl:template name="makeDir">
- <xsl:param name="uri" select="''"/>
- <xsl:param name="basename" select="''"/>
- <xsl:param name="icon" select="''"/>
- <xsl:param name="alt" select="''"/>
- <tr>
- <td>
- <img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{$alt}]"/>
- </td>
- <td>
- <xsl:variable name="quoteduri">
- <xsl:call-template name="jsquote">
- <xsl:with-param name="s" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <a
- onClick=
- "top.{$target}uri='{$quoteduri}';
- refresh{$target}Header('{$interfaceURL}/html/library/header.html');
- var search='?keys={$keys}' +
- '&profile={$profile}' +
- '&param.profile={$profile}' +
- '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$quoteduri}')+
- '&param.uri={$quoteduri}' +
- '&param.keys={$keys}' +
- '&param.target={$target}';
- var pathname = this.pathname;
- if (pathname.charAt(0) != '/')
- pathname = '/' + pathname;
- this.href=
- this.protocol + '//' + this.host + pathname + search + this.hash;"
- onMouseOver="window.status='{$quoteduri}'; return true"
- href="apply"
- ><xsl:value-of select="$basename"/></a>
- </td>
- </tr>
-</xsl:template>
-
-<xsl:template match="/">
- <html>
- <head>
- <title>Index of <xsl:value-of select="$uri"/></title>
- <xsl:copy-of select="document(concat($interfaceURL,'/javascript/control.js_xml'))" />
- <xsl:copy-of select="document(concat($interfaceURL,'/javascript/utils.js_xml'))" />
- </head>
- <body bgcolor="#ffffff" text="#000000">
- <table>
- <xsl:if test="$uridotdot != ''">
- <xsl:call-template name="makeDir">
- <xsl:with-param name="uri" select="$uridotdot"/>
- <xsl:with-param name="basename" select="'Parent Directory'"/>
- <xsl:with-param name="icon" select="'back.gif'"/>
- <xsl:with-param name="alt" select="'Parent Directory'"/>
- </xsl:call-template>
- </xsl:if>
- <xsl:apply-templates select="*"/>
- </table>
- <hr noshade="yes" align="left" width="80%"/>
- </body>
- </html>
-</xsl:template>
-
-<xsl:template match="section">
- <xsl:variable name="diruri">
- <xsl:value-of select="."/>
- </xsl:variable>
- <xsl:call-template name="makeDir">
- <xsl:with-param name="uri" select="concat($uri,$diruri,'/')"/>
- <xsl:with-param name="basename" select="$diruri"/>
- <xsl:with-param name="icon" select="'folder.gif'"/>
- <xsl:with-param name="alt" select="$uri"/>
- </xsl:call-template>
-</xsl:template>
-
-<xsl:template match="object">
- <xsl:variable name="name" select="@name"/>
- <xsl:variable name="ann" select="ann/@value"/>
- <xsl:variable name="types" select="types/@value"/>
- <xsl:variable name="body" select="body/@value"/>
- <xsl:variable name="proof_tree" select="proof_tree/@value"/>
- <xsl:variable name="icon">
- <xsl:choose>
- <xsl:when test="$ann = 'YES'">text.gif</xsl:when>
- <xsl:otherwise>generic.red.gif</xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
- <tr>
- <td>
- <img border="0" src="{concat($interfaceURL,'/icons/',$icon)}" alt="[{@name}]"/>
- </td>
- <td>
- <xsl:variable name="quoteduri">
- <xsl:call-template name="jsquote">
- <xsl:with-param name="s" select="$uri"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:variable name="quotedname">
- <xsl:call-template name="jsquote">
- <xsl:with-param name="s" select="$name"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:variable name="quotedbodyname">
- <xsl:call-template name="jsquote">
- <xsl:with-param name="s" select="concat($name,'.body')"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:variable name="quotedprooftreename">
- <xsl:call-template name="jsquote">
- <xsl:with-param name="s" select="concat($name,'.proof_tree')"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:value-of select="$name"/>
- <xsl:text> </xsl:text>
- <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedname)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'));"
- onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
- >
- <xsl:choose>
- <xsl:when test="not($body='NO')">Statement</xsl:when>
- <xsl:otherwise>Definition</xsl:otherwise>
- </xsl:choose>
- </a>
- <xsl:if test="not($body='NO')">
- <xsl:text> </xsl:text>
- <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedbodyname)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'))"
- onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
- >Proof term</a>
- </xsl:if>
- <xsl:if test="not($proof_tree='NO')">
- <xsl:text> </xsl:text>
- <a href="javascript: var _ = window.open(top.frames[0].makeURL('{$target}','{concat($quoteduri,$quotedprooftreename)}','{$ann}','{$types}','{$profile}','{$processorURL}','{$interfaceURL}','{$getterURL}'))"
- onMouseOver="window.status='{concat($quoteduri,$quotedname)}'; return true"
- >Proof tree</a>
- </xsl:if>
- </td>
- </tr>
-</xsl:template>
-
-</xsl:stylesheet>
projects / helm.git / commitdiff