annotationHelper now working again. A control frame has been added to

[helm.git] / helm / on-line / html / theory / control.html
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>