helm/on-line/javascript/control.js

   1 function updateMode(i, s)
   2 {
   3   var mode = top.mode;
   4   var mode_list = mode.split(",");
   5   var res = "";
   6   var j;
   7
   8   for (j = 0; j < mode_list.length; j++) {
   9     if (j == i) res += s;
  10     else res += mode_list[j];
  11     if (j < mode_list.length - 1) res += ",";
  12   }
  13
  14   top.mode = res;
  15 }
  16
  17 function updateOutput(output,format)
  18 {
  19   var theoryuri = top.theoryuri;
  20   var cicuri = top.cicuri;
  21   var mode = top.mode;
  22   var topurl = top.topurl;
  23   var processorURL = top.processorURL;
  24   var getterURL = top.getterURL;
  25   var proofcheckerURL = top.proofcheckerURL;
  26   var draw_graphURL = top.draw_graphURL;
  27   var uri_set_queueURL = top.uri_set_queueURL;
  28   var mode_list = mode.split(",");
  29   var new_mode = output.options[output.selectedIndex].value;
  30   var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&proofcheckerURL=" + proofcheckerURL + "&draw_graphURL=" + draw_graphURL + "&uri_set_queueURL=" + uri_set_queueURL + "&mode=";
  31
  32   if (new_mode != mode_list[0]) {
  33     updateMode(0, new_mode);
  34     if (new_mode == "raw") updateMode(2, format.options[format.selectedIndex].value);
  35     else updateMode(1, format.options[format.selectedIndex].value);
  36
  37     var href =
  38      top.processorURL + 'apply' +
  39      '?keys=RT' +
  40      '&param.topurl=' + topurl +
  41      '&xmluri=' +
  42      escape(top.topurl + '/html/library/control.html' + dest + top.mode);
  43
  44     location.href = href;
  45   }
  46 }
  47
  48 function updateFormat(format)
  49 {
  50   var mode = top.mode;
  51   var mode_list = mode.split(",");
  52
  53   if (mode_list[0] == "raw") {
  54     updateMode(1, format.options[format.selectedIndex].value);
  55   } else {
  56     updateMode(2, format.options[format.selectedIndex].value);
  57   }
  58
  59   refreshReload();
  60 }
  61
  62 function updateNatural(checkbox)
  63 {
  64   if (checkbox.checked) updateMode(3, "yes");
  65   else updateMode(3, "no");
  66   refreshReload();
  67 }
  68
  69 function updateAnnotations(checkbox)
  70 {
  71   if (checkbox.checked) updateMode(4, "yes");
  72   else updateMode(4, "no");
  73   refreshReload();
  74 }
  75
  76 function updateCompressed(checkbox)
  77 {
  78   if (checkbox.checked) updateMode(5, "gz");
  79   else updateMode(5, "normal");
  80   refreshReload();
  81 }
  82
  83 function updateDTDPatched(checkbox)
  84 {
  85   if (checkbox.checked) updateMode(6, "yes");
  86   else updateMode(6, "no");
  87   refreshReload();
  88 }
  89
  90 function refreshReload()
  91 {
  92    var search =
  93       "?mode=" + top.mode +
  94       "&cicuri=" + top.cicuri +
  95       "&theoryuri=" + top.theoryuri +
  96       "&processorURL=" + top.processorURL +
  97       "&getterURL=" + top.getterURL +
  98       "&proofcheckerURL=" + top.proofcheckerURL +
  99       "&draw_graphURL=" + top.draw_graphURL +
 100       "&uri_set_queueURL=" + top.uri_set_queueURL +
 101       "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL;
 102
 103    var href =
 104     top.processorURL + 'apply' +
 105     '?keys=RT' +
 106     '&param.topurl=' + top.topurl +
 107     '&xmluri=' +
 108     escape(top.topurl + '/html/library/index.html' + search);
 109
 110    top.frames[0].document.links[0].href = href;
 111    top.frames[0].document.links[1].href =
 112     top.topurl + '/html/index.html' + search;
 113
 114    return true;
 115 }
 116
 117 function refreshcicHeader(headerURL)
 118 {
 119    top.cicheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.cicuri;
 120    return true;
 121 }
 122
 123 function refreshtheoryHeader(headerURL)
 124 {
 125    top.theoryheader.location.search = "?keys=GP&xmluri=" + headerURL + "&param.uri=" + top.theoryuri;
 126    return true;
 127 }
 128
 129 function getCICMathMLKeys()
 130 {
 131   return escape("d_c,C1,G,C2,L");
 132 }
 133
 134 function getTheoryKeys()
 135 {
 136   return escape("T1,T2,L,E");
 137 }
 138
 139 function getEmbedKeys()
 140 {
 141   return escape("d_c,TC1,HC2,L");
 142 }
 143
 144 function getCICHTMLKeys()
 145 {
 146   return escape("d_c,C1,HC2,L");
 147 }
 148
 149 function getCICProofTreeXHTMLMathMLKeys()
 150 {
 151   return escape("HAT,G,HAO,L");
 152 }
 153
 154 function makeURL(type,uri,cicflags,typesflags)
 155 {
 156   var mode = top.mode;
 157   var processorURL = top.processorURL;
 158   var getterURL = top.getterURL;
 159   var proofcheckerURL = top.proofcheckerURL;
 160   var draw_graphURL = top.draw_graphURL;
 161   var uri_set_queueURL = top.uri_set_queueURL;
 162   var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL;
 163   var mode_list = mode.split(",");
 164
 165   var keys = "";
 166   var url = "";
 167
 168   var interfaceURL = top.topurl + "/html/cic/index.html";
 169   var thinterfaceURL = top.topurl + "/html/theory/index.html";
 170
 171   var output = mode_list[0];
 172   var format;
 173   if (output == "raw") format = mode_list[1];
 174   else format = mode_list[2];
 175
 176   if (output == "raw") {
 177     var ext = "";
 178     var rdfprefix = "";
 179     if (format == "types") ext = ".types"
 180     else if (format == "ann") ext = ".ann"
 181     else if (format == "fwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/forward//"
 182     else if (format == "bwd") rdfprefix = "helm:rdf:www.cs.unibo.it/helm/rdf/backward//";
 183     url = getterURL + "getxml?uri=" + rdfprefix + uri + ext + "&format=" +
 184           mode_list[5] + "&patch_dtd=" + mode_list[6];
 185   } else {
 186     var uri_len = uri.length;
 187     if (format == "html" && type == "cic" && uri.substring(uri.length - 10, uri.length) == "proof_tree") {
 188       keys = getCICProofTreeXHTMLMathMLKeys() +
 189        "&param.processorURL=" + escape(processorURL) +
 190        "&param.getterURL=" + escape(getterURL) +
 191        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 192        "&param.draw_graphURL=" + escape(draw_graphURL) +
 193        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 194        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
 195        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.1 plus MathML 2.0//EN")+
 196        "&prop.doctype-system="+escape("http://www.w3.org/TR/MathML2/dtd/xhtml-math11-f.dtd")+
 197        "&prop.encoding=iso-8859-1" +
 198        "&prop.media-type=text/xml" +
 199        "&prop.method=xml" +
 200        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
 201        "&param.encoding=iso-8859-1" +
 202        "&param.media-type=text/html" +
 203        "&param.keys=" + getCICHTMLKeys() +
 204        "&param.interfaceURL=" + escape(interfaceURL) +
 205        "&param.framewidth=150";
 206     } else if (format == "html" && type == "cic") {
 207       keys = getCICHTMLKeys() +
 208        "&param.processorURL=" + escape(processorURL) +
 209        "&param.getterURL=" + escape(getterURL) +
 210        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 211        "&param.draw_graphURL=" + escape(draw_graphURL) +
 212        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 213        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
 214        "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
 215        "&prop.encoding=iso-8859-1" +
 216        "&prop.media-type=text/html" +
 217        "&prop.method=html" +
 218        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
 219        "&param.encoding=iso-8859-1" +
 220        "&param.media-type=text/html" +
 221        "&param.keys=" + getCICHTMLKeys() +
 222        "&param.interfaceURL=" + escape(interfaceURL);
 223     } else if (format == "html" && type == "theory") {
 224       keys = getTheoryKeys()+
 225        "&param.processorURL=" + escape(processorURL) +
 226        "&param.getterURL=" + escape(getterURL) +
 227        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 228        "&param.draw_graphURL=" + escape(draw_graphURL) +
 229        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 230        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
 231        "&param.keys=" + getCICHTMLKeys() +
 232        "&param.thkeys=" + getTheoryKeys() +
 233        "&param.embedkeys=" + getEmbedKeys() +
 234        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
 235        "&param.encoding=iso-8859-1" +
 236        "&param.thencoding=iso-8859-1" +
 237        "&param.media-type=text/html" +
 238        "&param.thmedia-type=text/html" +
 239        "&param.interfaceURL=" + escape(interfaceURL) +
 240        "&param.thinterfaceURL=" + escape(thinterfaceURL);
 241     } else if (format == "mml_cont" && type == "cic") {
 242       keys = escape("d_c,C1")+
 243        "&param.processorURL=" + escape(processorURL) +
 244        "&param.getterURL=" + escape(getterURL) +
 245        "&prop.doctype-public="+
 246        //"&prop.encoding=" +
 247        "&prop.media-type=text/xml" +
 248        "&param.doctype-public=" +
 249        "&param.encoding=" +
 250        "&param.media-type=text/xml";
 251     } else if (format == "mml_cont" && type == "theory") {
 252       keys = escape("T1,L,E")+
 253        "&param.processorURL=" + escape(processorURL) +
 254        "&param.getterURL=" + escape(getterURL) +
 255        "&param.keys=" + escape("d_c,C1") +
 256        "&param.thkeys=T1,L,E" +
 257        "&param.embedkeys=" + escape("d_c,TC1") +
 258
 259        "&param.processorURL=" + escape(processorURL) +
 260        "&param.getterURL=" + escape(getterURL) +
 261        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 262        "&param.draw_graphURL=" + escape(draw_graphURL) +
 263        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 264        "&param.doctype-public=" +
 265        "&param.encoding=" +
 266        "&param.thencoding=iso-8859-1" +
 267        "&param.media-type=text/xml" +
 268        "&param.thmedia-type=text/html" +
 269        "&param.interfaceURL=" + escape(interfaceURL) +
 270        "&param.thinterfaceURL=" + escape(thinterfaceURL);
 271     } else if (format == "mml_pres" && type == "cic") {
 272       keys = getCICMathMLKeys()+
 273        "&param.processorURL=" + escape(processorURL) +
 274        "&param.getterURL=" + escape(getterURL) +
 275        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 276        "&param.draw_graphURL=" + escape(draw_graphURL) +
 277        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 278        "&prop.doctype-public="+
 279        //"&prop.encoding=" +
 280        "&prop.media-type=text/xml" +
 281        "&param.doctype-public=" +
 282        "&param.encoding=" +
 283        "&param.media-type=text/xml" +
 284        "&param.keys=" + getCICMathMLKeys() +
 285        "&param.interfaceURL=" + escape(interfaceURL);
 286     } else if (format == "mml_pres" && type == "theory") {
 287       keys = getTheoryKeys()+
 288        "&param.keys=" + getCICMathMLKeys() +
 289        "&param.thkeys=" + getTheoryKeys() +
 290        "&param.embedkeys=" + escape("d_c,TC1,G,C2,L") +
 291        "&param.processorURL=" + escape(processorURL) +
 292        "&param.getterURL=" + escape(getterURL) +
 293        "&param.proofcheckerURL=" + escape(proofcheckerURL) +
 294        "&param.draw_graphURL=" + escape(draw_graphURL) +
 295        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
 296        "&param.doctype-public=" +
 297        "&param.encoding=" +
 298        "&param.thencoding=iso-8859-1" +
 299        "&param.media-type=text/xml" +
 300        "&param.thmedia-type=text/html" +
 301        "&param.interfaceURL=" + escape(interfaceURL) +
 302        "&param.thinterfaceURL=" + escape(thinterfaceURL);
 303     }
 304
 305     var naturalLanguage = typesflags.toLowerCase();
 306     if (typesflags != "NO" || type == "theory") {
 307        naturalLanguage = mode_list[3];
 308     }
 309     var annotations = cicflags.toLowerCase();
 310     if (cicflags != "NO" || type == "theory") {
 311        annotations = mode_list[4];
 312     }
 313     url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations + "&param.topurl=" + top.topurl;
 314   }
 315
 316   if (output == "raw")
 317    return url;
 318   else if (type == "cic")
 319    return interfaceURL + "?url=" + escape(url);
 320   else if (type == "theory")
 321    return thinterfaceURL + "?url=" + escape(url)
 322 }
 323