]> 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: a3e1fde)
annotationHelper now working again. A control frame has been added to
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Apr 2001 16:03:13 +0000 (16:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Apr 2001 16:03:13 +0000 (16:03 +0000)
the CIC or the Theory window to invoke the annotationHelper.

helm/on-line/html/cic/control.html patch | blob | history
helm/on-line/html/cic/index.html patch | blob | history
helm/on-line/html/theory/control.html [new file with mode: 0644] patch | blob
helm/on-line/html/theory/index.html [new file with mode: 0644] patch | blob
helm/on-line/javascript/control.js patch | blob | history
helm/on-line/javascript/utils.js patch | blob | history

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index 106392429a79f27fbc9ea539685c592dffe88c2d..288015dace02eab1d6f3d8862e2a993385766bdb 100644 (file)
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -4,7 +4,7 @@
 <title>???</title>
 
 <style type="text/css">
-#normal { background-color: white; font-family: sans-serif }
+#normal { background-color: #e6e6fa; 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 }
@@ -13,18 +13,49 @@ td.back { background-color: #e6e6fa; color: brown }
 
 <script language="JavaScript" src="../../javascript/defaults.js"></script>
 <script language="JavaScript" src="../../javascript/utils.js"></script>
+<script language="JavaScript" src="../../javascript/control.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>
+ <h1>Object: 
+  &quot;<script>document.write(extractParam(unescape(getParam('url')),'param.CICURI'))</script>&quot;
+ &nbsp;&nbsp;&nbsp;<font size="+1">[Annotations are
+ <script>if ((extractParam(unescape(getParam('url')),'param.annotations')) == 'NO') document.write('off'); else document.write('on')</script>
+ ]</font>
+ </h1>
+ <table>
+  <tr>
+   <td>
+    <script>
+     var url = unescape(getParam('url'));
+     url = setParam(url,"keys",getCICMathMLKeys());
+     url = setParam(url,"prop.doctype-public","");
+     url = setParam(url,"prop.encoding","");
+     url = setParam(url,"prop.media-type","application/x-helm-annotation-helper");
+     document.write(
+      '<a target="result" href="' + url + '">Annotate it</a>'
+     )
+    </script>
+   </td>
+   <td>
+    (Before following the link, you must install the HELM Annotation Helper)
+   </td>
+  </tr>
+  <tr>
+   <td>
+    View its metadata
+   </td>
+   <td>(Not implemented, yet. Coming soon.)</td>
+  </tr>
+  <tr>
+   <td>
+    Proof-check it
+   </td>
+   <td>
+    (Not ported to V7, yet. Coming soon.)
+   </td>
+  </tr>
+ </table>
 </body>
 </html>
diff --git a/helm/on-line/html/cic/index.html b/helm/on-line/html/cic/index.html
index c0611022cf52a4f96b3da6d204164b9a5c2a97b9..c40fd06cb4007b5b383dd0f3a636c1761286554a 100644 (file)
--- a/helm/on-line/html/cic/index.html
+++ b/helm/on-line/html/cic/index.html
@@ -9,7 +9,7 @@
 <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="' + unescape(getParam('url')) + '" + name="result"/>');
 /*
   document.write('<frame src="control.html' +
        '?topurl=' + location.protocol + "//" + location.host + location.pathname +
diff --git a/helm/on-line/html/theory/control.html b/helm/on-line/html/theory/control.html
new file mode 100644 (file)
index 0000000..d399941
--- /dev/null
+++ b/helm/on-line/html/theory/control.html
@@ -0,0 +1,42 @@
+<html>
+
+<head>
+<title>???</title>
+
+<style type="text/css">
+#normal { background-color: #e6e6fa; 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>
+<script language="JavaScript" src="../../javascript/control.js"></script>
+
+</head>
+
+<body id="normal">
+ <h1>Theory: 
+  &quot;<script>document.write(extractParam(unescape(getParam('url')),'param.CICURI'))</script>&quot;
+ &nbsp;&nbsp;&nbsp;<font size="+1">[Annotations have no meaning for theories, yet]</font>
+ </h1>
+ <table>
+  <tr>
+   <td>
+    View its metadata
+   </td>
+   <td>(Not implemented, yet. Coming soon.)</td>
+  </tr>
+  <tr>
+   <td>
+    Proof-check it
+   </td>
+   <td>
+    (Not ported to V7, yet. Coming soon.)
+   </td>
+  </tr>
+ </table>
+</body>
+</html>
diff --git a/helm/on-line/html/theory/index.html b/helm/on-line/html/theory/index.html
new file mode 100644 (file)
index 0000000..a1f6e6c
--- /dev/null
+++ b/helm/on-line/html/theory/index.html
@@ -0,0 +1,16 @@
+<!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')) + '" + name="result"/>');
+  document.write('</frameset>');
+</script>
+
+</html>
diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index de22891cc09b3fc74d4fa2c11b17448bfe30116a..fbc08f3f9b692e38f3fd33c53992cb3fa308b93d 100644 (file)
--- 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")+"&param.processorURL=" + escape(processorURL) +
        "&param.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 + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.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 7a52b7cbe6d491200ae44cffdede8665ada7ff7f..feab364de235d77bd30d79ca59974bd9b8c8ae5c 100644 (file)
--- 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;
Unnamed repository; edit this file 'description' to name the repository.