UNICODEvsSYMBOL parameter now added everywhere

diff --git a/helm/on-line/html/control.html b/helm/on-line/html/control.html
index 6e8662db856cfa91ce440afd01d9f87c2376263a..791a8b28a14edabccd73634966cf40b83be80097 100644 (file)
--- a/helm/on-line/html/control.html
+++ b/helm/on-line/html/control.html
@@ -109,8 +109,48 @@ and
     </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>
+      &nbsp;&nbsp;&nbsp;
+      <script>
+       document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="symbol" ' + getInitialUNICODEvsSYMBOLsymbol() + ' />');
+      </script>
+      <font face="symbol">&#207;</font>
+      &nbsp;&nbsp;&nbsp;
+      <script>
+       document.write('<input type="radio" name="radioUNICODEvsSYMBOL" value="unicode" ' + getInitialUNICODEvsSYMBOLunicode() + ' />');
+      </script>
+      &#8713;
+    </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>

diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html
index 57c6c3900e83920432cdbc3f97e61146697fdc41..f70dd94cc9397d6e5a51e71b33ad7ecfe9c1e5d3 100644 (file)
--- a/helm/on-line/html/library/control.html
+++ b/helm/on-line/html/library/control.html
@@ -50,6 +50,7 @@
         '&theoryuri=' + getParam('theoryuri') +
         '&processorURL=' + getParam('processorURL') +
         '&getterURL=' + getParam('getterURL') +
+        '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '" onClick="refreshReload()">Reload</a>');
      </script>
      <br>
@@ -57,6 +58,7 @@
      <script>
        top.processorURL = getParam('processorURL');
        top.getterURL = getParam('getterURL');
+       top.UNICODEvsSYMBOL = getParam('UNICODEvsSYMBOL');
        top.topurl = getParam('topurl');
        top.mode = getParam('mode');
        top.cicuri = getParam('cicuri');
@@ -90,6 +92,7 @@
         '&theoryuri=' + getParam('theoryuri') +
         '&processorURL=' + getParam('processorURL') +
         '&getterURL=' + getParam('getterURL') +
+        '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '" onClick="refreshReload()">Configuration Panel</a>');
      </script>
      <br>

diff --git a/helm/on-line/html/library/index.html b/helm/on-line/html/library/index.html
index fb9afb3e41afe09c197aaae02ef5643aab392c49..2c16dff396383a50201a767af170fd66ee446364 100644 (file)
--- a/helm/on-line/html/library/index.html
+++ b/helm/on-line/html/library/index.html
@@ -15,6 +15,7 @@
        '&theoryuri=' + getParam('theoryuri') +
        '&processorURL=' + getParam('processorURL') +
        '&getterURL=' + getParam('getterURL') +
+       '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
        '" name="control"/>');
   document.write('<frameset cols="50%,50%" border="0" scrolling="no">');
   document.write('<frameset rows="11%,*" border="0" scrolling="no">');
@@ -31,6 +32,7 @@
         '&param.keys=L2H' +
        '&param.uri=' + getParam('theoryuri') +
        '&param.getterURL=' + getParam('getterURL') +
+       '&param.UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '&param.target=theory' +
        '&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
        '" name="theoryresult"/>');
@@ -49,6 +51,7 @@
         '&param.keys=L2H' +
        '&param.uri=' + getParam('cicuri') +
        '&param.getterURL=' + getParam('getterURL') +
+       '&param.UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '&param.target=cic' +
        '&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) +
        '" name="cicresult"/>');

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 8d16150cbd5c499f3425117dbf690ee75c49cd75..a36165f78cd16cdaa8c95a9de5880109f3af8a14 100644 (file)
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -83,7 +83,8 @@ function refreshReload()
       "&cicuri=" + top.cicuri +
       "&theoryuri=" + top.theoryuri +
       "&processorURL=" + top.processorURL +
-      "&getterURL=" + top.getterURL;
+      "&getterURL=" + top.getterURL +
+      "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL;
 
    top.frames[0].document.links[0].search = search;
    top.frames[0].document.links[1].search = search;
@@ -106,7 +107,7 @@ function refreshtheoryHeader(headerURL)
 function getCICMathMLKeys()
 {
   //Important note: do not modify this function without modifying makeURL
-  return escape("C1,G,C2,L");
+  return escape("d_c,C1,G,C2,L");
 }
 
 function makeURL(type,uri,cicflags,typesflags)
@@ -114,6 +115,7 @@ function makeURL(type,uri,cicflags,typesflags)
   var mode = top.mode;
   var processorURL = top.processorURL;
   var getterURL = top.getterURL;
+  var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
   var mode_list = mode.split(",");
   
   var keys = "";
@@ -137,8 +139,9 @@ function makeURL(type,uri,cicflags,typesflags)
     if (format == "html" && type == "cic") {
       //Important note: do not modify this function without modifying
       //getCICMathMLKeys
-      keys = escape("C1,HC2,L")+"&param.processorURL=" + escape(processorURL) +
+      keys = escape("d_c,C1,HC2,L")+"&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
        "&prop.encoding=iso-8859-1" +
        "&prop.media-type=text/html" +
@@ -151,6 +154,7 @@ function makeURL(type,uri,cicflags,typesflags)
       keys = escape("T1,T2,L,E")+
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
+       "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
        "&param.keys=" + escape("C1,HC2,L") +
        "&param.thkeys=" + escape("T1,T2,L,E") +
        "&param.embedkeys=" + escape("TC1,HC2,L") +

diff --git a/helm/on-line/javascript/defaults.js b/helm/on-line/javascript/defaults.js
index 54d51002ff60b7cfccdb7f27e5eff0fb96270dd9..271f6eabcb8e228401685a4a73746e9a82ba9ffe 100644 (file)
--- a/helm/on-line/javascript/defaults.js
+++ b/helm/on-line/javascript/defaults.js
@@ -12,6 +12,8 @@ function getDefaultParam(name)
     return "theory:/";
   case "mode":
     return "processed,cic,html,yes,no,normal,no";
+  case "UNICODEvsSYMBOL":
+    return "symbol";
   }
   
   return "???";

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
index 90e877a01381e934b5caa2e6adfbd5b82afc7fc0..12862e545024b4b116acc010a9f5555063c6667c 100644 (file)
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -27,6 +27,36 @@ function getInitialGetterURL()
   return getterURL;
 }
 
+function getInitialUNICODEvsSYMBOL()
+{
+  var search = top.location.search;
+  search = search.slice(1);
+  var args = search.split("&");
+  var UNICODEvsSYMBOL = "-1";
+  for (var i = 0 ; i < args.length ; i++) {
+     var couple = args[i].split("=");
+     if (couple[0] == "UNICODEvsSYMBOL") UNICODEvsSYMBOL = couple[1];
+  }
+  if (UNICODEvsSYMBOL == "-1") UNICODEvsSYMBOL = getDefaultParam("UNICODEvsSYMBOL");
+  return UNICODEvsSYMBOL;
+}
+
+function getInitialUNICODEvsSYMBOLsymbol()
+{
+  if (getInitialUNICODEvsSYMBOL() == "symbol")
+   return "CHECKED";
+  else
+   return "";
+}
+
+function getInitialUNICODEvsSYMBOLunicode()
+{
+  if (getInitialUNICODEvsSYMBOL() == "unicode")
+   return "CHECKED";
+  else
+   return "";
+}
+
 function getUwoboURL()
 {
   return document.uwoboURL.elements[0].value;
@@ -37,6 +67,14 @@ function getGetterURL()
   return document.getterURL.elements[0].value;
 }
 
+function getUNICODEvsSYMBOL()
+{
+  if (document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].checked)
+   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[0].value;
+  else
+   return document.UNICODEvsSYMBOL.radioUNICODEvsSYMBOL[1].value;
+}
+
 function refreshLinks()
 {
   var search = top.location.search;
@@ -65,7 +103,8 @@ function refreshLinks()
      + "&theoryuri=" + theoryuri
      + "&mode=" + mode
      + "&processorURL=" + getUwoboURL()
-     + "&getterURL=" + getGetterURL();
+     + "&getterURL=" + getGetterURL()
+     + "&UNICODEvsSYMBOL=" + getUNICODEvsSYMBOL();
 }
 
 function selectUwoboURL(ss)
@@ -76,7 +115,7 @@ function selectUwoboURL(ss)
     document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/";
   }
 
-  refreshLink();
+  refreshLinks();
 }
 
 function selectGetterURL(ss)
@@ -87,5 +126,5 @@ function selectGetterURL(ss)
     document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/";
   }
 
-  refreshLink();
+  refreshLinks();
 }