helm/on-line/html/library/control.html

   1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
   2 "http://www.w3.org/TR/REC-html40/loose.dtd">
   3 <html>
   4 <head>
   5 <title>Control panel</title>
   6 <script language="JavaScript" src="../../javascript/defaults.js"></script>
   7 <script language="JavaScript" src="../../javascript/utils.js"></script>
   8 <script language="JavaScript" src="../../javascript/control.js"></script>
   9 </head>
  10 <body bgcolor="#ffffff" text="#000000">
  11 <form>
  12 <table>
  13   <tr>
  14     <td>
  15       <b>Format</b>:
  16     </td>
  17     <td>
  18       <select name="output" onChange="updateOutput(this,document.forms[0].format)">
  19       <script>
  20         var mode = getParam('mode');
  21         var mode_list = mode.split(',');
  22         outputOption(document, "processed", "Processed", mode_list[0]);
  23         outputOption(document, "raw", "Raw", mode_list[0]);
  24       </script>
  25       </select>
  26     </td>
  27     <td>
  28       <select name="format" onChange="updateFormat(this)">
  29       <script>
  30         var mode = getParam('mode');
  31         var mode_list = mode.split(',');
  32         if (mode_list[0] == "raw") {
  33           outputOption(document, "cic",   "CIC", mode_list[1]);
  34           outputOption(document, "types", "TYPES", mode_list[1]);
  35           outputOption(document, "ann",   "ANN", mode_list[1]);
  36         } else {
  37           outputOption(document, "html", "HTML", mode_list[2]);
  38           outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
  39           outputOption(document, "mml_pres", "MathML Presentation", mode_list[2]);
  40         }
  41       </script>
  42       </select>
  43     </td>
  44     <td>
  45      <script>
  46        document.write('<a target="_top" href="' +
  47          getParam('topurl') +
  48          '?mode=' + getParam('mode') +
  49          '&cicuri=' + getParam('cicuri') +
  50          '&theoryuri=' + getParam('theoryuri') +
  51          '&processorURL=' + getParam('processorURL') +
  52          '&getterURL=' + getParam('getterURL') +
  53          '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
  54          '" onClick="refreshReload()">Reload</a>');
  55      </script>
  56      <br>
  57      (do it also before attempting to take a link to the current page)
  58      <script>
  59        top.processorURL = getParam('processorURL');
  60        top.getterURL = getParam('getterURL');
  61        top.UNICODEvsSYMBOL = getParam('UNICODEvsSYMBOL');
  62        top.topurl = getParam('topurl');
  63        top.mode = getParam('mode');
  64        top.cicuri = getParam('cicuri');
  65        top.theoryuri = getParam('theoryuri');
  66      </script>
  67     </td>
  68   </tr>
  69   <tr>
  70     <td colspan="3">
  71       <script>
  72         var mode = getParam('mode');
  73         var mode_list = mode.split(',');
  74         if (mode_list[0] == "raw") {
  75          outputCheckbox(document, "updateCompressed(this)",
  76           "&nbsp;Compressed", mode_list[5] == "yes");
  77          outputCheckbox(document, "updateDTDPatched(this)",
  78           "&nbsp;Resolve DTD URL", mode_list[6] == "yes");
  79         } else {
  80          outputCheckbox(document, "updateNatural(this)",
  81           "&nbsp;Natural Language", mode_list[3] == "yes");
  82          outputCheckbox(document, "updateAnnotations(this)",
  83           "&nbsp;Annotations", mode_list[4] == "yes");
  84         }
  85       </script>
  86     </td>
  87     <td>
  88      <script>
  89        document.write('<a target="_top" href="../../html/index.html' +
  90          '?mode=' + getParam('mode') +
  91          '&cicuri=' + getParam('cicuri') +
  92          '&theoryuri=' + getParam('theoryuri') +
  93          '&processorURL=' + getParam('processorURL') +
  94          '&getterURL=' + getParam('getterURL') +
  95          '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
  96          '" onClick="refreshReload()">Configuration Panel</a>');
  97      </script>
  98      <br>
  99     </td>
 100   </tr>
 101 </table>
 102 </form>
 103 </body>
 104 </html>