From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jun 2001 13:31:46 +0000 (+0000)
Subject: UNICODEvsSYMBOL parameter now added everywhere
X-Git-Tag: v0_1_3~145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d1132a3652b678eeece55c9163f21091ec42ae84;p=helm.git

UNICODEvsSYMBOL parameter now added everywhere
---

diff --git a/helm/on-line/html/control.html b/helm/on-line/html/control.html
index 6e8662db8..791a8b28a 100644
--- 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 57c6c3900..f70dd94cc 100644
--- 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 fb9afb3e4..2c16dff39 100644
--- 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 8d16150cb..a36165f78 100644
--- 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 54d51002f..271f6eabc 100644
--- 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 90e877a01..12862e545 100644
--- 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();
 }