X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fon-line%2Fjavascript%2Fcontrol.js;h=26291e73f087f0938fc42643ca2b4cd3a8dc14ee;hb=f5419c538928932f114f78887e489f6b2e19764a;hp=ca62cff5728d5f06fec4bf726171ea676399dd01;hpb=79538d65a060641788bae111438edb705119a4cd;p=helm.git diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js index ca62cff57..26291e73f 100644 --- a/helm/on-line/javascript/control.js +++ b/helm/on-line/javascript/control.js @@ -146,6 +146,11 @@ function getCICHTMLKeys() return escape("d_c,C1,HC2,L"); } +function getCICProofTreeXHTMLMathMLKeys() +{ + return escape("HAT,G,HAO,L"); +} + function makeURL(type,uri,cicflags,typesflags) { var mode = top.mode; @@ -178,7 +183,28 @@ function makeURL(type,uri,cicflags,typesflags) url = getterURL + "getxml?uri=" + rdfprefix + uri + ext + "&format=" + mode_list[5] + "&patch_dtd=" + mode_list[6]; } else { - if (format == "html" && type == "cic") { + var uri_len = uri.length; + if (format == "html" && type == "cic" && uri.substring(uri.length - 10, uri.length) == "proof_tree") { + keys = getCICProofTreeXHTMLMathMLKeys() + + "¶m.processorURL=" + escape(processorURL) + + "¶m.getterURL=" + escape(getterURL) + + "¶m.proofcheckerURL=" + escape(proofcheckerURL) + + "¶m.draw_graphURL=" + escape(draw_graphURL) + + "¶m.uri_set_queueURL=" + escape(uri_set_queueURL) + + "¶m.UNICODEvsSYMBOL=" + escape(UNICODEvsSYMBOL) + + "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.1 plus MathML 2.0//EN")+ + "&prop.doctype-system="+escape("http://www.w3.org/TR/MathML2/dtd/xhtml-math11-f.dtd")+ + "&prop.encoding=iso-8859-1" + + "&prop.media-type=text/xml" + + "&prop.method=xml" + + "¶m.doctype-public="+escape("-//W3C//DTD XHTML 1.1 plus MathML 2.0//EN")+ + "¶m.doctype-system="+escape("http://www.w3.org/TR/MathML2/dtd/xhtml-math11-f.dtd")+ + "¶m.encoding=iso-8859-1" + + "¶m.media-type=text/xml" + + "¶m.method=xml" + + "¶m.keys=" + getCICProofTreeXHTMLMathMLKeys() + + "¶m.interfaceURL=" + escape(interfaceURL); + } else if (format == "html" && type == "cic") { keys = getCICHTMLKeys() + "¶m.processorURL=" + escape(processorURL) + "¶m.getterURL=" + escape(getterURL) +