From: Claudio Sacerdoti Coen Date: Wed, 18 Apr 2001 16:03:13 +0000 (+0000) Subject: annotationHelper now working again. A control frame has been added to X-Git-Tag: v0_1_2~14 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3924d3a11a488176c28af5e82ee3810d9a6350ed;p=helm.git annotationHelper now working again. A control frame has been added to the CIC or the Theory window to invoke the annotationHelper. --- diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html index 106392429..288015dac 100644 --- a/helm/on-line/html/cic/control.html +++ b/helm/on-line/html/cic/control.html @@ -4,7 +4,7 @@ ??? + + + + + + + + +

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

+ + + + + + + + + +

+ View its metadata +	(Not implemented, yet. Coming soon.)
+ Proof-check it +	+ (Not ported to V7, yet. Coming soon.) +

+ + diff --git a/helm/on-line/html/theory/index.html b/helm/on-line/html/theory/index.html new file mode 100644 index 000000000..a1f6e6c46 --- /dev/null +++ b/helm/on-line/html/theory/index.html @@ -0,0 +1,16 @@ + + + + + + ???</script> + + + + diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js index de22891cc..fbc08f3f9 100644 --- a/helm/on-line/javascript/control.js +++ b/helm/on-line/javascript/control.js @@ -103,6 +103,12 @@ function refreshtheoryHeader(headerURL) return true; } +function getCICMathMLKeys() +{ + //Important note: do not modify this function without modifying makeURL + return escape("C1,C2,L"); +} + function makeURL(type,uri,cicflags,typesflags) { var mode = top.mode; @@ -113,7 +119,8 @@ function makeURL(type,uri,cicflags,typesflags) var keys = ""; var url = ""; - var interfaceURL = chopSlash(chopSlash(top.topurl)) + "/cic/index.html"; + var interfaceURL = chopSlash(chopSlash(top.topurl)) + + ((type == "cic") ? "/cic/index.html" : "/theory/index.html"); var output = mode_list[0]; var format; @@ -128,6 +135,8 @@ function makeURL(type,uri,cicflags,typesflags) "&patch_dtd=" + mode_list[6]; } else { if (format == "html" && type == "cic") { + //Important note: do not modify this function without modifying + //getCICMathMLKeys keys = escape("C1,HC2,L")+"¶m.processorURL=" + escape(processorURL) + "¶m.getterURL=" + escape(getterURL) + "&prop.doctype-public="+escape("-//W3C//DTD XHTML 1.0 Transitional//EN")+ @@ -183,6 +192,9 @@ function makeURL(type,uri,cicflags,typesflags) url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "¶m.CICURI=" + uri + "¶m.naturalLanguage=" + naturalLanguage + "¶m.annotations=" + annotations; } - return interfaceURL + "?url=" + escape(url); + if (output == "raw") + return url + else + return interfaceURL + "?url=" + escape(url); } diff --git a/helm/on-line/javascript/utils.js b/helm/on-line/javascript/utils.js index 7a52b7cbe..feab364de 100644 --- a/helm/on-line/javascript/utils.js +++ b/helm/on-line/javascript/utils.js @@ -3,6 +3,37 @@ function chopSlash(url) return url.slice(0,url.lastIndexOf('/')); } +function setParam(url,name,value) +{ + var urla = url.split("?"); + var search = urla[1]; + var args = search.split("&"); + + for (var i = 0 ; i < args.length ; i++) { + var couple = args[i].split("="); + if (couple[0] == name) args[i] = name + "=" + value; + } + + + return (urla[0] + "?" + args.join("&")); +} + +function extractParam(url,name) +{ + var search = url.split("?")[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 getParam(name) { var search = location.search;