From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Oct 2001 12:12:10 +0000 (+0000)
Subject: Problem of URLs too long for I.E. avoided by removing an unuseful parameter
X-Git-Tag: v0_1_3~30
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=07012ae694021be859c780b2aa0bb85c47dd8c6c;p=helm.git

Problem of URLs too long for I.E. avoided by removing an unuseful parameter
from the inner URL to create a graph. It seems to work for now...
---

diff --git a/helm/on-line/javascript/graphLinks.js b/helm/on-line/javascript/graphLinks.js
index 423d3101f..26ebb2a10 100644
--- a/helm/on-line/javascript/graphLinks.js
+++ b/helm/on-line/javascript/graphLinks.js
@@ -36,6 +36,11 @@ function mkGraphURL(uri,keys,use_rdf_uri)
    url = setParam(url,"param.CICURI",escape(uri));
    var uri_set_size = document.uri_set_size.elements[0].value;
    url = setParam(url,"param.uri_set_size",uri_set_size);
+
+   // The generated URL is sometimes too long for I.E.
+   // So it is now better to remove some unuseful pararams from the inner URL
+   url = dropParam(url,"param.processorURL");
+
    url = draw_graphURL + 'draw?url=' + escape(url);
    var url2 = setParam(location.href,"keys","MGL,RT");
    url2 = setParam(url2,"xmluri",escape(url));
diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js
index 42599f7e8..bb018ad0e 100644
--- a/helm/on-line/javascript/utils.js
+++ b/helm/on-line/javascript/utils.js
@@ -3,6 +3,25 @@ function chopSlash(url)
   return url.slice(0,url.lastIndexOf('/'));
 }
 
+function dropParam(url,name)
+{
+  var urla = url.split("?");
+  var search = urla[1];
+  var args = search.split("&");
+  var newargs = new Array();
+  var j = 0;
+
+  for (var i = 0 ; i < args.length ; i++) {
+     var couple = args[i].split("=");
+     if (couple[0] != name) {
+        newargs[j] = args[i];
+        j++;
+     }
+  }
+
+  return (urla[0] + "?" + newargs.join("&"));
+}
+
 function setParam(url,name,value)
 {
   var urla = url.split("?");