From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 3 Jun 2009 20:20:11 +0000 (+0000)
Subject: - boxPp: added missing spaces
X-Git-Tag: make_still_working~3926
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b4a67321811bdc123636eaa0f117d5308cb7a07b;p=helm.git

- boxPp: added missing spaces
- core_notation: bug fix in the input notation for congruent: we added term 90 after \sub
- library/nat/permutation.ma: added input notation for transpose and fixed term precedence in its output notation
- library/Makefile: compilation of single files re-enabled.
The syntax for compiling file.ma is is "make file.mo" and "make file.mo.opt"

now nat/congruence.ma and nat/permutation.ma are fully reconstructed :)
---

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index bdd97a5e6..0d58d9764 100644
--- a/helm/software/components/content_pres/boxPp.ml
+++ b/helm/software/components/content_pres/boxPp.ml
@@ -210,11 +210,11 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup =
         let children' = List.map aux_mpres children in
         (fun size -> render_row size false children')
     | Pres.Mfrac (_, m, n) ->
-       aux_mpres (mrow [ text " \\frac "; parentesize m ; parentesize n])
-    | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; ])
+       aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ])
+    | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "])
     | Pres.Mroot (_, r, i) ->
         aux_mpres (mrow [
-          text " \\root "; parentesize i; text " \\of "; parentesize r ])
+          text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ])
     | Pres.Mstyle (_, m)
     | Pres.Merror (_, m)
     | Pres.Mpadded (_, m)
@@ -223,13 +223,13 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup =
     | Pres.Mfenced (_, children) -> aux_mpres (mrow children)
     | Pres.Maction (_, []) -> assert false
     | Pres.Msub (_, m, n) ->
-        aux_mpres (mrow [ parentesize m; text " \\sub "; parentesize n ])
+        aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ])
     | Pres.Msup (_, m, n) ->
-        aux_mpres (mrow [ parentesize m; text " \\sup "; parentesize n ])
+        aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ])
     | Pres.Munder (_, m, n) ->
-        aux_mpres (mrow [ parentesize m; text " \\below "; parentesize n ])
+        aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ])
     | Pres.Mover (_, m, n) ->
-        aux_mpres (mrow [ parentesize m; text " \\above "; parentesize n ])
+        aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ])
     | Pres.Msubsup _
     | Pres.Munderover _
     | Pres.Mtable _ ->
diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index 3d4ad9893..328274bb8 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -62,7 +62,7 @@ notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
   non associative with precedence 45
 for @{ 'eq $t $a $b }.
 
-notation > "hvbox(n break (≅ \sub p) m)"
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
   non associative with precedence 45
 for @{ 'congruent $n $m $p }.
 
diff --git a/helm/software/matita/library/Makefile b/helm/software/matita/library/Makefile
index 799841d70..33368a32d 100644
--- a/helm/software/matita/library/Makefile
+++ b/helm/software/matita/library/Makefile
@@ -12,3 +12,8 @@ depend:
 	../matitadep -dot
 depend.opt:
 	../matitadep.opt -dot
+
+%.mo: 
+	../matitac $*.ma
+%.mo.opt: 
+	../matitac.opt $*.ma
diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma
index e594b8220..bfa5112bc 100644
--- a/helm/software/matita/library/nat/permutation.ma
+++ b/helm/software/matita/library/nat/permutation.ma
@@ -72,10 +72,13 @@ match eqb n i with
       [ true \Rightarrow i
       | false \Rightarrow n]].
 
-notation < "(❲i↹j❳)n" with precedence 71 
+notation < "(❲i↹j❳) term 72 n" with precedence 71 
 for @{ 'transposition $i $j $n}.
 
-notation < "(❲i \atop j❳)n" with precedence 71 
+notation < "(❲i \atop j❳) term 72 n" with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71 
 for @{ 'transposition $i $j $n}.
 
 interpretation "natural transposition" 'transposition i j n = (transpose i j n).
@@ -747,4 +750,4 @@ intros 4.elim k
       ]
     ]
   ]
-qed.
\ No newline at end of file
+qed.