From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 21 Nov 2001 18:32:00 +0000 (+0000)
Subject: mkMetaTheoryURL(): param.embedKeys() forgot.
X-Git-Tag: mlminidom_0_2_2~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46b441cfa0f4a2c2076450a32452796db7ac8c7c;p=helm.git

mkMetaTheoryURL(): param.embedKeys() forgot.
Code improvement.
---

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index e0e37bb05..7dc83d7f2 100644
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -134,6 +134,16 @@ function getTheoryKeys()
   return escape("T1,T2,L,E");
 }
 
+function getEmbedKeys()
+{
+  return escape("d_c,TC1,HC2,L");
+}
+
+function getCICHTMLKeys()
+{
+  return escape("d_c,C1,HC2,L");
+}
+
 function makeURL(type,uri,cicflags,typesflags)
 {
   var mode = top.mode;
@@ -166,7 +176,7 @@ function makeURL(type,uri,cicflags,typesflags)
           mode_list[5] + "&patch_dtd=" + mode_list[6];
   } else {
     if (format == "html" && type == "cic") {
-      keys = escape("d_c,C1,HC2,L") +
+      keys = getCICHTMLKeys() +
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
        "&param.draw_graphURL=" + escape(draw_graphURL) +
@@ -178,7 +188,7 @@ function makeURL(type,uri,cicflags,typesflags)
        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
        "&param.encoding=iso-8859-1" +
        "&param.media-type=text/html" +
-       "&param.keys=" + escape("d_c,C1,HC2,L") +
+       "&param.keys=" + getCICHTMLKeys() +
        "&param.interfaceURL=" + escape(interfaceURL);
     } else if (format == "html" && type == "theory") {
       keys = getTheoryKeys()+
@@ -187,9 +197,9 @@ function makeURL(type,uri,cicflags,typesflags)
        "&param.draw_graphURL=" + escape(draw_graphURL) +
        "&param.uri_set_queueURL=" + escape(uri_set_queueURL) +
        "&param.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) +
-       "&param.keys=" + escape("d_c,C1,HC2,L") +
+       "&param.keys=" + getCICHTMLKeys() +
        "&param.thkeys=" + getTheoryKeys() +
-       "&param.embedkeys=" + escape("d_c,TC1,HC2,L") +
+       "&param.embedkeys=" + getEmbedKeys() +
        "&param.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+
        "&param.encoding=iso-8859-1" +
        "&param.thencoding=iso-8859-1" +
diff --git a/helm/on-line/javascript/graphLinks.js b/helm/on-line/javascript/graphLinks.js
index b7f351e9f..a01a6f6d6 100644
--- a/helm/on-line/javascript/graphLinks.js
+++ b/helm/on-line/javascript/graphLinks.js
@@ -72,6 +72,7 @@ function mkMetaTheoryURL(uri)
    var rdfuri = mkBackwardRDFURI(uri);
    var getterURL = getParam("param.getterURL");
    var url = setParam(location.href,"keys","meta_theory," + unescape(getTheoryKeys()));
+   url = setParam(url,"param.embedkeys", getEmbedKeys());
    url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + rdfuri);
    return url;
 }