From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Jun 2001 17:44:41 +0000 (+0000)
Subject: First version of metadata interface.
X-Git-Tag: v0_1_3~127
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40aaf8dcb5f4251186d6b4380ded7cf50ffd5345;p=helm.git

First version of metadata interface.
Still many things to be fixed and one stylesheet (of Andrea) not committed.
But it is a new beginning...
---

diff --git a/helm/on-line/html/cic/control.html b/helm/on-line/html/cic/control.html
index 288015dac..29a222faa 100644
--- a/helm/on-line/html/cic/control.html
+++ b/helm/on-line/html/cic/control.html
@@ -44,9 +44,27 @@ 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 = extractParam(url,'param.CICURI');
+     var RDFURI = "helm:rdf:www.cs.unibo.it/helm/rdf/rdfprova//" + CICURI;
+     if (CICURI.substr(-4,4) == ".ind") {
+      url = setParam(url,"keys","DM%2CRT");
+      url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + CICURI);
+     } else {
+      url = setParam(url,"keys","MC%2CRT");
+      url = setParam(url,"xmluri", getterURL + "resolve%3Furi%3D" + RDFURI);
+     }
+     url =
+      url +
+      "&param.RDFURI=" + RDFURI ;
+     document.write(
+      '<a target="metadata" href="' + url + '">View its metadata</a>'
+     );
+    </script>
    </td>
-   <td>(Not implemented, yet. Coming soon.)</td>
+   <td>(Work in progress. Coming soon.)</td>
   </tr>
   <tr>
    <td>
diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index 472100b9f..1f811dc68 100644
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -235,7 +235,7 @@ function makeURL(type,uri,cicflags,typesflags)
     if (cicflags != "NO" || type == "theory") {
        annotations = mode_list[4];
     }
-    url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations;
+    url = processorURL + "apply?xmluri=" + escape(getterURL + "getxml?uri=" + uri) + "&keys=" + keys + "&param.CICURI=" + uri + "&param.naturalLanguage=" + naturalLanguage + "&param.annotations=" + annotations + "&param.topurl=" + top.topurl;
   }
 
   if (output == "raw")
diff --git a/helm/on-line/xslt/demultiplexMutual.xsl b/helm/on-line/xslt/demultiplexMutual.xsl
new file mode 100644
index 000000000..2f8650937
--- /dev/null
+++ b/helm/on-line/xslt/demultiplexMutual.xsl
@@ -0,0 +1,38 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<xsl:output 
+	method="xml"
+	encoding="iso-8859-1" 
+	media-type="text/html"
+ 	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
+  	doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
+
+<xsl:param name="RDFURI" select="''"/>
+
+<!-- BUG UWOBO -->
+<xsl:include href="http://phd.cs.unibo.it/helm/xslt/metadataLib.xsl"/>
+
+<xsl:variable name="url" select="concat($getterURL,'resolve?uri=')"/>
+
+<xsl:template match="InductiveDefinition">
+ <xsl:for-each select="InductiveType">
+  <xsl:variable name="RDFURIInductiveType" select="concat($RDFURI,',',position())"/>
+   <xsl:apply-templates select="document(concat($url,$RDFURIInductiveType))" mode="makelink">
+    <xsl:with-param name="name" select="@name"/>
+    <xsl:with-param name="RDFURI" select="$RDFURIInductiveType"/>
+   </xsl:apply-templates>
+  <xsl:for-each select="Constructor">
+   <xsl:variable name="RDFURIConstructor" select="concat($RDFURIInductiveType,',',position())"/>
+   <xsl:apply-templates select="document(concat($url,$RDFURIConstructor))" mode="makelink">
+    <xsl:with-param name="name" select="@name"/>
+    <xsl:with-param name="RDFURI" select="$RDFURIConstructor"/>
+   </xsl:apply-templates>
+  </xsl:for-each>
+ </xsl:for-each>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/on-line/xslt/metadataControl.xsl b/helm/on-line/xslt/metadataControl.xsl
new file mode 100644
index 000000000..c33d7b2b4
--- /dev/null
+++ b/helm/on-line/xslt/metadataControl.xsl
@@ -0,0 +1,26 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<xsl:output 
+	method="xml"
+	encoding="iso-8859-1" 
+	media-type="text/html"
+ 	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
+  	doctype-system="http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd" />
+
+<xsl:param name="RDFURI" select="''"/>
+
+<!-- BUG UWOBO -->
+<xsl:include href="http://phd.cs.unibo.it/helm/xslt/metadataLib.xsl"/>
+
+<xsl:template match="unresolved|url">
+ <xsl:apply-templates mode="makelink" select=".">
+  <xsl:with-param name="name" select="$CICURI"/>
+  <xsl:with-param name="RDFURI" select="$RDFURI"/>
+ </xsl:apply-templates>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/on-line/xslt/metadataLib.xsl b/helm/on-line/xslt/metadataLib.xsl
new file mode 100644
index 000000000..f264516b2
--- /dev/null
+++ b/helm/on-line/xslt/metadataLib.xsl
@@ -0,0 +1,59 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:subst="http://www.cs.unibo.it/helm/subst">
+
+<xsl:param name="CICURI" select="''"/>
+<xsl:param name="getterURL" select="''"/>
+
+<xsl:template match="/">
+ <html>
+  <head>
+   <subst:script language="JavaScript" src="/javascript/defaults.js"/>
+   <subst:script language="JavaScript" src="/javascript/utils.js"/>
+   <subst:script language="JavaScript" src="/javascript/control.js"/>
+   <title>Metadata of <xsl:value-of select="$CICURI"/></title>
+  </head>
+  <body bgColor="white">
+   <h1>Metadata of <xsl:value-of select="$CICURI"/></h1>
+   <xsl:apply-templates select="*"/>
+  </body>
+ </html>
+</xsl:template>
+
+<xsl:template match="/" mode="makelink">
+ <xsl:param name="name" select="''"/>
+ <xsl:param name="RDFURI" select="''"/>
+ <xsl:apply-templates select="*" mode="makelink">
+  <xsl:with-param name="name" select="$name"/>
+  <xsl:with-param name="RDFURI" select="$RDFURI"/>
+ </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="unresolved" mode="makelink">
+ <xsl:param name="name" select="''"/>
+ <p>
+  Object <xsl:value-of select="$name"/> is never referenced in other objects
+ </p>
+</xsl:template>
+
+<xsl:template match="url" mode="makelink">
+ <xsl:param name="name" select="''"/>
+ <xsl:param name="RDFURI" select="''"/>
+ <p>
+  <script>
+   var name = "<xsl:value-of select="$name"/>";
+   var RDFURI = "<xsl:value-of select="$RDFURI"/>";
+   var getterURL = "<xsl:value-of select="$getterURL"/>";
+<![CDATA[
+   //url = setParam(url,"keys",getCICMathMLKeys());
+   var url = setParam(location.href,"keys","mth");
+   url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + RDFURI);
+   document.write('<a href="' + url + '">View the objects depending on ' + name + '.</a>');
+]]>
+  </script>
+ </p>
+</xsl:template>
+
+</xsl:stylesheet>
diff --git a/helm/uwobo-panel/control.html b/helm/uwobo-panel/control.html
index efa1f8571..51050ad7c 100644
--- a/helm/uwobo-panel/control.html
+++ b/helm/uwobo-panel/control.html
@@ -226,6 +226,8 @@ the getter is used by default (you can deselect it, however):
         <option value="L2H,http://phd.cs.unibo.it/helm/xslt/ls2html.xsl,false">Getter LS ==&gt; HTML</option>
         <option value="GP,http://phd.cs.unibo.it/helm/xslt/getParam.xsl,false">Get Param</option>
         <option value="RT,http://phd.cs.unibo.it/helm/xslt/resolve_topurl.xsl,false">Logic-sheet to substitute the interface URL</option>
+        <option value="DM,http://phd.cs.unibo.it/helm/xslt/demultiplexMutual.xsl,false">Stylesheet to create the link to the metadata for inductive types</option>
+        <option value="MC,http://phd.cs.unibo.it/helm/xslt/metadataControl.xsl,false">Stylesheet to create the link to the metadata for constants and variables</option>
       </select>
     </form>
   </td>