]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/html/library/control.html
Changes in raw mode interface
[helm.git] / helm / on-line / html / library / control.html
index 7b8806e2b290241c0a25b7f078ed59bffcadd7c2..57c6c3900e83920432cdbc3f97e61146697fdc41 100644 (file)
@@ -30,8 +30,9 @@
        var mode = getParam('mode');
        var mode_list = mode.split(',');
        if (mode_list[0] == "raw") {
-         outputOption(document, "cic", "CIC", mode_list[1]);
-         outputOption(document, "zcic", "CIC GZipped", mode_list[1]);
+         outputOption(document, "cic",   "CIC", mode_list[1]);
+         outputOption(document, "types", "TYPES", mode_list[1]);
+         outputOption(document, "ann",   "ANN", mode_list[1]);
        } else {
          outputOption(document, "html", "HTML", mode_list[2]);
          outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
       <script>
        var mode = getParam('mode');
        var mode_list = mode.split(',');
-        outputCheckbox(document, "updateNatural(this)", "&nbsp;Natural Language", mode_list[3] == "yes");
-        outputCheckbox(document, "updateAnnotations(this)", "&nbsp;Annotations", mode_list[4] == "yes");
+       if (mode_list[0] == "raw") {
+         outputCheckbox(document, "updateCompressed(this)",
+          "&nbsp;Compressed", mode_list[5] == "yes");
+         outputCheckbox(document, "updateDTDPatched(this)",
+          "&nbsp;Resolve DTD URL", mode_list[6] == "yes");
+        } else {
+         outputCheckbox(document, "updateNatural(this)",
+          "&nbsp;Natural Language", mode_list[3] == "yes");
+         outputCheckbox(document, "updateAnnotations(this)",
+          "&nbsp;Annotations", mode_list[4] == "yes");
+        }
       </script>
     </td>
     <td>