]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/boxPp.ml
parameter sintax added to axiom statement
[helm.git] / helm / software / components / content_pres / boxPp.ml
index bdd97a5e64aa5c3dbe6d275ab1ea0451ef3de5e3..0d58d97643a17aa147d117d006ed4cc8cec212d5 100644 (file)
@@ -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 _ ->