proofcheckerURL configuration parameter added

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index dba30d5aa869ee570e215360ddc03c6157408c68..470f82322ea2025f243a3e5069b6295231da6ab4 100644 (file)
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -64,8 +64,9 @@ td.back { background-color: #e6e6fa; color: brown }
    <td>
     <script>
      var url = unescape(getParam('url'));
+     var proofcheckerURL = unescape(extractParam(url,'param.proofcheckerURL'));
      var CICURI = extractParam(url,'param.CICURI');
-     url = "http://phd.cs.unibo.it:8085/proofCheck?uri=" + CICURI;
+     url = proofcheckerURL + "proofCheck?uri=" + CICURI;
      document.write(
       '<a target="proofChecker" href="' + url + '">Proof-check it</a>'
      );

diff --git a/helm/on-line/html/control.html b/helm/on-line/html/control.html
index 08840663cd5f361996b61e7b6aa568ce1ab3fc53..1e07c108fa52fa66b6c7eab1a2773285ba280ff9 100644 (file)
--- a/helm/on-line/html/control.html
+++ b/helm/on-line/html/control.html
@@ -63,6 +63,7 @@ and
         <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>
@@ -96,6 +97,7 @@ and
         <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>
@@ -112,6 +114,40 @@ and
 
 <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">Graph Drawer URL</th>
@@ -129,6 +165,7 @@ and
         <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>
@@ -162,6 +199,7 @@ and
         <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>

diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html
index 501e1d02883e2746331df021d4b908a30d600b28..72c13b65f63bc4ab03de914953b392b58e830eee 100644 (file)
--- a/helm/on-line/html/library/control.html
+++ b/helm/on-line/html/library/control.html
@@ -62,6 +62,7 @@
 <![CDATA[
        top.processorURL = getParam2('processorURL');
        top.getterURL = getParam2('getterURL');
+       top.proofcheckerURL = getParam2('proofcheckerURL');
        top.draw_graphURL = getParam2('draw_graphURL');
        top.uri_set_queueURL = getParam2('uri_set_queueURL');
        top.UNICODEvsSYMBOL = getParam2('UNICODEvsSYMBOL');

diff --git a/helm/on-line/html/library/index.html b/helm/on-line/html/library/index.html
index 16ca2a00f9eb4c158169df043839d0a150e5aaf3..4f1be5faac96722d62bd4e524ea6e528284a63e0 100644 (file)
--- a/helm/on-line/html/library/index.html
+++ b/helm/on-line/html/library/index.html
@@ -23,6 +23,7 @@
        '&theoryuri=' + getParam2('theoryuri') +
        '&processorURL=' + getParam2('processorURL') +
        '&getterURL=' + getParam2('getterURL') +
+       '&proofcheckerURL=' + getParam2('proofcheckerURL') +
        '&draw_graphURL=' + getParam2('draw_graphURL') +
        '&uri_set_queueURL=' + getParam2('uri_set_queueURL') +
        '&UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL');
@@ -48,6 +49,7 @@
         '&param.keys=L2H' +
        '&param.uri=' + getParam2('theoryuri') +
        '&param.getterURL=' + getParam2('getterURL') +
+       '&param.proofcheckerURL=' + getParam2('proofcheckerURL') +
        '&param.draw_graphURL=' + getParam2('draw_graphURL') +
        '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
        '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +
@@ -71,6 +73,7 @@
         '&param.keys=L2H' +
        '&param.uri=' + getParam2('cicuri') +
        '&param.getterURL=' + getParam2('getterURL') +
+       '&param.proofcheckerURL=' + getParam2('proofcheckerURL') +
        '&param.draw_graphURL=' + getParam2('draw_graphURL') +
        '&param.uri_set_queueURL='+getParam2('uri_set_queueURL') +
        '&param.UNICODEvsSYMBOL=' + getParam2('UNICODEvsSYMBOL') +

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 6734d4a133f5e6fc9ab60961b87fae73995bfc3a..d49da35ba42c81d687d55c431b919bf47ecb0f5c 100644 (file)
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -22,11 +22,12 @@ function updateOutput(output,format)
   var topurl = top.topurl;
   var processorURL = top.processorURL;
   var getterURL = top.getterURL;
+  var proofcheckerURL = top.proofcheckerURL;
   var draw_graphURL = top.draw_graphURL;
   var uri_set_queueURL = top.uri_set_queueURL;
   var mode_list = mode.split(",");
   var new_mode = output.options[output.selectedIndex].value;
-  var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&draw_graphURL=" + draw_graphURL + "&uri_set_queueURL=" + uri_set_queueURL + "&mode=";
+  var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&proofcheckerURL=" + proofcheckerURL + "&draw_graphURL=" + draw_graphURL + "&uri_set_queueURL=" + uri_set_queueURL + "&mode=";
   
   if (new_mode != mode_list[0]) {
     updateMode(0, new_mode);
@@ -94,6 +95,7 @@ function refreshReload()
       "&theoryuri=" + top.theoryuri +
       "&processorURL=" + top.processorURL +
       "&getterURL=" + top.getterURL +
+      "&proofcheckerURL=" + top.proofcheckerURL +
       "&draw_graphURL=" + top.draw_graphURL +
       "&uri_set_queueURL=" + top.uri_set_queueURL +
       "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL;
@@ -149,6 +151,7 @@ function makeURL(type,uri,cicflags,typesflags)
   var mode = top.mode;
   var processorURL = top.processorURL;
   var getterURL = top.getterURL;
+  var proofcheckerURL = top.proofcheckerURL;
   var draw_graphURL = top.draw_graphURL;
   var uri_set_queueURL = top.uri_set_queueURL;
   var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
@@ -179,6 +182,7 @@ function makeURL(type,uri,cicflags,typesflags)
       keys = getCICHTMLKeys() +
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.proofcheckerURL=" + escape(proofcheckerURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
@@ -194,6 +198,7 @@ function makeURL(type,uri,cicflags,typesflags)
       keys = getTheoryKeys()+
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.proofcheckerURL=" + escape(proofcheckerURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
@@ -223,6 +228,7 @@ function makeURL(type,uri,cicflags,typesflags)
 
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.proofcheckerURL=" + escape(proofcheckerURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&param.doctype-public=" +
@@ -236,6 +242,7 @@ function makeURL(type,uri,cicflags,typesflags)
       keys = getCICMathMLKeys()+
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.proofcheckerURL=" + escape(proofcheckerURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&prop.doctype-public="+
@@ -253,6 +260,7 @@ function makeURL(type,uri,cicflags,typesflags)
        "&param.embedkeys=" + escape("d_c,TC1,G,C2,L") +
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.proofcheckerURL=" + escape(proofcheckerURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&param.doctype-public=" +

diff --git a/helm/on-line/javascript/defaults.js b/helm/on-line/javascript/defaults.js
index db3172cfea6986ab1accbbe5d2b41f3bc8f97bf8..98dfed1c249de93dd45acc9788de14dfc486f6d2 100644 (file)
--- a/helm/on-line/javascript/defaults.js
+++ b/helm/on-line/javascript/defaults.js
@@ -10,6 +10,8 @@ function getDefaultParam(name)
     return "http://phd.cs.unibo.it:8083/"; 
   case "uri_set_queueURL":
     return "http://phd.cs.unibo.it:8084/"; 
+  case "proofcheckerURL":
+    return "http://mowgli.cs.unibo.it:48084/"; 
   case "UNICODEvsSYMBOL":
     return "symbol";
   case "cicuri":

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
index f319735038448a6d956367e7a2eaba9871329d13..26bd4978b0e555e6c07f7b398a9364b4801d72c7 100644 (file)
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -27,6 +27,21 @@ function getInitialGetterURL()
   return getterURL;
 }
 
+function getInitialProofCheckerURL()
+{
+  var search = top.location.search;
+  search = search.slice(1);
+  var args = search.split("&");
+  var proofcheckerURL = "-1";
+  for (var i = 0 ; i < args.length ; i++) {
+     var couple = args[i].split("=");
+     if (couple[0] == "proofcheckerURL") proofcheckerURL = couple[1];
+  }
+  if (proofcheckerURL == "-1")
+     proofcheckerURL = getDefaultParam("proofcheckerURL");
+  return proofcheckerURL;
+}
+
 function getInitialDrawGraphURL()
 {
   var search = top.location.search;
@@ -95,6 +110,11 @@ function getGetterURL()
   return document.getterURL.elements[0].value;
 }
 
+function getProofCheckerURL()
+{
+  return document.proofcheckerURL.elements[0].value;
+}
+
 function getDrawGraphURL()
 {
   return document.draw_graphURL.elements[0].value;
@@ -166,6 +186,7 @@ function refreshLinks()
        "&mode=" + mode +
        "&processorURL=" + getUwoboURL() +
        "&getterURL=" + getGetterURL() +
+       "&proofcheckerURL=" + getProofCheckerURL() +
        "&draw_graphURL=" + getDrawGraphURL() +
        "&uri_set_queueURL=" + getURISetQueueURL() +
        "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL()
@@ -177,7 +198,7 @@ function selectUwoboURL(ss)
   if (ss.selectedIndex == 0) {
     document.uwoboURL.elements[0].value = "";
   } else {
-    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
+    document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/helm/servlet/uwobo/";
   }
 
   refreshLinks();
@@ -188,7 +209,18 @@ function selectGetterURL(ss)
   if (ss.selectedIndex == 0) {
     document.getterURL.elements[0].value = "";
   } else {
-    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
+    document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":48081/";
+  }
+
+  refreshLinks();
+}
+
+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/";
   }
 
   refreshLinks();