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

helm/on-line/html/folder/control.html [new file with mode: 0644] patch | blob
helm/on-line/html/folder/index.html [new file with mode: 0644] patch | blob
helm/on-line/xslt/ls2theory.xsl patch | blob | history
helm/on-line/xslt/toplevel_header.xsl patch | blob | history
helm/on-line/xslt/xslt_index.txt patch | blob | history

diff --git a/helm/on-line/html/folder/control.html b/helm/on-line/html/folder/control.html
new file mode 100644 (file)
index 0000000..34a2f95
--- /dev/null
+++ b/helm/on-line/html/folder/control.html
@@ -0,0 +1,51 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<head>
+
+<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 }
+li     { padding-bottom: 1ex }
+div.center { 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>
+<script>
+ var interfaceURL = "<subst:interfaceURL/>";
+ var url = "<subst:url/>";
+</script>
+
+</head>
+
+<body id="normal">
+ <div class="center">
+   <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/folder.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" target="_top">HELM home</a>
+ </div>
+<!--
+ <ul>
+   <li>
+     <script>
+       var url = "<subst:url/>";
+       document.write('<a href="' + url + '" target="_blank">Open theory in new window</a>');
+     </script>
+   </li>
+ </ul>
+-->
+</body>
+</html>
diff --git a/helm/on-line/html/folder/index.html b/helm/on-line/html/folder/index.html
new file mode 100644 (file)
index 0000000..4c50442
--- /dev/null
+++ b/helm/on-line/html/folder/index.html
@@ -0,0 +1,24 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
+<head>
+ <title><subst:CICURI/></title>
+</head>
+<script>
+ var processorURL = "<subst:processorURL/>";
+ var interfaceURL = "<subst:interfaceURL/>";
+ var profile = "<subst:profile/>";
+ var CICURI = "<subst:CICURI/>";
+ var annotations = "<subst:annotations/>";
+ var url = "<subst:makeTheoryURL/>";
+<![CDATA[
+  document.write('<frameset cols="20%,*" border="1" >');
+  document.write('<frame src="' + processorURL + 'apply?keys=RT&profile=' +
+    profile + '&param.annotations=' + annotations + '&param.CICURI=' + CICURI +
+    '&param.url=' + escape(url) + '&xmluri=' +
+    escape(interfaceURL + 'html/folder/control.html') +'"/>');
+  document.write('<frame src="' + url + '&param.toplevel=true" name="result"/>');
+  document.write('</frameset>');
+]]>
+</script>
+</html>
diff --git a/helm/on-line/xslt/ls2theory.xsl b/helm/on-line/xslt/ls2theory.xsl
index 210ab768bb8fff5d3c4a44265969587bd1014197..5e221bd07f0b8472d18ecb368194f678f556632c 100644 (file)
--- a/helm/on-line/xslt/ls2theory.xsl
+++ b/helm/on-line/xslt/ls2theory.xsl
@@ -9,18 +9,23 @@
   <xsl:output method="html" encoding="iso-8859-1"/>
 
   <xsl:param name="CICURI" select="''" />
+  <xsl:param name="interfaceURL" select="''" />
 
   <xsl:template match="ls">
     <html>
       <head>
        <style>
-         li.section {
+         li.theory {
            list-style-image:
-             url(http://helm.cs.unibo.it/helm/icons/section.png)
+             url(<xsl:value-of select="$interfaceURL"/>/icons/theory.png)
+         }
+         li.folder {
+           list-style-image:
+             url(<xsl:value-of select="$interfaceURL"/>/icons/folder.png)
          }
          li.object {
            list-style-image:
-             url(http://helm.cs.unibo.it/helm/icons/object.png)
+             url(<xsl:value-of select="$interfaceURL"/>/icons/object.png)
          }
        </style>
       </head>
@@ -34,8 +39,8 @@
   </xsl:template>
 
   <xsl:template match="section">
-    <li class="section">
-      <a class="section" href="{concat($CICURI, text(), '/')}"
+    <li class="folder">
+      <a class="folder" href="{concat($CICURI, text(), '/')}"
        helm:helm_link="href">
        <xsl:value-of select="text()" />
       </a>
@@ -44,11 +49,25 @@
   </xsl:template>
 
   <xsl:template match="object">
-    <li class="object">
-      <a class="object" href="{concat($CICURI, @name)}" helm:helm_link="href">
-       <xsl:value-of select="@name" />
-      </a>
-    </li>
+    <xsl:choose>
+      <xsl:when test="substring-after(@name, '.')='theory'">
+       <li class="theory">
+         <a class="theory" href="{concat($CICURI, @name)}"
+           helm:helm_link="href">
+           <xsl:value-of select="@name" />
+         </a>
+       </li>
+      </xsl:when>
+      <xsl:otherwise>
+       <li class="object">
+         <a class="object"
+           href="{concat('cic:', substring-after($CICURI, ':'), @name)}"
+           helm:helm_link="href">
+           <xsl:value-of select="@name" />
+         </a>
+       </li>
+      </xsl:otherwise>
+    </xsl:choose>
   </xsl:template>
 
 </xsl:stylesheet>
diff --git a/helm/on-line/xslt/toplevel_header.xsl b/helm/on-line/xslt/toplevel_header.xsl
index a22213a2edc4b2c44200c54a543c5d48abd80d01..deca927a1531a7ce49b93f8771fa61791d05914d 100644 (file)
--- a/helm/on-line/xslt/toplevel_header.xsl
+++ b/helm/on-line/xslt/toplevel_header.xsl
@@ -34,7 +34,7 @@
   <xsl:variable name="prefix" select="substring-before($CICURI, ':')" />
   <html:table width="100%">
     <html:tr>
-      <html:td style="text-align:left">
+      <html:td>
        <html:h3 style="font-family: sans-serif">
          <html:a style="text-decoration: none"
            href="{concat($prefix, ':/')}" helm:helm_link="href">
@@ -48,6 +48,12 @@
          </xsl:call-template>
        </html:h3>
       </html:td>
+      <html:td style="text-align:right">
+       <html:span style="font-family:sans-serif">
+         <html:a href="">Search</html:a>
+       </html:span>
+      </html:td>
+<!--
       <html:td style="text-align:right">
        <html:span style="font-family:sans-serif">
          <html:a href="theory:/" helm:helm_link="href">theory:/</html:a>
@@ -55,6 +61,7 @@
          <html:a href="cic:/" helm:helm_link="href">cic:/</html:a>
        </html:span>
       </html:td>
+-->
     </html:tr>
   </html:table>
   <html:hr />
diff --git a/helm/on-line/xslt/xslt_index.txt b/helm/on-line/xslt/xslt_index.txt
index 7d1abeb38276cc04967c6e9264b420e7336c9d9d..3b62468395838942a18019bce55482858686d163 100644 (file)
--- a/helm/on-line/xslt/xslt_index.txt
+++ b/helm/on-line/xslt/xslt_index.txt
@@ -5,5 +5,6 @@ makeGraphLinks.xsl
 metadataControl.xsl
 metadataLib.xsl
 resolve_topurl.xsl
+substKey.xsl
 toplevel_header.xsl
 utils.xsl
Unnamed repository; edit this file 'description' to name the repository.