]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/html/library/control.html
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / on-line / html / library / control.html
diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html
index 7b8806e2b290241c0a25b7f078ed59bffcadd7c2..72c13b65f63bc4ab03de914953b392b58e830eee 100644 (file)
--- a/helm/on-line/html/library/control.html
+++ b/helm/on-line/html/library/control.html
@@ -1,11 +1,16 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
-"http://www.w3.org/TR/REC-html40/loose.dtd">
-<html>
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
+-->
+
+<html xmlns:subst="http://www.cs.unibo.it/helm/subst">
 <head>
 <title>Control panel</title>
-<script language="JavaScript" src="../../javascript/defaults.js"></script>
-<script language="JavaScript" src="../../javascript/utils.js"></script>
-<script language="JavaScript" src="../../javascript/control.js"></script>
+<!-- Note: <subst:script/> are substitued by the stylesheet with <script />  -->
+<!-- after changing @src in the concatenation of the interface URL with @src -->
+<subst:script language="JavaScript" src="/javascript/defaults.js" />
+<subst:script language="JavaScript" src="/javascript/utils.js" />
+<subst:script language="JavaScript" src="/javascript/control.js" />
 </head>
 <body bgcolor="#ffffff" text="#000000">
 <form>
@@ -17,7 +22,7 @@
     <td>
       <select name="output" onChange="updateOutput(this,document.forms[0].format)">
       <script>
-       var mode = getParam('mode');
+       var mode = getParam2('mode');
        var mode_list = mode.split(',');
        outputOption(document, "processed", "Processed", mode_list[0]);
        outputOption(document, "raw", "Raw", mode_list[0]);
@@ -27,11 +32,14 @@
     <td>
       <select name="format" onChange="updateFormat(this)">
       <script>
-       var mode = getParam('mode');
+       var mode = getParam2('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]);
+         outputOption(document, "fwd",   "RDF: Forward pointers", mode_list[1]);
+         outputOption(document, "bwd",   "RDF: Backward pointers", mode_list[1]);
        } else {
          outputOption(document, "html", "HTML", mode_list[2]);
          outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
@@ -42,47 +50,58 @@
     </td>
     <td>
      <script>
+<![CDATA[
        document.write('<a target="_top" href="' +
-         getParam('topurl') +
-        '?mode=' + getParam('mode') +
-        '&cicuri=' + getParam('cicuri') +
-        '&theoryuri=' + getParam('theoryuri') +
-        '&processorURL=' + getParam('processorURL') +
-        '&getterURL=' + getParam('getterURL') +
+         getParam2('topurl') + '/html/library/index.html' +
         '" onClick="refreshReload()">Reload</a>');
+]]>
      </script>
-     <br>
+     <br />
      (do it also before attempting to take a link to the current page)
      <script>
-       top.processorURL = getParam('processorURL');
-       top.getterURL = getParam('getterURL');
-       top.topurl = getParam('topurl');
-       top.mode = getParam('mode');
-       top.cicuri = getParam('cicuri');
-       top.theoryuri = getParam('theoryuri');
+<![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');
+       top.topurl = getParam2('topurl');
+       top.mode = getParam2('mode');
+       top.cicuri = getParam2('cicuri');
+       top.theoryuri = getParam2('theoryuri');
+]]>
      </script>
     </td>
   </tr>
   <tr>
     <td colspan="3">
       <script>
-       var mode = getParam('mode');
+<![CDATA[
+       var mode = getParam2('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] == "gz");
+         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>
      <script>
-       document.write('<a target="_top" href="../../html/index.html' +
-         '?mode=' + getParam('mode') +
-        '&cicuri=' + getParam('cicuri') +
-        '&theoryuri=' + getParam('theoryuri') +
-        '&processorURL=' + getParam('processorURL') +
-        '&getterURL=' + getParam('getterURL') +
-        '" onClick="refreshReload()">Configuration Panel</a>');
+<![CDATA[
+       document.write('<a target="_top" href=""' +
+        ' onClick="refreshReload()">Configuration Panel</a>');
+]]>
      </script>
-     <br>
+     <br />
     </td>
   </tr>
 </table>
Unnamed repository; edit this file 'description' to name the repository.