]> 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: b866f53)
Major interface upgrade still going on. But we are approaching the end of
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 May 2004 17:51:38 +0000 (17:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 May 2004 17:51:38 +0000 (17:51 +0000)
the tunnel.

helm/on-line/html/cic/control.html patch | blob | history
helm/on-line/html/theory/control.html patch | blob | history

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index 1868818b705aff80a5849388885822c60d260725..3dc908db5d210504b82c10707f52fb713f193197 100644 (file)
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -25,6 +25,7 @@ div.center { text-align: center }
  var InverseRDFURL = "<subst:InverseRDFURL/>";
  var MathMLContentURL = "<subst:MathMLContentURL/>";
  var MathMLPresentationURL = "<subst:MathMLPresentationURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
  var mkDirDepURL = "<subst:makeDirectDependencyURL/>";
  var mkInvDepURL = "<subst:makeInverseDirectDependencyURL/>";
  var mkInvRecDepURL = "<subst:makeInverseRecDependencyURL/>";
@@ -38,8 +39,10 @@ div.center { text-align: center }
 
 <body id="normal">
  <div class="center">
-  <script>document.write('&lt;a target="result" style="text-decoration:none" href="' + url + '">');</script>
-  <img style="border-style:none" src="http://helm.cs.unibo.it/helm/icons/object.png" />
+   <script>
+     document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
+     document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/object.png" />');
+   </script>
   <h2><subst:base_CICURI/></h2>
   <script>document.write('&lt;/a>');</script>
  </div>
@@ -160,7 +163,7 @@ div.center { text-align: center }
 </ul>
 <hr />
 <div class="center">
-  <a href="http://helm.cs.unibo.it">HELM home</a>
+  <a href="http://helm.cs.unibo.it" target="_top">HELM home</a>
 </div>
 </body>
 </html>
diff --git a/helm/on-line/html/theory/control.html b/helm/on-line/html/theory/control.html
index 637c563da4f4f832a78d140152931379d3d16ac2..ffc2e82d224fc9e0b5b9591d206161b105546d03 100644 (file)
--- a/helm/on-line/html/theory/control.html
+++ b/helm/on-line/html/theory/control.html
@@ -17,17 +17,25 @@ div.center { text-align: center }
 <script language="JavaScript" src="../../javascript/defaults.js"></script>
 <script language="JavaScript" src="../../javascript/utils.js"></script>
 <script language="JavaScript" src="../../javascript/control.js"></script>
+<script>
+ var interfaceURL = "<subst:interfaceURL/>";
+ var url = "<subst:url/>";
+</script>
 
 </head>
 
 <body id="normal">
  <div class="center">
- <img src="http://helm.cs.unibo.it/helm/icons/section.png" />
+   <script>
+     document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '&amp;param.toplevel=true">');
+     document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/theory.png" />');
+   </script>
  <h2><subst:base_CICURI/></h2>
+  <script>document.write('&lt;/a>');</script>
  </div>
  <hr />
  <div class="center">
-  <a href="http://helm.cs.unibo.it">HELM home</a>
+  <a href="http://helm.cs.unibo.it" target="_top">HELM home</a>
  </div>
 <!--
  <ul>
Unnamed repository; edit this file 'description' to name the repository.