New: UWOBO profiles added.

diff --git a/helm/uwobo-panel/control.html b/helm/uwobo-panel/control.html
index 5345fa33466762b593164b36fe785ecd2c0e2293..4cb183bdce6c3d7d2bf9e3327be3a388b49e21c7 100644 (file)
--- a/helm/uwobo-panel/control.html
+++ b/helm/uwobo-panel/control.html
@@ -37,6 +37,7 @@ The sections:
   <li><a href="#params">Global Parameters</a></li>
   <li><a href="#sessions">Daemon Management</a></li>
   <li><a href="#queries">Queries</a></li>
+  <li><a href="#profiles">Profiles</a></li>
   <li><a href="#stylesheets">Stylesheet Management</a></li>
   <li><a href="#process">Processing</a></li>
 </ul>
@@ -238,6 +239,152 @@ The following are commands to do some simple queries about the UWOBO service.
 
 </div>
 
+<br />
+<a name="profiles"/>
+<table border="0" width="100%" cellpadding="4" cellspacing="0">
+<tr>
+  <td class="head" align="left"><big>Profiles</big></td>
+  <td class="back" align="right"><a href="#top">top</a></td>
+</tr>
+</table>
+
+<div id="indent">
+
+<br />
+
+The following are commands to list and edit the UWOBO profiles.
+
+<br /><br />
+
+<p><em>List existent profiles.</em></p>
+<table border="0">
+<tr>
+  <td><form><input type="button" value="List Profiles" onClick="top.result.location.replace(getUwoboURL() + 'listprofiles')"/></form></td>
+</tr>
+</table>
+
+<p><em>Create a new profile.</em></p>
+<table border="0">
+<tr>
+  <th align="left">Name</th>
+  <th align="left">Parent profile</th>
+  <th align="left">Parent profile password</th>
+</tr>
+<tr>
+  <td>
+    <form name="createProfileID">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="createProfileClone">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="createProfilePassword">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form>
+      <input type="button" value="Create Profile" onClick="createProfile()"/>
+    </form>
+  </td>
+</tr>
+</table>
+
+<p><em>Remove a profile.</em></p>
+<table border="0">
+<tr>
+  <th align="left">Name</th>
+  <th align="left">Password</th>
+</tr>
+<tr>
+  <td>
+    <form name="removeProfileID">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="removeProfilePassword">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form>
+      <input type="button" value="Remove Profile" onClick="removeProfile()"/>
+    </form>
+  </td>
+</tr>
+</table>
+
+<p><em>Show profile parameters.</em></p>
+<table border="0">
+<tr>
+  <th align="left">Name</th>
+  <th align="left">Password</th>
+</tr>
+<tr>
+  <td>
+    <form name="getParamsProfileID">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="getParamsProfilePassword">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form>
+      <input type="button" value="Show Params" onClick="getProfileParams()"/>
+    </form>
+  </td>
+</tr>
+</table>
+
+<p><em>Set profile parameters.</em></p>
+<table border="0">
+<tr>
+  <th align="left">Name</th>
+  <th align="left">Password</th>
+  <th align="left">Parameter name</th>
+  <th align="left">Parameter value</th>
+</tr>
+<tr>
+  <td>
+    <form name="setParamProfileID">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="setParamProfilePassword">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="setParamProfileKey">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form name="setParamProfileValue">
+      <input type="text" size="20"/>
+    </form>
+  </td>
+  <td>
+    <form>
+      <input type="button" value="Set Param" onClick="setProfileParam()"/>
+    </form>
+  </td>
+</tr>
+</table>
+
+<br />
+
+</div>
+
 <a name="stylesheets"/>
 <table border="0" width="100%" cellpadding="4" cellspacing="0">
 <tr>
@@ -278,6 +425,7 @@ the getter is used by default (you can deselect it, however):
         <option value="d_c,drop_coercions.xsl,true">Drop implicit coercions</option>
         <option value="meta_theory,mk_meta_theory.xsl,true">Metadata (back-pointers) to theory</option>
         <option value="L2H,ls2html.xsl,true">Getter LS ==&gt; HTML</option>
+       <option value="L2T,ls2theory.xsl,true">Getter LS ==&gt; Theory</option>
         <option value="GP,getParam.xsl,true">Get Param</option>
         <option value="RT,resolve_topurl.xsl,true">Logic-sheet to substitute the interface URL</option>
         <option value="MC,metadataControl.xsl,true">Stylesheet to create links to metadata</option>

diff --git a/helm/uwobo-panel/control.js b/helm/uwobo-panel/control.js
index 393bd3a68d647f01257041a7d91a09673731b9c7..9858fe1400c6d8a53f8a8e27d2b089ca37b33154 100644 (file)
--- a/helm/uwobo-panel/control.js
+++ b/helm/uwobo-panel/control.js
@@ -91,6 +91,44 @@ function selectPredefinedStylesheet(ss)
   document.loadEscape.elements[0].checked = true;
 }
 
+function getProfileParams()
+{
+  var password = document.getParamsProfilePassword.elements[0].value;
+  if (password != "") { password = "&password=" + password; };
+
+  top.result.location.replace(getUwoboURL() + "getparams?id=" + document.getParamsProfileID.elements[0].value + password);
+}
+
+function setProfileParam()
+{
+  var password = document.setParamProfilePassword.elements[0].value;
+  if (password != "") { password = "&password=" + password; };
+
+  top.result.location.replace(getUwoboURL() + "setparam?id=" + document.setParamProfileID.elements[0].value + "&key=" + document.setParamProfileKey.elements[0].value + "&value=" + document.setParamProfileValue.elements[0].value + password);
+}
+
+function createProfile()
+{
+  var id = document.createProfileID.elements[0].value;
+  if (id != "") { id = "&id=" + id; };
+
+  var password = document.createProfilePassword.elements[0].value;
+  if (password != "") { password = "&password=" + password; };
+
+  var clone = document.createProfileClone.elements[0].value;
+  if (clone != "") { clone = "&orig=" + clone; };
+
+  top.result.location.replace(getUwoboURL() + "createprofile?foo=x" + id + password + clone);
+}
+
+function removeProfile()
+{
+  var password = document.removeProfilePassword.elements[0].value;
+  if (password != "") { password = "&password=" + password; };
+
+  top.result.location.replace(getUwoboURL() + "removeprofile?id=" + document.removeProfileID.elements[0].value + password);
+}
+
 function getStylesheetURL()
 {
   var s;