X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=533cf22998ed1cceaa23e55e7f89644e601a0a00;hb=e1d232bab1b061d9098fd666ca24bed84b38f99e;hp=cd17b6d4cd45f7c74b243de257ffac390b81cee8;hpb=2e365db5721e934b77f3648ab7df6d31a02142b2;p=helm.git

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index cd17b6d4c..533cf2299 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -35,10 +35,11 @@
 <xsl:param name="getterURL" select="'http://localhost:8081/'"/>
 <xsl:param name="processorURL" select="'http://localhost:8080/helm/servlet/uwobo/'"/>
 <xsl:param name="keys" select="'C1,HC2'"/>
+<xsl:param name="naturalLanguage" select="'yes'"/>
 
 <xsl:variable name="absPath"><xsl:value-of select="$getterURL"/>getciconly?uri=</xsl:variable>
 
-<xsl:variable name="header"><xsl:value-of select="$processorURL"/>/apply?keys=<xsl:value-of select="$keys"/>&#x26;param.keys=<xsl:value-of select="$keys"/>&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
+<xsl:variable name="header"><xsl:value-of select="$processorURL"/>apply?keys=<xsl:value-of select="$keys"/>&#x26;param.naturalLanguage=<xsl:value-of select="$naturalLanguage"/>&#x26;param.keys=<xsl:value-of select="$keys"/>&#x26;param.getterURL=<xsl:value-of select="$getterURL"/>&#x26;param.processorURL=<xsl:value-of select="$processorURL"/>&#x26;xmluri=<xsl:value-of select="$absPath"/></xsl:variable>
 
 <xsl:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
@@ -46,13 +47,27 @@
 
 <xsl:variable name="showcast" select="0"/>
 
+<xsl:template name="makeURL">
+ <xsl:param name="url" select="''"/>
+ <xsl:value-of select="concat(string($header),string($url),'&#x26;param.CICURI=',string($url))"/>
+</xsl:template>
 
 <!--***********************************************************************-->
 <!-- HTML Head and Body                                                    -->
 <!--***********************************************************************-->
 
-<!-- <xsl:output method="html"/> -->
-<xsl:output method="html" encoding="iso-8859-1"/>
+<!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
+
+<!-- document needs method="xml" and searches locally for the dtd if        -->
+<!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
+<!-- For having output html must be media-type="html" and for having the    -->
+<!-- correct <br /> you must specify at least the remote dtd by means of    -->
+<!-- doctype-public                                                         -->
+<xsl:output 
+	method="xml" 
+	encoding="iso-8859-1" 
+	media-type="text/html"
+	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
 
 <xsl:variable name="framewidth" select="36"/>
 
@@ -121,7 +136,9 @@
   <xsl:when test="boolean(@definitionURL)">
    <a>
    <xsl:attribute name="href">
-    <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
+    <xsl:call-template name="makeURL">
+     <xsl:with-param name="url" select="@definitionURL"/>
+    </xsl:call-template>
    </xsl:attribute>
    <xsl:apply-templates/>
    </a>
@@ -268,16 +285,16 @@
      <FONT color="red">From&#x00a0;</FONT>
      <xsl:apply-templates select="*[2]"/>
      <FONT color="red">&#x00a0;we get</FONT>
-     <m:mtext>(</m:mtext>
+     (
      <xsl:apply-templates select="*[3]"/>
-     <m:mtext>)&#x00a0;</m:mtext>
+     )&#x00a0;
      <xsl:apply-templates mode="inline" select="*[4]"/>
      <FONT color="red">&#x00a0;and&#x00a0;</FONT>
-     <m:mtext>(</m:mtext>
+     (
      <xsl:apply-templates select="*[5]"/>
-     <m:mtext>)&#x00a0;</m:mtext>
+     )&#x00a0;
      <xsl:apply-templates mode="inline" select="*[6]"/>
-     <m:mtext>;</m:mtext>
+     ;
      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
      <xsl:apply-templates mode="inline" select="*[7]"/>
     </xsl:when>
@@ -319,7 +336,7 @@
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
           <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
          </xsl:apply-templates>
          <br/>
          <xsl:call-template name="make_indent">
@@ -344,7 +361,7 @@
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
           <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
          </xsl:apply-templates><br/> 
          <xsl:call-template name="make_indent">
           <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
@@ -610,9 +627,9 @@
       </xsl:when>
       <!-- Let -->
       <xsl:when test="$name='let'">
-       <m:mtext>(</m:mtext>
+       (
        <xsl:apply-templates select="m:ci"/>
-       <m:mtext>) </m:mtext>
+       )
        <xsl:apply-templates select="*[3]">
         <xsl:with-param name="current_indent" select="$current_indent + 7"/>
        </xsl:apply-templates>
@@ -675,9 +692,9 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       <m:mtext>(</m:mtext>
+       (
        <xsl:apply-templates select="*[3]"/>
-       <m:mtext>)&#x00a0;</m:mtext>
+       )&#x00a0;
        <xsl:apply-templates select="*[4]">
         <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
        </xsl:apply-templates>
@@ -685,9 +702,9 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       <m:mtext>(</m:mtext>
+       (
        <xsl:apply-templates select="*[5]"/>
-       <m:mtext>)&#x00a0;</m:mtext>
+       )&#x00a0;
        <xsl:apply-templates select="*[6]">
         <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
        </xsl:apply-templates>
@@ -723,7 +740,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       <m:mtext>*</m:mtext>
+       *
        <xsl:apply-templates select="*[4]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -731,7 +748,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       <m:mtext>*</m:mtext>
+       *
        <xsl:apply-templates select="*[5]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -757,16 +774,16 @@
        </xsl:call-template>
        <FONT color="red">Let&#x00a0;</FONT>
        <xsl:apply-templates mode="inline" select="*[3]"/>
-       <m:mtext>:</m:mtext>
+       :
        <xsl:apply-templates mode="inline" select="*[4]"/>
        <FONT color="red">&#x00a0;such that</FONT>
        <br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       <m:mtext>(</m:mtext>
+       (
        <xsl:apply-templates mode="inline" select="*[5]"/>
-       <m:mtext>)</m:mtext>
+       )
        <xsl:apply-templates select="*[6]">
         <xsl:with-param name="current_indent" select="$current_indent +7"/>
        </xsl:apply-templates>
@@ -799,7 +816,7 @@
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">
         <xsl:with-param name="current_indent" 
-           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+           select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
        </xsl:apply-templates><br/>
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
@@ -821,7 +838,9 @@
   <xsl:when test="boolean(@definitionURL)">
    <a>
    <xsl:attribute name="href">
-    <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
+    <xsl:call-template name="makeURL">
+     <xsl:with-param name="url" select="@definitionURL"/>
+    </xsl:call-template>
    </xsl:attribute>
    <xsl:apply-templates/>
    </a>
@@ -1003,10 +1022,10 @@ PROOF:
          <xsl:text>| </xsl:text>
          </xsl:otherwise>
          </xsl:choose>
-         <xsl:value-of select="./@name"/> 
+         <xsl:value-of select="./@name"/>
          <xsl:text>: </xsl:text>
          <xsl:apply-templates select="./*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+          <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
          </xsl:apply-templates>
       </xsl:for-each>
      </xsl:for-each>