]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
maction layout added to notation
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index b92b38656dd3704e58ee97342b6f1f94fbe150dc..a994c9fd166b83feb063e6e27a4cca1eed38ebaa 100644 (file)
@@ -212,7 +212,10 @@ and pp_layout = function
   | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
   | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
   | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
-  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3)
+  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1)
+  (pp_term t2) (pp_term t3)
+  | Ast.Maction l -> sprintf "\\MACTION (%s)" 
+     (String.concat "," (List.map pp_term l))
   | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Ast.Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
@@ -227,6 +230,10 @@ and pp_layout = function
       sprintf "\\MSTYLE %s [%s]" 
         (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
         (String.concat " " (List.map pp_term terms))
+  | Ast.Mpadded (l,terms) -> 
+      sprintf "\\MSTYLE %s [%s]" 
+        (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
+        (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | Ast.List0 (t, sep_opt) ->