]> matita.cs.unibo.it Git - helm.git/commitdiff
New HELM interface almost stable.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 27 May 2004 17:27:52 +0000 (17:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 27 May 2004 17:27:52 +0000 (17:27 +0000)
14 files changed:
helm/on-line/html/cic/control.html
helm/on-line/html/cic/index.html
helm/on-line/html/configuration.html [new file with mode: 0644]
helm/on-line/html/folder/control.html
helm/on-line/html/folder/index.html
helm/on-line/html/theory/control.html
helm/on-line/html/theory/index.html
helm/on-line/javascript/control.js
helm/on-line/javascript/prelude.js
helm/on-line/xslt/ls2theory.xsl
helm/on-line/xslt/makeGraphLinks.xsl
helm/on-line/xslt/resolve_topurl.xsl
helm/on-line/xslt/substKey.xsl [new file with mode: 0644]
helm/on-line/xslt/toplevel_header.xsl

index 3dc908db5d210504b82c10707f52fb713f193197..d22499a4078c75f1506793299d2a8cd681f60758 100644 (file)
@@ -12,6 +12,7 @@ td.back { background-color: #e6e6fa; color: brown }
 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>
@@ -38,12 +39,29 @@ div.center { text-align: center }
 </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&amp;param.processorURL=' + escape(processorURL) +
+     '&amp;param.profile=' + escape(profile) +
+     '&amp;xmluri=' + interfaceURL + 'html/configuration.html' +
+     '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
  <div class="center">
    <script>
      document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
      document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/object.png" />');
    </script>
-  <h2><subst:base_CICURI/></h2>
+  <h2 class="uri"><subst:base_CICURI/></h2>
   <script>document.write('&lt;/a>');</script>
  </div>
  <hr />
@@ -60,13 +78,12 @@ div.center { text-align: center }
   </li>
 -->
   <li>
-    View [
+    View
     <script>
-     document.write('<a href="' + HTMLURL + '&amp;param.toplevel=true" target="result"><small>HTML</small></a>');
-     document.write(' / ');
-     document.write('<a href="' + MathMLPresentationURL + '&amp;param.toplevel=true" target="result"><small>MathML</small></a>');
+     document.write('<a href="' + HTMLURL + '&amp;param.toplevel=true" target="result"><small>HTML</small></a>');
+     document.write(' | ');
+     document.write('<a href="' + MathMLPresentationURL + '&amp;param.toplevel=true" target="result"><small>MathML</small></a> ]');
      </script>
-     ]
   </li>
   <li>
     <script>
@@ -161,9 +178,5 @@ div.center { text-align: center }
     </ul>
   </li>
 </ul>
-<hr />
-<div class="center">
-  <a href="http://helm.cs.unibo.it" target="_top">HELM home</a>
-</div>
 </body>
 </html>
index 3cf555534cbafa92b128beb55e94d536ede91b5a..ff3b7ba2077ce31c479dc0c0e23f4211707d1202 100644 (file)
  var url = "<subst:makeURL/>";
 <![CDATA[
   document.write('<frameset cols="20%,*" border="1">');
-  document.write('<frame src="' + processorURL + 'apply?keys=RT&profile=' +
-    profile + '&param.profile=' + profile + '&param.annotations=' + annotations +
-    '&param.CICURI=' + CICURI + '&param.url=' + escape(url) + '&xmluri=' +
+  document.write('<frame src="' + processorURL +
+    'apply?keys=SPK%2CRT&profile=' + profile + '&param.profile=' + profile +
+    '&param.annotations=' + annotations + '&param.CICURI=' +
+    CICURI + '&param.url=' + escape(url) + '&xmluri=' +
     escape(interfaceURL + 'html/cic/control.html') +'"/>');
   document.write('<frame src="' + url + '&param.toplevel=true" name="result"/>');
   document.write('</frameset>');
diff --git a/helm/on-line/html/configuration.html b/helm/on-line/html/configuration.html
new file mode 100644 (file)
index 0000000..3139d63
--- /dev/null
@@ -0,0 +1,324 @@
+<?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">
+&#xa0;
+</script>
+<script language="JavaScript" src="http://helm.cs.unibo.it/helm/javascript/prelude.js">
+&#xa0;
+</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')"/>
+       &#xa0;&#xa0;
+       [<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')"/>
+       &#xa0;&#xa0;
+       [<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">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>
+</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 &quot;symbol&quot; font.
+   </td>
+  </tr>
+  <tr>
+   <td>
+    To make us understand what kind of browser you have, please
+    select below the symbol for &quot;not belongs to&quot;. 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 &quot;not belongs to&quot; 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">&#207;</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>
+      &#8713;
+      </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>
+
index 34a2f95233426792d39071223b9232fdf384e060..a3d6c0fedcefbeb8f89446889609fbd597eb6e51 100644 (file)
@@ -12,31 +12,44 @@ td.back { background-color: #e6e6fa; color: brown }
 #centered { text-align: center }
 li     { padding-bottom: 1ex }
 div.center { text-align: center }
+h2.uri { margin-top: 0ex; margin-bottom: 0ex }
 </style>
 
-<script language="JavaScript" src="../../javascript/defaults.js"></script>
-<script language="JavaScript" src="../../javascript/utils.js"></script>
-<script language="JavaScript" src="../../javascript/control.js"></script>
 <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&amp;param.processorURL=' + escape(processorURL) +
+     '&amp;param.profile=' + escape(profile) +
+     '&amp;xmluri=' + interfaceURL + 'html/configuration.html' +
+     '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
  <div class="center">
    <script>
      document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
      document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/folder.png" />');
    </script>
- <h2><subst:base_CICURI/></h2>
+ <h2 class="uri"><subst:base_CICURI/></h2>
   <script>document.write('&lt;/a>');</script>
  </div>
- <hr />
- <div class="center">
-  <a href="http://helm.cs.unibo.it" target="_top">HELM home</a>
- </div>
 <!--
  <ul>
    <li>
index 4c50442bd0f170ebd7ccf567692380fdd689fbae..afa6b8935478e88fc05c43ab2f1e82c80e0be9f3 100644 (file)
@@ -13,8 +13,9 @@
  var url = "<subst:makeTheoryURL/>";
 <![CDATA[
   document.write('<frameset cols="20%,*" border="1" >');
-  document.write('<frame src="' + processorURL + 'apply?keys=RT&profile=' +
-    profile + '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
+  document.write('<frame src="' + processorURL +
+    'apply?keys=SPK%2CRT&profile=' + profile + '&param.profile=' + profile +
+    '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
     '&param.url=' + escape(url) + '&xmluri=' +
     escape(interfaceURL + 'html/folder/control.html') +'"/>');
   document.write('<frame src="' + url + '&param.toplevel=true" name="result"/>');
index ffc2e82d224fc9e0b5b9591d206161b105546d03..1602a6985ca288e86107f3b9aefdf1f944ccb93c 100644 (file)
@@ -12,6 +12,7 @@ td.back { background-color: #e6e6fa; color: brown }
 #centered { text-align: center }
 li     { padding-bottom: 1ex }
 div.center { text-align: center }
+h2.uri { margin-top: 0ex; margin-bottom: 0ex }
 </style>
 
 <script language="JavaScript" src="../../javascript/defaults.js"></script>
@@ -19,24 +20,39 @@ div.center { text-align: center }
 <script language="JavaScript" src="../../javascript/control.js"></script>
 <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&amp;param.processorURL=' + escape(processorURL) +
+     '&amp;param.profile=' + escape(profile) +
+     '&amp;xmluri=' + interfaceURL + 'html/configuration.html' +
+     '">configuration</a>]');
+ </script>
+ </small>
+ </div>
+ <hr />
  <div class="center">
    <script>
      document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
      document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/theory.png" />');
    </script>
- <h2><subst:base_CICURI/></h2>
+ <h2 class="uri"><subst:base_CICURI/></h2>
   <script>document.write('&lt;/a>');</script>
  </div>
- <hr />
- <div class="center">
-  <a href="http://helm.cs.unibo.it" target="_top">HELM home</a>
- </div>
 <!--
  <ul>
    <li>
index 5159f9830512b14814d7b228a8505181d6bd58c7..98b2ed61f5ff739b151d816dbb508957e2924cb3 100644 (file)
@@ -13,8 +13,9 @@
  var url = "<subst:makeTheoryURL/>";
 <![CDATA[
   document.write('<frameset cols="20%,*" border="1" >');
-  document.write('<frame src="' + processorURL + 'apply?keys=RT&profile=' +
-    profile + '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
+  document.write('<frame src="' + processorURL +
+    'apply?keys=SPK&2CRT&profile=' + profile + '&param.profile=' + profile +
+    '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
     '&param.url=' + escape(url) + '&xmluri=' +
     escape(interfaceURL + 'html/theory/control.html') +'"/>');
   document.write('<frame src="' + url + '&param.toplevel=true" name="result"/>');
index bc52d02b617d6a2948d56b65dcaf4d103528d862..0e6e566a05d46f4049a9ebeeef6265c713f813ce 100644 (file)
@@ -258,3 +258,4 @@ function makeURL(type,uri,cicflags,typesflags,profile,processorURL,interfaceURL,
   else if (type == "theory")
    return processorURL + "apply?keys=RT&xmluri=" + escape(thinterfaceURLidx) + "&param.ignore=" + keys + "&param.CICURI=" + uri;
 }
+
index 83cff42bc5d2541db61bc284aaff3a50a0166093..fc3b2470e51749b0f2553fabb5f3d733321c6f02 100644 (file)
@@ -84,21 +84,26 @@ function getInitialUNICODEvsSYMBOL()
   return UNICODEvsSYMBOL;
 }
 
-function getInitialUNICODEvsSYMBOLsymbol()
+function getInitialUNICODEvsSYMBOLsymbol(defaultValue)
 {
-  if (getInitialUNICODEvsSYMBOL() == "symbol")
+  if (defaultValue == "symbol")
    return "CHECKED";
   else
    return "";
 }
 
-function getInitialUNICODEvsSYMBOLunicode()
+function getInitialUNICODEvsSYMBOLunicode(defaultValue)
 {
-  if (getInitialUNICODEvsSYMBOL() == "unicode")
+  if (defaultValue == "unicode")
    return "CHECKED";
   else
    return "";
 }
+function getProfileId()
+{
+  return document.profile.elements[0].value;
+}
 
 function getUwoboURL()
 {
@@ -125,12 +130,43 @@ function getURISetQueueURL()
   return document.uri_set_queueURL.elements[0].value;
 }
 
+function getRdflyURL()
+{
+  return document.rdflyURL.elements[0].value;
+}
+
 function getUNICODEvsSYMBOL()
 {
   if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
-   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
+   return 'symbol';
+  else
+   return 'unicode';
+}
+
+function getNaturalLanguage()
+{
+  if (document.naturalLanguage.elements[0].checked)
+   return 'yes';
   else
-   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
+   return 'no';
+}
+
+function getMaxGraphSize()
+{
+  return document.maxGraphSize.elements[0].value;
+}
+
+function getUpdateURL()
+{
+  return '&param.processorURL=' + escape(getUwoboURL()) +
+    '&param.getterURL=' + escape(getGetterURL()) +
+    '&param.uri_set_queueURL=' + escape(getURISetQueueURL()) +
+    '&param.draw_graphURL=' + escape(getDrawGraphURL()) +
+    '&param.proofcheckerURL=' + escape(getProofCheckerURL()) +
+    '&param.rdflyURL=' + escape(getRdflyURL()) +
+    '&param.naturalLanguage=' + escape(getNaturalLanguage()) +
+    '&param.uri_set_size=' + escape(getMaxGraphSize()) +
+    '&param.UNICODEvsSYMBOL=' + escape(getUNICODEvsSYMBOL());
 }
 
 function chopSlash(url)
@@ -198,10 +234,8 @@ function selectUwoboURL(ss)
   if (ss.selectedIndex == 0) {
     document.uwoboURL.elements[0].value = "";
   } else {
-    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/helm/servlet/uwobo/";
+    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58080/";
   }
-
-  refreshLinks();
 }
 
 function selectGetterURL(ss)
@@ -209,10 +243,8 @@ function selectGetterURL(ss)
   if (ss.selectedIndex == 0) {
     document.getterURL.elements[0].value = "";
   } else {
-    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48081/";
+    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58081/";
   }
-
-  refreshLinks();
 }
 
 function selectProofCheckerURL(ss)
@@ -220,10 +252,8 @@ function selectProofCheckerURL(ss)
   if (ss.selectedIndex == 0) {
     document.proofcheckerURL.elements[0].value = "";
   } else {
-    document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48084/";
+    document.proofcheckerURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58084/";
   }
-
-  refreshLinks();
 }
 
 function selectDrawGraphURL(ss)
@@ -231,10 +261,8 @@ 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 + ":48083/";
+    document.draw_graphURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":58083/";
   }
-
-  refreshLinks();
 }
 
 function selectURISetQueueURL(ss)
@@ -242,8 +270,41 @@ 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 + ":48082/";
+    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 selectProfile(ss, interfaceURL)
+{
+  location = getUwoboURL() +
+    'apply?keys=SPK&param.processorURL=' + escape(getUwoboURL()) +
+    '&param.profile=' + escape(ss.options[ss.selectedIndex].value) +
+    '&xmluri=' + escape(interfaceURL + 'html/configuration.html');
+}
 
-  refreshLinks();
+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();
+  }
 }
+
index 5e221bd07f0b8472d18ecb368194f678f556632c..6ecf569865bb071ac6064aca39834f7305225d0a 100644 (file)
            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>
+         <!-- sorting: folders interleaved with theories, then objects-->
+         <xsl:apply-templates
+           select="section|object[substring-after(@name,'.')='theory']">
+           <xsl:sort select="concat(@name,string(.))" />
+         </xsl:apply-templates>
+         <xsl:apply-templates
+           select="object[not(substring-after(@name,'.')='theory')]" />
+         <!-- sorting: folders, theories, objects -->
+<!--
          <xsl:apply-templates select="section" />
          <xsl:apply-templates select="object" />
+-->
        </ul>
       </body>
     </html>
index 45e88aa085680a3fdbc961ca0cefd120c449ea07..3cc6566fff92ea8917694653effde1b0015f3ea8 100644 (file)
@@ -78,9 +78,9 @@
     <table bgColor="green" id="pippo">
      <tr><td>
       <table bgColor="cyan" border="2">
-       <tr><td><a href="javascript: var _ = window.open(selectedForwardURL)">Objects this one depends on.</a></td></tr>
+       <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: var _ = window.open(selectedBackwardURL)">Objects depending on this one.</a></td></tr>
+       <tr><td><a href="javascript: location = selectedBackwardURL">Objects depending on this one.</a></td></tr>
       </table>
      </td></tr>
     </table>
index 27651899ef437f0cdbc385f9708e2d963f1d6068..c2ad9e28c132ddc956b14178294d07f7b5353dcd 100644 (file)
  </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: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 name="makeGraphURL">
     <xsl:with-param name="uri" select="$CICURI"/>
     <xsl:with-param name="keys" select="'MDG'"/>
-    <!-- <xsl:with-param name="uri_set_size" select="'document.uri_set_size.elements[0].value'"/> -->
-    <xsl:with-param name="uri_set_size" select="'30'"/>
+    <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
   </xsl:call-template>
 </xsl:template>
 
   <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="'document.uri_set_size.elements[0].value'"/> -->
-    <xsl:with-param name="uri_set_size" select="'30'"/>
+    <xsl:with-param name="uri_set_size" select="$uri_set_size"/>
   </xsl:call-template>
 </xsl:template>
 
diff --git a/helm/on-line/xslt/substKey.xsl b/helm/on-line/xslt/substKey.xsl
new file mode 100644 (file)
index 0000000..a5acc09
--- /dev/null
@@ -0,0 +1,94 @@
+<?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>
index 4ed5731cabffabf5649fa332cda5cec0dae6227b..f20862840dab4622aa99ce09351f0d2af783b811 100644 (file)
 <xsl:template name="add_breadcrumb_trail">
   <xsl:param name="CICURI" select="''"/>
   <xsl:variable name="prefix" select="substring-before($CICURI, ':')" />
-  <html:table width="100%">
-    <html:tr>
-      <html:td>
-       <html:h3 style="font-family: sans-serif">
+  <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, ':')" />
              select="substring($CICURI, string-length($prefix)+3)" />
            <xsl:with-param name="acc" select="concat($prefix, ':/')" />
          </xsl:call-template>
-       </html:h3>
-      </html:td>
-      <html:td style="text-align:right">
+       </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">
-         <html:a href="http://mowgli.cs.unibo.it:58085/getpage?url=index.html&amp;preprocess=true&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=iso-8859-1&amp;param.thencoding=iso-8859-1&amp;param.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.CICURI=dummy:query_result&amp;param.naturalLanguage=yes&amp;param.annotations=no&amp;param.processorURL=http://mowgli.cs.unibo.it:58080/" target="_top">Search</html:a>
-       </html:span>
-      </html:td>
+         [<html:a href="http://mowgli.cs.unibo.it:58085/getpage?url=index.html&amp;preprocess=true&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=iso-8859-1&amp;param.thencoding=iso-8859-1&amp;param.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.CICURI=dummy:query_result&amp;param.naturalLanguage=yes&amp;param.annotations=no&amp;param.processorURL=http://mowgli.cs.unibo.it:58080/" target="_top">search</html:a>]
+       </html:span><xsl:text>
+      </xsl:text>
+      </html:td><xsl:text>
+    </xsl:text>
     </html:tr>
-  </html:table>
+  </html:table><xsl:text>
+  </xsl:text>
   <html:hr />
 </xsl:template>