X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fon-line%2Fhtml%2Fcic%2Fcontrol.html;h=1697419970723bb5a6f096e0a40c8ca0b553cc5a;hb=b4a7a577a04c56a68b6d79d06fdb925ff0bbd331;hp=288015dace02eab1d6f3d8862e2a993385766bdb;hpb=3924d3a11a488176c28af5e82ee3810d9a6350ed;p=helm.git

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index 288015dac..169741997 100644
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -21,10 +21,21 @@ td.back { background-color: #e6e6fa; color: brown }
  <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>
+ <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'));
+     document.write('<a href="' + url + '" target="_blank">Object URL</a>');
+     </script>
+   </td>
+   <td>
+    Follow the link to view the displayed object alone (without this control frame)
+   </td>
+  </tr>
   <tr>
    <td>
     <script>
@@ -33,6 +44,7 @@ td.back { background-color: #e6e6fa; color: brown }
      url = setParam(url,"prop.doctype-public","");
      url = setParam(url,"prop.encoding","");
      url = setParam(url,"prop.media-type","application/x-helm-annotation-helper");
+     url = url + "&param.explodeall=true";
      document.write(
       '<a target="result" href="' + url + '">Annotate it</a>'
      )
@@ -44,16 +56,37 @@ td.back { background-color: #e6e6fa; color: brown }
   </tr>
   <tr>
    <td>
-    View its metadata
+    <script>
+     var url = unescape(getParam('url'));
+     var getterURL = extractParam(url,'param.getterURL');
+     var CICURI = dropBodySuffix(extractParam(url,'param.CICURI'));
+     url = setParam(url,"keys","MC%2CRT");
+     url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + CICURI);
+     url = setParam(url,"prop.media-type","text/html");
+     url = setParam(url,"prop.encoding","iso-8859-1");
+     url = setParam(url,"param.CICURI",CICURI);
+     document.write(
+      '<a target="_blank" href="' + url + '">View its metadata and dependencies</a>'
+     );
+    </script>
+   </td>
+   <td>DC Metadata and dependency metadata; Dependency graphs
    </td>
-   <td>(Not implemented, yet. Coming soon.)</td>
   </tr>
   <tr>
    <td>
-    Proof-check it
+    <script>
+     var url = unescape(getParam('url'));
+     var proofcheckerURL = unescape(extractParam(url,'param.proofcheckerURL'));
+     var CICURI = dropBodySuffix(extractParam(url,'param.CICURI'));
+     url = proofcheckerURL + "proofCheck?uri=" + CICURI;
+     document.write(
+      '<a target="_blank" href="' + url + '">Proof-check it</a>'
+     );
+    </script>
    </td>
-   <td>
-    (Not ported to V7, yet. Coming soon.)
+   <td>Proof-checking is recursively performed over the untrusted parts of the
+       library
    </td>
   </tr>
  </table>