X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fcontrol.js;h=e43587573745af5662d917d655cd71d6821a9bd0;hb=98bebe823e0b925f5b4bd3b0c70f1a966ae12758;hp=8debc89f8d486e1ed17c5d40bd6792cb3914def3;hpb=fb158d51c621e55962a6139d03cd1678cfb2e8f1;p=helm.git

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 8debc89f8..e43587573 100644
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -1,4 +1,3 @@
-
 function updateMode(i, s)
 {
   var mode = top.mode;
@@ -63,6 +62,20 @@ function updateAnnotations(checkbox)
   refreshReload();
 }
 
+function updateCompressed(checkbox)
+{
+  if (checkbox.checked) updateMode(5, "gz");
+  else updateMode(5, "normal");
+  refreshReload();
+}
+
+function updateDTDPatched(checkbox)
+{
+  if (checkbox.checked) updateMode(6, "yes");
+  else updateMode(6, "no");
+  refreshReload();
+}
+
 function refreshReload()
 {
    var search = 
@@ -106,8 +119,11 @@ function makeURL(type,uri,cicflags,typesflags)
   else format = mode_list[2];
   
   if (output == "raw") {
-    url = getterURL + "getxml?uri=" + uri +
-     "&format=" + (format == "zcic" ? "gz" : "normal");
+    var ext = "";
+    if (format == "types") ext = ".types"
+    else if (format == "ann") ext = ".ann";
+    url = getterURL + "getxml?uri=" + uri + ext + "&format=" + mode_list[5] +
+     "&patch_dtd=" + mode_list[6];
   } else {
     if (format == "html" && type == "cic") {
       keys = "C1,HC2,L&param.processorURL=" + escape(processorURL) +
@@ -143,6 +159,8 @@ function makeURL(type,uri,cicflags,typesflags)
        "&param.keys=" + escape("C1,C2,L");
     } else if (format == "mml_pres" && type == "theory") {
       keys = "T1,T2,L,E&param.keys=C1,C2&param.thkeys=TC1,C2,L" +
+       "&param.processorURL=" + escape(processorURL) +
+       "&param.getterURL=" + escape(getterURL) +
        "&param.doctype-public=" +
        "&param.encoding=" +
        "&param.media-type=text/xml";