From 1996440b67ed8e2cfa8490cfb07548ecea5962bd Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 11 Apr 2001 11:04:06 +0000
Subject: [PATCH] In natural language, non vengono piu' stampati glia argomenti
 delle applicazioni con sort divers da prop.

---
 helm/style/content_to_html.xsl | 30 +++++++++++++--
 helm/style/proofs.xsl          | 68 ++++++++++++++++++++++++++++++++--
 2 files changed, 90 insertions(+), 8 deletions(-)

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 75b7bcc3a..9708f3cd7 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -467,6 +467,9 @@
           <xsl:with-param name="current_indent" select="$current_indent + 2"/>
          </xsl:apply-templates>
          <xsl:text>&gt; </xsl:text>
+         <br/>
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
          <xsl:text>CASE </xsl:text>
          <xsl:apply-templates select="*[position()=3]">
           <xsl:with-param name="current_indent" select="$current_indent + 8"/>
@@ -475,7 +478,7 @@
          <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
          <br/>
          <xsl:call-template name="make_indent">
-            <xsl:with-param name="current_indent" select="$current_indent + 2"/>  
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
          </xsl:call-template> 
             <xsl:choose>
             <xsl:when test="position() = 1">
@@ -487,9 +490,28 @@
             </xsl:choose>
             <xsl:apply-templates select="."/>
             <FONT FACE="Symbol" SIZE="+0" mathcolor="green">&#222;</FONT>
-            <xsl:apply-templates select="following-sibling::*[position()= 1]">
-             <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
-            </xsl:apply-templates>
+            <xsl:variable name="body_size">
+             <xsl:apply-templates 
+              select="following-sibling::*[1]/*[1]" mode="charcount"/>
+            </xsl:variable>
+            <xsl:choose>
+             <xsl:when test="$body_size > $framewidth">
+              <br/>
+              <xsl:call-template name="make_indent">
+               <xsl:with-param name="current_indent" 
+                    select="$current_indent + 8"/>   
+              </xsl:call-template>
+	      <xsl:apply-templates 
+                   select="following-sibling::*[position()= 1]">
+              <xsl:with-param name="current_indent" 
+                   select="$current_indent + 8"/>      
+             </xsl:apply-templates>
+            </xsl:when>
+            <xsl:otherwise>
+             <xsl:apply-templates select="following-sibling::*[position()= 1]"
+                   mode="inline" />
+            </xsl:otherwise>
+           </xsl:choose>
          </xsl:for-each>
        </xsl:when>
        <xsl:otherwise>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index f82d77690..05cf06dd1 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -55,7 +55,6 @@
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
-    <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
    </m:apply>
   </xsl:when>
@@ -409,6 +408,29 @@
     </xsl:otherwise>
    </xsl:choose>
   </xsl:when>
+  <xsl:when test="name()='LAMBDA'">
+   <xsl:choose>
+     <xsl:when test="(name(target/*[1])='APPLY'  and
+      name(target/*[1]/*[1])='CONST' and
+      (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+       target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+       target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
+      and count(target/*[1]/*) = 8 
+      and name(target/*[1]/*[8])='REL'
+      and target/@binder = target/*[1]/*[8]/@binder )"> 
+      <m:apply>
+       <m:csymbol>rw_step</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
+       <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
+       <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
+       <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/>
+      </m:apply>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-templates mode="pure" select="."/>
+     </xsl:otherwise>
+    </xsl:choose>
+   </xsl:when>
   <xsl:otherwise>
    <xsl:apply-templates select="." mode="pure"/>
   </xsl:otherwise>
@@ -447,7 +469,17 @@
      </m:apply>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:apply-templates mode="pure" select="."/>
+     <xsl:choose>
+     <xsl:when test="@sort='Prop'">
+      <m:apply>
+       <m:csymbol>app</m:csymbol>
+       <xsl:apply-templates mode="erase" select="*[1]"/>
+      </m:apply>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-templates mode="pure" select="."/>
+     </xsl:otherwise>
+     </xsl:choose>
     </xsl:otherwise>
    </xsl:choose>
 </xsl:template>
@@ -464,13 +496,33 @@
       </xsl:for-each>
 </xsl:template>
 
+<xsl:template match="*" mode="erase">
+  <xsl:choose>
+   <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+    <xsl:apply-templates mode="pure" select="."/>
+   </xsl:when>
+   <xsl:otherwise>
+    <m:ci>.</m:ci>
+   </xsl:otherwise>
+   </xsl:choose>
+ <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
+</xsl:template>
+
 <xsl:template match="*" mode="previous">
  <xsl:choose>
   <xsl:when test="$naturalLanguage='yes' and(@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX'))">
    <m:ci>previous</m:ci>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-templates select="." mode="pure"/>
+   <xsl:choose>
+   <xsl:when test="@sort='Prop' or $naturalLanguage='no' ">
+    <xsl:apply-templates mode="pure" select="."/>
+   </xsl:when>
+   <xsl:otherwise>
+    <m:ci>.</m:ci>
+   </xsl:otherwise>
+   </xsl:choose>
+   <!-- <xsl:apply-templates select="." mode="pure"/> -->
   </xsl:otherwise>
  </xsl:choose>
  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
@@ -491,7 +543,15 @@
    </xsl:apply-templates>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-templates mode="pure" select="."/>
+   <xsl:choose>
+   <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+    <xsl:apply-templates mode="pure" select="."/>
+   </xsl:when>
+   <xsl:otherwise>
+    <m:ci>.</m:ci>
+   </xsl:otherwise>
+   </xsl:choose>
+   <!-- <xsl:apply-templates mode="pure" select="."/> -->
    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
     <xsl:with-param name="n" select="$n"/>
    </xsl:apply-templates>
-- 
2.39.2