From b4a67321811bdc123636eaa0f117d5308cb7a07b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 3 Jun 2009 20:20:11 +0000
Subject: [PATCH] - 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 :)
---
 helm/software/components/content_pres/boxPp.ml  | 14 +++++++-------
 helm/software/matita/core_notation.moo          |  2 +-
 helm/software/matita/library/Makefile           |  5 +++++
 helm/software/matita/library/nat/permutation.ma |  9 ++++++---
 4 files changed, 19 insertions(+), 11 deletions(-)

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.
-- 
2.39.2