From: Luca Padovani Date: Tue, 25 May 2004 17:56:07 +0000 (+0000) Subject: ############################################################### X-Git-Tag: premoogle~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;p=helm.git ############################################################### ### Partial major upgrade of the HELM/MoWGLI Web interface. ### ############################################################### WARNING: requires the new UWOBO profiles. Known bugs: 1. the JSMmenu for graphs is broken 2. the configuration stuff is utterly broken: you should rely on the default configuration 3. only HTML has been tested (MathML and ProofTrees are broken for sure) 4. dead code everywhere (e.g. almost all the existent javascript code; several tokens in links_library.xsl) --- diff --git a/helm/graphs/tools/mk_html.pl b/helm/graphs/tools/mk_html.pl index 6ca4d0bcf..a928cd5ad 100755 --- a/helm/graphs/tools/mk_html.pl +++ b/helm/graphs/tools/mk_html.pl @@ -4,16 +4,14 @@ use URI::Escape; print < - + Graph diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html index 169741997..be00b755c 100644 --- a/helm/on-line/html/cic/control.html +++ b/helm/on-line/html/cic/control.html @@ -1,7 +1,8 @@ - + + -??? - - - - + -

Object: - "" - [Annotations are - - ] -

- - - - - - - - - - - - - -

+

+ +

-

- (Before following the link, you must install the HELM Annotation Helper) -

+ var url = ""; + document.write('Object'); + + +

-

DC Metadata and dependency metadata; Dependency graphs -

+ +

-

Proof-checking is recursively performed over the untrusted parts of the - library -

+ + diff --git a/helm/on-line/html/cic/index.html b/helm/on-line/html/cic/index.html index c2a2ef504..1d9bd88c7 100644 --- a/helm/on-line/html/cic/index.html +++ b/helm/on-line/html/cic/index.html @@ -1,16 +1,24 @@ - + - - - ???</script> + <subst:CICURI/> - diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html index 72c13b65f..50016dcea 100644 --- a/helm/on-line/html/library/control.html +++ b/helm/on-line/html/library/control.html @@ -50,23 +50,18 @@
(do it also before attempting to take a link to the current page)
diff --git a/helm/on-line/html/library/index.html b/helm/on-line/html/library/index.html index 4f1be5faa..a667aba28 100644 --- a/helm/on-line/html/library/index.html +++ b/helm/on-line/html/library/index.html @@ -12,7 +12,10 @@ Index @@ -18,25 +21,24 @@ td.back { background-color: #e6e6fa; color: brown } -

Theory: - "" - [Annotations have no meaning for theories, yet] -

- +

+

+ +

+ diff --git a/helm/on-line/html/theory/index.html b/helm/on-line/html/theory/index.html index c2a2ef504..64dbeb3c9 100644 --- a/helm/on-line/html/theory/index.html +++ b/helm/on-line/html/theory/index.html @@ -1,16 +1,24 @@ - + - - - ???</script> + <subst:CICURI/> - diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js index 79ed47fd7..bc52d02b6 100644 --- a/helm/on-line/javascript/control.js +++ b/helm/on-line/javascript/control.js @@ -14,20 +14,14 @@ function updateMode(i, s) top.mode = res; } -function updateOutput(output,format) +function updateOutput(output,format,processorURL,interfaceURL) { var theoryuri = top.theoryuri; var cicuri = top.cicuri; var mode = top.mode; - var topurl = top.topurl; - var processorURL = top.processorURL; - var getterURL = top.getterURL; - var proofcheckerURL = top.proofcheckerURL; - var draw_graphURL = top.draw_graphURL; - var uri_set_queueURL = top.uri_set_queueURL; var mode_list = mode.split(","); var new_mode = output.options[output.selectedIndex].value; - 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="; + var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&mode="; if (new_mode != mode_list[0]) { updateMode(0, new_mode); @@ -35,17 +29,17 @@ function updateOutput(output,format) else updateMode(1, format.options[format.selectedIndex].value); var href = - top.processorURL + 'apply' + + processorURL + 'apply' + '?keys=RT' + '¶m.topurl=' + topurl + '&xmluri=' + - escape(top.topurl + '/html/library/control.html' + dest + top.mode); + escape(interfaceURL + '/html/library/control.html' + dest + top.mode); location.href = href; } } -function updateFormat(format) +function updateFormat(format,profile,processorURL,interfaceURL) { var mode = top.mode; var mode_list = mode.split(","); @@ -56,60 +50,55 @@ function updateFormat(format) updateMode(2, format.options[format.selectedIndex].value); } - refreshReload(); + refreshReload(profile,processorURL,interfaceURL); } -function updateNatural(checkbox) +function updateNatural(checkbox,profile,processorURL,interfaceURL) { if (checkbox.checked) updateMode(3, "yes"); else updateMode(3, "no"); - refreshReload(); + refreshReload(profile,processorURL,interfaceURL); } -function updateAnnotations(checkbox) +function updateAnnotations(checkbox,profile,processorURL,interfaceURL) { if (checkbox.checked) updateMode(4, "yes"); else updateMode(4, "no"); - refreshReload(); + refreshReload(profile,processorURL,interfaceURL); } -function updateCompressed(checkbox) +function updateCompressed(checkbox,profile,processorURL,interfaceURL) { if (checkbox.checked) updateMode(5, "gz"); else updateMode(5, "normal"); - refreshReload(); + refreshReload(profile,processorURL,interfaceURL); } -function updateDTDPatched(checkbox) +function updateDTDPatched(checkbox,profile,processorURL,interfaceURL) { if (checkbox.checked) updateMode(6, "yes"); else updateMode(6, "no"); - refreshReload(); + refreshReload(profile,processorURL,interfaceURL); } -function refreshReload() +function refreshReload(profile, processorURL, interfaceURL) { var search = "?mode=" + top.mode + "&cicuri=" + top.cicuri + - "&theoryuri=" + top.theoryuri + - "&processorURL=" + top.processorURL + - "&getterURL=" + top.getterURL + - "&proofcheckerURL=" + top.proofcheckerURL + - "&draw_graphURL=" + top.draw_graphURL + - "&uri_set_queueURL=" + top.uri_set_queueURL + - "&UNICODEvsSYMBOL=" + top.UNICODEvsSYMBOL; + "&theoryuri=" + top.theoryuri; - var href = - top.processorURL + 'apply' + + var href = processorURL + + 'apply' + '?keys=RT' + - '¶m.topurl=' + top.topurl + + '&profile=' + profile + + '¶m.profile=' + profile + '&xmluri=' + - escape(top.topurl + '/html/library/index.html' + search); + escape(interfaceURL + '/html/library/index.html' + search); top.frames[0].document.links[0].href = href; top.frames[0].document.links[1].href = - top.topurl + '/html/index.html' + search; + interfaceURL + '/html/index.html' + search; return true; } @@ -151,22 +140,16 @@ function getCICProofTreeXHTMLMathMLKeys() return escape("HAT,G,HAO,L"); } -function makeURL(type,uri,cicflags,typesflags) +function makeURL(type,uri,cicflags,typesflags,profile,processorURL,interfaceURL,getterURL) { var mode = top.mode; - var processorURL = top.processorURL; - var getterURL = top.getterURL; - var proofcheckerURL = top.proofcheckerURL; - var draw_graphURL = top.draw_graphURL; - var uri_set_queueURL = top.uri_set_queueURL; - var UNICODEvsSYMBOL = top.UNICODEvsSYMBOL; var mode_list = mode.split(","); var keys = ""; var url = ""; - var interfaceURL = top.topurl + "/html/cic/index.html"; - var thinterfaceURL = top.topurl + "/html/theory/index.html"; + var interfaceURLidx = interfaceURL + "/html/cic/index.html"; + var thinterfaceURLidx = interfaceURL + "/html/theory/index.html"; var output = mode_list[0]; var format; @@ -186,12 +169,8 @@ function makeURL(type,uri,cicflags,typesflags) 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) + + "&profile=" + profile + + "&default.profile=" + profile + "&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" + @@ -201,16 +180,11 @@ function makeURL(type,uri,cicflags,typesflags) "¶m.encoding=iso-8859-1" + "¶m.media-type=text/html" + "¶m.keys=" + getCICHTMLKeys() + - "¶m.interfaceURL=" + escape(interfaceURL) + "¶m.framewidth=150"; } else if (format == "html" && type == "cic") { keys = getCICHTMLKeys() + - "¶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) + + "&profile=" + profile + + "¶m.profile=" + profile + "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+ "&prop.encoding=iso-8859-1" + "&prop.media-type=text/html" + @@ -218,16 +192,11 @@ function makeURL(type,uri,cicflags,typesflags) "¶m.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+ "¶m.encoding=iso-8859-1" + "¶m.media-type=text/html" + - "¶m.keys=" + getCICHTMLKeys() + - "¶m.interfaceURL=" + escape(interfaceURL); + "¶m.keys=" + getCICHTMLKeys(); } else if (format == "html" && type == "theory") { keys = getTheoryKeys()+ - "¶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) + + "&profile=" + profile + + "¶m.profile=" + profile + "¶m.keys=" + getCICHTMLKeys() + "¶m.thkeys=" + getTheoryKeys() + "¶m.embedkeys=" + getEmbedKeys() + @@ -235,89 +204,57 @@ function makeURL(type,uri,cicflags,typesflags) "¶m.encoding=iso-8859-1" + "¶m.thencoding=iso-8859-1" + "¶m.media-type=text/html" + - "¶m.thmedia-type=text/html" + - "¶m.interfaceURL=" + escape(interfaceURL) + - "¶m.thinterfaceURL=" + escape(thinterfaceURL); + "¶m.thmedia-type=text/html"; } else if (format == "mml_cont" && type == "cic") { keys = escape("d_c,C1")+ - "¶m.processorURL=" + escape(processorURL) + - "¶m.getterURL=" + escape(getterURL) + + "&profile=" + profile + + "¶m.profile=" + profile + "&prop.doctype-public="+ - //"&prop.encoding=" + "&prop.media-type=text/xml" + "¶m.doctype-public=" + "¶m.encoding=" + "¶m.media-type=text/xml"; } else if (format == "mml_cont" && type == "theory") { keys = escape("T1,L,E")+ - "¶m.processorURL=" + escape(processorURL) + - "¶m.getterURL=" + escape(getterURL) + + "&profile=" + profile + + "¶m.profile=" + profile + "¶m.keys=" + escape("d_c,C1") + "¶m.thkeys=T1,L,E" + "¶m.embedkeys=" + escape("d_c,TC1") + - - "¶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.doctype-public=" + "¶m.encoding=" + "¶m.thencoding=iso-8859-1" + "¶m.media-type=text/xml" + - "¶m.thmedia-type=text/html" + - "¶m.interfaceURL=" + escape(interfaceURL) + - "¶m.thinterfaceURL=" + escape(thinterfaceURL); + "¶m.thmedia-type=text/html"; } else if (format == "mml_pres" && type == "cic") { keys = getCICMathMLKeys()+ - "¶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) + + "&profile=" + profile + + "¶m.profile=" + profile + "&prop.doctype-public="+ - //"&prop.encoding=" + "&prop.media-type=text/xml" + "¶m.doctype-public=" + "¶m.encoding=" + "¶m.media-type=text/xml" + - "¶m.keys=" + getCICMathMLKeys() + - "¶m.interfaceURL=" + escape(interfaceURL); + "¶m.keys=" + getCICMathMLKeys(); } else if (format == "mml_pres" && type == "theory") { keys = getTheoryKeys()+ + "&profile=" + profile + + "¶m.profile=" + profile + "¶m.keys=" + getCICMathMLKeys() + "¶m.thkeys=" + getTheoryKeys() + "¶m.embedkeys=" + escape("d_c,TC1,G,C2,L") + - "¶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.doctype-public=" + "¶m.encoding=" + "¶m.thencoding=iso-8859-1" + "¶m.media-type=text/xml" + - "¶m.thmedia-type=text/html" + - "¶m.interfaceURL=" + escape(interfaceURL) + - "¶m.thinterfaceURL=" + escape(thinterfaceURL); + "¶m.thmedia-type=text/html"; } - - var naturalLanguage = typesflags.toLowerCase(); - if (typesflags != "NO" || type == "theory") { - naturalLanguage = mode_list[3]; - } - var annotations = cicflags.toLowerCase(); - if (cicflags != "NO" || type == "theory") { - annotations = mode_list[4]; - } - url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "¶m.CICURI=" + uri + "¶m.naturalLanguage=" + naturalLanguage + "¶m.annotations=" + annotations + "¶m.topurl=" + top.topurl; } if (output == "raw") return url; else if (type == "cic") - return interfaceURL + "?url=" + escape(url); + return processorURL + "apply?keys=RT&xmluri=" + escape(interfaceURLidx) + "¶m.ignore=" + keys + "¶m.CICURI=" + uri; else if (type == "theory") - return thinterfaceURL + "?url=" + escape(url) + return processorURL + "apply?keys=RT&xmluri=" + escape(thinterfaceURLidx) + "¶m.ignore=" + keys + "¶m.CICURI=" + uri; } - diff --git a/helm/on-line/xslt/ls2html.xsl b/helm/on-line/xslt/ls2html.xsl index 9302e5841..80d6946e5 100644 --- a/helm/on-line/xslt/ls2html.xsl +++ b/helm/on-line/xslt/ls2html.xsl @@ -10,9 +10,11 @@ + + @@ -55,12 +57,12 @@ "top.{$target}uri='{$quoteduri}'; refresh{$target}Header('{$interfaceURL}/html/library/header.html'); var search='?keys={$keys}' + + '&profile={$profile}' + + '&param.profile={$profile}' + '&xmluri=' + escape('{$getterURL}ls?format=xml'+'&baseuri={$quoteduri}')+ '&param.uri={$quoteduri}' + '&param.keys={$keys}' + - '&param.getterURL={$getterURL}' + - '&param.target={$target}' + - '&param.interfaceURL={$interfaceURL}'; + '&param.target={$target}'; var pathname = this.pathname; if (pathname.charAt(0) != '/') pathname = '/' + pathname; @@ -148,7 +150,7 @@ - @@ -158,13 +160,13 @@ - Proof term - Proof tree diff --git a/helm/on-line/xslt/ls2theory.xsl b/helm/on-line/xslt/ls2theory.xsl new file mode 100644 index 000000000..ed9c217e0 --- /dev/null +++ b/helm/on-line/xslt/ls2theory.xsl @@ -0,0 +1,45 @@ + + + + + + + + + + + + + + +

+ +

+ + + + + +

+ + + + / +

+ + + +

+ + + +

+ + + diff --git a/helm/on-line/xslt/makeGraphLinks.xsl b/helm/on-line/xslt/makeGraphLinks.xsl index 4be261bcb..4f946cbe6 100644 --- a/helm/on-line/xslt/makeGraphLinks.xsl +++ b/helm/on-line/xslt/makeGraphLinks.xsl @@ -25,10 +25,13 @@ + @@ -43,32 +46,32 @@ - +

- - - -

- - - - Number of nodes to show when following an hyperlink: - (30 suggested) - +

hideMenu(); + + + Number of nodes to show when following an hyperlink: + (30 suggested) +

@@ -76,10 +79,10 @@

- - - - + + + +

Objects this one depends on.

Render this object.

Objects depending directly on this one.

Objects depending on this one.

Objects this one depends on.

Render this object.

Objects depending directly on this one.

Objects depending on this one.

@@ -88,16 +91,56 @@ - +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

- lastX = getX(event); lastY = getY(event);selectedURI=''; + lastX = getX(event); lastY = getY(event); selectedURI=''; selectedCICURL=''; selectedTheoryURL=''; selectedForwardURL=''; selectedBackwardURL=''; javascript:moveMenu(lastX,lastY); showMenu();

diff --git a/helm/on-line/xslt/metadataLib.xsl b/helm/on-line/xslt/metadataLib.xsl index 17050ea66..bd9b84524 100644 --- a/helm/on-line/xslt/metadataLib.xsl +++ b/helm/on-line/xslt/metadataLib.xsl @@ -32,12 +32,12 @@ Metadata of <xsl:value-of select="$CICURI"/> - + + + + + +

Metadata of

@@ -77,11 +77,15 @@

- + + + + + + + + + View the graph of all the objects depending on this one.

@@ -94,12 +98,15 @@

- - + + + + + + + + + View the graph of all the dependencies of this object.

diff --git a/helm/on-line/xslt/resolve_topurl.xsl b/helm/on-line/xslt/resolve_topurl.xsl index 6cfe0eda0..50fd991fc 100644 --- a/helm/on-line/xslt/resolve_topurl.xsl +++ b/helm/on-line/xslt/resolve_topurl.xsl @@ -3,19 +3,110 @@ + + + - + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + # + .theory + .con + .ind + .var + .con.body + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + diff --git a/helm/on-line/xslt/toplevel_header.xsl b/helm/on-line/xslt/toplevel_header.xsl new file mode 100644 index 000000000..4dc5a88c6 --- /dev/null +++ b/helm/on-line/xslt/toplevel_header.xsl @@ -0,0 +1,49 @@ + + + + + + + + + + + + + + + / + + + + + + + + + + + + + + + + + + + + / + + + + + + + + + diff --git a/helm/on-line/xslt/xslt_index.txt b/helm/on-line/xslt/xslt_index.txt index 2f27d8e6f..7d1abeb38 100644 --- a/helm/on-line/xslt/xslt_index.txt +++ b/helm/on-line/xslt/xslt_index.txt @@ -1,7 +1,9 @@ getParam.xsl ls2html.xsl +ls2theory.xsl makeGraphLinks.xsl metadataControl.xsl metadataLib.xsl resolve_topurl.xsl +toplevel_header.xsl utils.xsl diff --git a/helm/searchEngine/html/index.html b/helm/searchEngine/html/index.html index 0e120ed90..fa91efcff 100644 --- a/helm/searchEngine/html/index.html +++ b/helm/searchEngine/html/index.html @@ -45,12 +45,7 @@ function initialize() // @variable@ will be substituted by the searchEngine with the param.variable // argument value var processorURL="@processorURL@"; -var getterURL="@getterURL@"; var thkeys="@thkeys@"; -var proofcheckerURL="@proofcheckerURL@"; -var draw_graphURL="@draw_graphURL@"; -var uri_set_queueURL="@uri_set_queueURL@"; -var UNICODEvsSYMBOL="@UNICODEvsSYMBOL@"; var keys="@keys@"; var thkeys="@thkeys@"; var embedkeys="@embedkeys@"; @@ -59,25 +54,18 @@ var encoding="@encoding@"; var thencoding="@thencoding@"; var media_type="@media-type@"; var thmedia_type="@thmedia-type@"; -var interfaceURL="@interfaceURL@"; -var thinterfaceURL="@thinterfaceURL@"; var CICURI="@CICURI@"; var naturalLanguage="@naturalLanguage@"; var annotations="@annotations@"; -var interface_topurl="@topurl@"; function ask_uwobo(url) { return (top.topurl+"/ask_uwobo?url="+ encodeURIComponent(processorURL + "apply?" + "xmluri=" + encodeURIComponent(url) + + "&profile=default" + + "¶m.profile=default" + "&keys=" + encodeURIComponent(thkeys) + - "¶m.processorURL=" + encodeURIComponent(processorURL) + - "¶m.getterURL=" + encodeURIComponent(getterURL) + - "¶m.proofcheckerURL=" + encodeURIComponent(proofcheckerURL) + - "¶m.draw_graphURL=" + encodeURIComponent(draw_graphURL) + - "¶m.uri_set_queueURL=" + encodeURIComponent(uri_set_queueURL) + - "¶m.UNICODEvsSYMBOL=" + encodeURIComponent(UNICODEvsSYMBOL) + "¶m.keys=" + encodeURIComponent(keys) + "¶m.thkeys=" + encodeURIComponent(thkeys) + "¶m.embedkeys=" + encodeURIComponent(embedkeys) + @@ -86,12 +74,9 @@ function ask_uwobo(url) "¶m.thencoding=" + encodeURIComponent(thencoding) + "¶m.media-type=" + encodeURIComponent(media_type) + "¶m.thmedia-type=" + encodeURIComponent(thmedia_type) + - "¶m.interfaceURL=" + encodeURIComponent(interfaceURL) + - "¶m.thinterfaceURL=" + encodeURIComponent(thinterfaceURL) + "¶m.CICURI=" + encodeURIComponent(CICURI) + "¶m.naturalLanguage=" + encodeURIComponent(naturalLanguage) + "¶m.annotations=" + encodeURIComponent(annotations) + - "¶m.topurl=" + encodeURIComponent(interface_topurl) + "&prop.method=html" + "¶m.expandasking=" + encodeURIComponent(top.topurl))); }