]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/javascript/graphLinks.js
Version 1.2.1beta => 1.2.1
[helm.git] / helm / on-line / javascript / graphLinks.js
index 15708475e9abe66f2d370e135504f758747a17e7..c95c85a45a6151415df35f536756fb1fcb258f94 100644 (file)
@@ -25,7 +25,7 @@ function removeXPointer(uri)
 
 // (use_rdf_uri==true) if the stylesheet must be applied to the
 // metadata; (use_rdf_uri==false) otherwise
-function mkGraphURL(uri,keys,use_rdf_uri,use_default_uri_set_size)
+function mkGraphURL(uri,keys,use_rdf_uri)
 {
    var getterURL = unescape(getParam("param.getterURL"));
    var draw_graphURL = unescape(getParam("param.draw_graphURL"));
@@ -34,27 +34,29 @@ function mkGraphURL(uri,keys,use_rdf_uri,use_default_uri_set_size)
    url = setParam(url,"xmluri", getterURL + 'getxml%3Furi%3D' +
     (use_rdf_uri ? rdfuri : removeXPointer(uri)));
    url = setParam(url,"param.CICURI",escape(uri));
-   var uri_set_size =
-    use_default_uri_set_size ? -1 : document.uri_set_size.elements[0].value;
-   if (uri_set_size > 0)
-    url = setParam(url,"param.uri_set_size",uri_set_size);
+   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));
-   if (uri_set_size > 0)
-    url2 = setParam(url2,"param.uri_set_size",uri_set_size);
+   url2 = setParam(url2,"param.uri_set_size",uri_set_size);
    return url2;
 }
 
-function mkDepURL(uri,use_default_uri_set_size)
+function mkDepURL(uri)
 {
-   return mkGraphURL(uri,"MDG",0,use_default_uri_set_size);
+   return mkGraphURL(uri,"MDG",0);
 }
 
 
-function mkMetaURL(uri,use_default_uri_set_size)
+function mkMetaURL(uri)
 {
-   return mkGraphURL(uri,"MMG",1,use_default_uri_set_size);
+   return mkGraphURL(uri,"MMG",1);
 }
 
 function mkCICURL(uri)
@@ -73,7 +75,7 @@ function mkMetaTheoryURL(uri)
 {
    var rdfuri = mkRDFURI(uri);
    var getterURL = getParam("param.getterURL");
-   var url = setParam(location.href,"keys","meta_theory%2CT1%2CT2%2CL%2CE");
+   var url = setParam(location.href,"keys","meta_theory," + unescape(getTheoryKeys()));
    url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + rdfuri);
    return url;
 }