]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 55b6c7c)
Control panel added to CIC window
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 11 Apr 2001 11:03:00 +0000 (11:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 11 Apr 2001 11:03:00 +0000 (11:03 +0000)
helm/on-line/html/cic/control.html [new file with mode: 0644] patch | blob
helm/on-line/html/cic/index.html [new file with mode: 0644] patch | blob
helm/on-line/javascript/control.js patch | blob | history
helm/on-line/xslt/ls2html.xsl patch | blob | history

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
new file mode 100644 (file)
index 0000000..1063924
--- /dev/null
+++ b/helm/on-line/html/cic/control.html
@@ -0,0 +1,30 @@
+<html>
+
+<head>
+<title>???</title>
+
+<style type="text/css">
+#normal { background-color: white; font-family: sans-serif }
+td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
+td.back { background-color: #e6e6fa; color: brown }
+#indent { margin-left: 1cm; margin-right: 1cm }
+#centered { text-align: center }
+</style>
+
+<script language="JavaScript" src="../../javascript/defaults.js"></script>
+<script language="JavaScript" src="../../javascript/utils.js"></script>
+
+</head>
+
+<body id="normal">
+ <center>
+  <h1>Broken control frame. Useful soon! (stay tooned)</h1>
+ </center>
+<form>
+ <script>document.write('<textarea rows="1" cols="75">' +
+  unescape(getParam('url')) +
+  '</textarea>');
+ </script>
+</form>
+</body>
+</html>
diff --git a/helm/on-line/html/cic/index.html b/helm/on-line/html/cic/index.html
new file mode 100644 (file)
index 0000000..c061102
--- /dev/null
+++ b/helm/on-line/html/cic/index.html
@@ -0,0 +1,44 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html>
+<head>
+ <script language="JavaScript" src="../../javascript/defaults.js"></script>
+ <script language="JavaScript" src="../../javascript/utils.js"></script>
+ <title>???</script></title>
+</head>
+<script>
+  document.write('<frameset rows="18%,*" border="0" scrolling="no">');
+  document.write('<frame src="control.html?url=' + getParam('url') +'"/>');
+  document.write('<frame src="' + unescape(getParam('url')) + '"/>');
+/*
+  document.write('<frame src="control.html' +
+       '?topurl=' + location.protocol + "//" + location.host + location.pathname +
+       '&mode=' + getParam('mode') +
+       '&cicuri=' + getParam('cicuri') +
+       '&theoryuri=' + getParam('theoryuri') +
+       '&processorURL=' + getParam('processorURL') +
+       '&getterURL=' + getParam('getterURL') +
+       '" name="control"/>');
+*/
+/*
+  document.write('<frame src="' +
+       getParam('processorURL') + 'apply' +
+       '?keys=GP' +
+       '&xmluri=' + location.protocol + "//" + location.host + chopSlash(location.pathname) + "/header.html" +
+       '&param.uri=' + getParam('theoryuri') + 
+       '" name="theoryheader"/>');
+  document.write('<frame src="' +
+       getParam('processorURL') + 'apply' +
+       '?keys=L2H' +
+       '&xmluri=' + escape(getParam('getterURL') + 'ls?format=xml&baseuri=' + getParam('theoryuri')) +
+        '&param.keys=L2H' +
+       '&param.uri=' + getParam('theoryuri') +
+       '&param.getterURL=' + getParam('getterURL') +
+        '&param.target=theory' +
+       '&param.interfaceURL=' + location.protocol + "//" + location.host + chopSlash(chopSlash(chopSlash(location.pathname))) + 
+       '" name="theoryresult"/>');
+*/
+  document.write('</frameset>');
+</script>
+
+</html>
diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 74903c692f5f7df156290cfd6b6c445d54ba3c5d..de22891cc09b3fc74d4fa2c11b17448bfe30116a 100644 (file)
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -113,6 +113,8 @@ function makeURL(type,uri,cicflags,typesflags)
   var keys = "";
   var url = "";
 
+  var interfaceURL = chopSlash(chopSlash(top.topurl)) + "/cic/index.html";
+
   var output = mode_list[0];
   var format;
   if (output == "raw") format = mode_list[1];
@@ -134,7 +136,8 @@ 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("C1,HC2,L");
+       "&param.keys=" + escape("C1,HC2,L") +
+       "&param.interfaceURL=" + escape(interfaceURL);
     } else if (format == "html" && type == "theory") {
       keys = escape("T1,T2,L,E")+"&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
@@ -142,7 +145,8 @@ 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("C1,HC2,L");
+       "&param.keys=" + escape("C1,HC2,L") +
+       "&param.interfaceURL=" + escape(interfaceURL);
     } else if (format == "mml_cont" && type == "cic") {
       keys = "C1";
     } else if (format == "mml_cont" && type == "theory") {
@@ -156,14 +160,16 @@ function makeURL(type,uri,cicflags,typesflags)
        "&param.doctype-public=" +
        "&param.encoding=" +
        "&param.media-type=text/xml" +
-       "&param.keys=" + escape("C1,C2,L");
+       "&param.keys=" + escape("C1,C2,L") +
+       "&param.interfaceURL=" + escape(interfaceURL);
     } else if (format == "mml_pres" && type == "theory") {
-      keys = escape("T1,T2,L,E")+"&param.keys=C1,C2&param.thkeys=TC1,C2,L" +
+      keys = escape("T1,T2,L,E")+"&param.keys=C1,C2,L&param.thkeys=TC1,C2,L" +
        "&param.processorURL=" + escape(processorURL) +
        "&param.getterURL=" + escape(getterURL) +
        "&param.doctype-public=" +
        "&param.encoding=" +
-       "&param.media-type=text/xml";
+       "&param.media-type=text/xml" +
+       "&param.interfaceURL=" + escape(interfaceURL);
     }
 
     var naturalLanguage = typesflags;
@@ -177,6 +183,6 @@ function makeURL(type,uri,cicflags,typesflags)
     url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations;
   }
 
-  return url;
+  return interfaceURL + "?url=" + escape(url);
 }
 
diff --git a/helm/on-line/xslt/ls2html.xsl b/helm/on-line/xslt/ls2html.xsl
index 4521eaaf46069aa55aa0d71ad576e87eb45d253c..606d750f827ba4fdd83ce6816c9e70fae8657f1f 100644 (file)
--- a/helm/on-line/xslt/ls2html.xsl
+++ b/helm/on-line/xslt/ls2html.xsl
@@ -66,6 +66,7 @@
   <head>
    <title>Index of <xsl:value-of select="$uri"/></title>
    <xsl:copy-of select="document(concat($interfaceURL,'/javascript/control.js_xml'))" />
+   <xsl:copy-of select="document(concat($interfaceURL,'/javascript/utils.js_xml'))" />
   </head>
   <body bgcolor="#ffffff" text="#000000">
    <table>
Unnamed repository; edit this file 'description' to name the repository.