From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 Jun 2004 10:12:46 +0000 (+0000)
Subject: Uncommited changes committed.
X-Git-Tag: pre_subst_in_kernel~35
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69bc5e13a65c76bcda125c9f11ef51fc0343ae12;p=helm.git

Uncommited changes committed.
---

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index 126772343..8e6aeaf1f 100644
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -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=" +
diff --git a/helm/on-line/html/folder/control.html b/helm/on-line/html/folder/control.html
index a3d6c0fed..32c5d71ed 100644
--- a/helm/on-line/html/folder/control.html
+++ b/helm/on-line/html/folder/control.html
@@ -44,7 +44,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/folder.png" />');
    </script>
  <h2 class="uri"><subst:base_CICURI/></h2>
diff --git a/helm/on-line/html/theory/index.html b/helm/on-line/html/theory/index.html
index d64a5745a..711ad87ba 100644
--- a/helm/on-line/html/theory/index.html
+++ b/helm/on-line/html/theory/index.html
@@ -18,7 +18,7 @@
     '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
     '&param.url=' + escape(url) + '&xmluri=' +
     escape(interfaceURL + 'html/theory/control.html') +'"/>');
-  document.write('<frame src="' + url + '&param.toplevel=true" name="result"/>');
+  document.write('<frame src="' + url + '" name="result"/>');
   document.write('</frameset>');
 ]]>
 </script>