X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=29898eb13ace83196d7340d8f10ff653dc170cc6;hb=e053aaf3085a079c3125ed4666ba648a48fbb2af;hp=a0f9dc2f12a8fb7e61ca82756e8f3c463a3519de;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index a0f9dc2f1..29898eb13 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -211,6 +211,7 @@ 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.Sqrt t -> sprintf "\\SQRT %s" (pp_term t) | Ast.Root (arg, index) -> sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) @@ -221,6 +222,10 @@ and pp_layout = function (String.concat " " (List.map pp_term terms)) | Ast.Group terms -> sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) + | Ast.Mstyle (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) ->