]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/html/cic/control.html
ocaml 3.09 transition
[helm.git] / helm / on-line / html / cic / control.html
index 126772343a2989ab13f6d3f00604bba72266b002..8e6aeaf1f7614b3f6b9f23aa490c642f7022e413 100644 (file)
@@ -24,6 +24,7 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
  var DirectRDFURL = "<subst:DirectRDFURL/>";
  var getterURL = "<subst:getterURL/>";
  var HTMLURL = "<subst:HTMLURL/>";
+ var ProofTreeURL = "<subst:makeProofTreeURL/>";
  var InverseRDFURL = "<subst:InverseRDFURL/>";
  var MathMLContentURL = "<subst:MathMLContentURL/>";
  var MathMLPresentationURL = "<subst:MathMLPresentationURL/>";
@@ -59,7 +60,7 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
  <hr />
  <div class="center">
    <script>
-     document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
+     document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '">');
      document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/object.png" />');
    </script>
   <h2 class="uri"><subst:base_CICURI/></h2>
@@ -86,6 +87,11 @@ h2.uri { margin-top: 0ex; margin-bottom: 0ex }
      document.write('<a href="' + MathMLPresentationURL + '&amp;param.toplevel=true" target="result"><small>MathML</small></a> ]');
      </script>
   </li>
+  <li>
+    <script>
+      document.write('<a href="' + ProofTreeURL + '&amp;param.toplevel=true" target="result">View proof tree</a>');
+    </script>
+  </li>
   <li>
     <script>
      var url = processorURL + "apply?keys=MC%2CRT%2CL&amp;xmluri=" +