From: Luca Padovani Date: Tue, 13 Mar 2001 09:12:56 +0000 (+0000) Subject: Initial revision X-Git-Tag: v0_1_2~82 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97829180b4bc5a72291eeb8156b15b3922f07048;p=helm.git Initial revision --- diff --git a/helm/on-line/html/control.html b/helm/on-line/html/control.html new file mode 100644 index 000000000..6e8662db8 --- /dev/null +++ b/helm/on-line/html/control.html @@ -0,0 +1,119 @@ + + + +On-Line Library Configuration + + + + + + + + + + + + +
On-Line Library Configuration
+ +
+ +
+The on-line interface will use a +Getter to locate and +download documents and an +UWOBO to apply transformations +to them. + + +

+ +Here you can choose the Getter and the UWOBO to use, providing valid URLs +to instances of them. + +

+ +To control the behaviour of them, use the apposite +Getter panel +and +UWOBO panel. + +

+ + + + + + + + + + +
UWOBO URL
+
+ +
+ 		+
+ +
+ 		+
+ +
+
+ +
+ + + + + + + + + + +
Getter URL
+
+ +
+ 		+
+ +
+ 		+
+ +
+
+
+ +
+

+
+ + + diff --git a/helm/on-line/html/index.html b/helm/on-line/html/index.html new file mode 100644 index 000000000..caeebcf24 --- /dev/null +++ b/helm/on-line/html/index.html @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html new file mode 100644 index 000000000..8450f3244 --- /dev/null +++ b/helm/on-line/html/library/control.html @@ -0,0 +1,91 @@ + + + +Control panel + + + + + +
+ + + + + + + + + + + +
+ Format: + + + + + + +
+ (do it also before attempting to take a link to the current page) + +
+ + + +
+
+
+ + diff --git a/helm/on-line/html/library/header.html b/helm/on-line/html/library/header.html new file mode 100644 index 000000000..a1dcbdab7 --- /dev/null +++ b/helm/on-line/html/library/header.html @@ -0,0 +1,18 @@ + + + +Control panel + + + + + + +
+ Index of +
+
+ + diff --git a/helm/on-line/html/library/index.html b/helm/on-line/html/library/index.html new file mode 100644 index 000000000..fb9afb3e4 --- /dev/null +++ b/helm/on-line/html/library/index.html @@ -0,0 +1,60 @@ + + + + + + Index</script> + + + + diff --git a/helm/on-line/html/welcome.html b/helm/on-line/html/welcome.html new file mode 100644 index 000000000..f6fbed438 --- /dev/null +++ b/helm/on-line/html/welcome.html @@ -0,0 +1,6 @@ + + + + + + diff --git a/helm/on-line/icons/back.gif b/helm/on-line/icons/back.gif new file mode 100644 index 000000000..a694ae1ec Binary files /dev/null and b/helm/on-line/icons/back.gif differ diff --git a/helm/on-line/icons/folder.gif b/helm/on-line/icons/folder.gif new file mode 100644 index 000000000..48264601a Binary files /dev/null and b/helm/on-line/icons/folder.gif differ diff --git a/helm/on-line/icons/generic.red.gif b/helm/on-line/icons/generic.red.gif new file mode 100644 index 000000000..94743981d Binary files /dev/null and b/helm/on-line/icons/generic.red.gif differ diff --git a/helm/on-line/javascript/.cvsignore b/helm/on-line/javascript/.cvsignore new file mode 100644 index 000000000..e268d4aeb --- /dev/null +++ b/helm/on-line/javascript/.cvsignore @@ -0,0 +1 @@ +*.js_xml diff --git a/helm/on-line/javascript/Makefile b/helm/on-line/javascript/Makefile new file mode 100644 index 000000000..a2e28081b --- /dev/null +++ b/helm/on-line/javascript/Makefile @@ -0,0 +1,19 @@ + +TARGETS = control.js_xml defaults.js_xml utils.js_xml + +.SUFFIXES: +.SUFFIXES: .js .js_xml + +.js.js_xml: + @echo "" >$@ + @echo "" >>$@ + +all: $(TARGETS) + +clean: + rm -rf $(TARGETS) + diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js new file mode 100644 index 000000000..66412aa9c --- /dev/null +++ b/helm/on-line/javascript/control.js @@ -0,0 +1,138 @@ + +function updateMode(i, s) +{ + var mode = top.mode; + var mode_list = mode.split(","); + var res = ""; + var j; + + for (j = 0; j < mode_list.length; j++) { + if (j == i) res += s; + else res += mode_list[j]; + if (j < mode_list.length - 1) res += ","; + } + + top.mode = res; +} + +function updateOutput(output,format) +{ + 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 mode_list = mode.split(","); + var new_mode = output.options[output.selectedIndex].value; + var dest = "?theoryuri=" + theoryuri + "&cicuri=" + cicuri + "&topurl=" + topurl + "&processorURL=" + processorURL + "&getterURL=" + getterURL + "&mode="; + + if (new_mode != mode_list[0]) { + updateMode(0, new_mode); + if (new_mode == "raw") updateMode(2, format.options[format.selectedIndex].value); + else updateMode(1, format.options[format.selectedIndex].value); + location.search = dest + top.mode; + } +} + +function updateFormat(format) +{ + var mode = top.mode; + var mode_list = mode.split(","); + + if (mode_list[0] == "raw") { + updateMode(1, format.options[format.selectedIndex].value); + } else { + updateMode(2, format.options[format.selectedIndex].value); + } + + refreshReload(); +} + +function updateNatural(checkbox) +{ + if (checkbox.checked) updateMode(3, "yes"); + else updateMode(3, "no"); + refreshReload(); +} + +function updateAnnotations(checkbox) +{ + if (checkbox.checked) updateMode(4, "yes"); + else updateMode(4, "no"); + refreshReload(); +} + +function refreshReload() +{ + var search = + "?mode=" + top.mode + + "&cicuri=" + top.cicuri + + "&theoryuri=" + top.theoryuri + + "&processorURL=" + top.processorURL + + "&getterURL=" + top.getterURL; + + top.frames[0].document.links[0].search = search; + top.frames[0].document.links[1].search = search; + + return true; +} + +function refreshcicHeader(headerURL) +{ + top.cicheader.location.search = "?keys=GP&xmluri=" + headerURL + "¶m.uri=" + top.cicuri; + return true; +} + +function refreshtheoryHeader(headerURL) +{ + top.theoryheader.location.search = "?keys=GP&xmluri=" + headerURL + "¶m.uri=" + top.theoryuri; + return true; +} + +function makeURL(type,uri,cicflags,typesflags) +{ + var mode = top.mode; + var processorURL = top.processorURL; + var getterURL = top.getterURL; + var mode_list = mode.split(","); + + var keys = ""; + var url = ""; + + var output = mode_list[0]; + var format; + if (output == "raw") format = mode_list[1]; + else format = mode_list[2]; + + if (output == "raw") { + url = getterURL + "get?uri=" + uri; + } else { + if (format == "html" && type == "cic") { + keys = "C1,HC2¶m.processorURL=" + escape(processorURL) + + "¶m.getterURL=" + escape(getterURL) + + "¶m.keys=" + escape("C1,HC2"); + } else if (format == "html" && type == "theory") { + keys = "T1,T2,E¶m.processorURL=" + escape(processorURL) + + "¶m.getterURL=" + escape(getterURL) + + "¶m.keys=" + escape("C1,HC2"); + } else if (format == "mml_cont" && type == "cic") { + keys = "C1"; + } else if (format == "mml_cont" && type == "theory") { + keys = "T1,E¶m.keys=C1"; + } else if (format == "mml_pres" && type == "cic") { + keys = "C1,C2"; + } else if (format == "mml_pres" && type == "theory") { + keys = "T1,T2,E¶m.keys=C1,C2"; + } + + var naturalLanguage = typesflags; + if (typesflags != "NO" || type == "theory") { + naturalLanguage = mode_list[3]; + } + url = processorURL + "apply?xmluri=" + escape(getterURL + "get?uri=" + uri) + "&keys=" + keys + "¶m.CICURI=" + uri + "¶m.naturalLanguage=" + naturalLanguage; + } + + return url; +} + diff --git a/helm/on-line/javascript/defaults.js b/helm/on-line/javascript/defaults.js new file mode 100644 index 000000000..f6abf7f87 --- /dev/null +++ b/helm/on-line/javascript/defaults.js @@ -0,0 +1,19 @@ + +function getDefaultParam(name) +{ + switch (name) { + case "processorURL": + return "http://phd.cs.unibo.it:8080/helm/servlet/uwobo/"; + case "getterURL": + return "http://phd.cs.unibo.it:8081/"; + case "cicuri": + return "cic:/"; + case "theoryuri": + return "theory:/"; + case "mode": + return "processed,cic,html,yes,no"; + } + + return "???"; +} + diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js new file mode 100644 index 000000000..dff8c31fa --- /dev/null +++ b/helm/on-line/javascript/prelude.js @@ -0,0 +1,91 @@ + +function getInitialProcessorURL() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var processorURL = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == "processorURL") processorURL = couple[1]; + } + if (processorURL == "-1") processorURL = getDefaultParam("processorURL"); + return processorURL; +} + +function getInitialGetterURL() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var getterURL = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == "getterURL") getterURL = couple[1]; + } + if (getterURL == "-1") getterURL = getDefaultParam("getterURL"); + return getterURL; +} + +function getUwoboURL() +{ + return document.uwoboURL.elements[0].value; +} + +function getGetterURL() +{ + return document.getterURL.elements[0].value; +} + +function refreshLinks() +{ + var search = top.location.search; + search = search.slice(1); + var args = search.split("&"); + var cicuri = "-1", theoryuri = "-1", mode = "-1"; + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + switch (couple[0]) { + case "cicuri" : cicuri =couple[1]; break; + case "theoryuri" : theoryicuri =couple[1]; break; + case "mode" : mode =couple[1]; break; + } + } + if (cicuri == "-1") cicuri = getDefaultParam("cicuri"); + if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri"); + if (mode == "-1") mode = getDefaultParam("mode"); + + document.links[2].search = "?getterURL=" + getGetterURL(); + + document.links[3].search = + "?processorURL=" + getUwoboURL() + + "&getterURL=" + getGetterURL(); + + document.links[4].href = "../html/library/index.html?cicuri=" + cicuri + + "&theoryuri=" + theoryuri + + "&mode=" + mode + + "&processorURL=" + getUwoboURL() + + "&getterURL=" + getGetterURL(); +} + +function selectUwoboURL(ss) +{ + if (ss.selectedIndex == 0) { + document.uwoboURL.elements[0].value = ""; + } else { + document.uwoboURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8080/helm/servlet/uwobo/"; + } + + refreshLink(); +} + +function selectGetterURL(ss) +{ + if (ss.selectedIndex == 0) { + document.getterURL.elements[0].value = ""; + } else { + document.getterURL.elements[0].value = "http://" + ss.options[ss.selectedIndex].value + ":8081/"; + } + + refreshLink(); +} diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js new file mode 100644 index 000000000..7a52b7cbe --- /dev/null +++ b/helm/on-line/javascript/utils.js @@ -0,0 +1,36 @@ +function chopSlash(url) +{ + return url.slice(0,url.lastIndexOf('/')); +} + +function getParam(name) +{ + var search = location.search; + search = search.slice(1); + var args = search.split("&"); + var value = "???"; + + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == name) value = couple[1]; + } + + if (value == "???") value = getDefaultParam(name); + + return value; +} + +function outputOption(doc, value, content, selected) +{ + doc.write(""); +} + +function outputCheckbox(doc, onclick, content, checked) +{ + doc.write("" + content + ""); +} + diff --git a/helm/on-line/xslt/getParam.xsl b/helm/on-line/xslt/getParam.xsl new file mode 100644 index 000000000..0ec71a869 --- /dev/null +++ b/helm/on-line/xslt/getParam.xsl @@ -0,0 +1,28 @@ + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/on-line/xslt/ls2html.xsl b/helm/on-line/xslt/ls2html.xsl new file mode 100644 index 000000000..fc3887719 --- /dev/null +++ b/helm/on-line/xslt/ls2html.xsl @@ -0,0 +1,116 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [{$alt}] + + + + + + + + + + + Index of <xsl:value-of select="$uri"/> + + + + + + + + + + + + + +
+
+ + + + + + + + + + + + + + + + + + + + + + + [{@name}] + + + + + + + +