From: Stefano Zacchiroli Date: Tue, 15 Nov 2005 13:18:32 +0000 (+0000) Subject: better output formatting X-Git-Tag: V_0_7_2_3~77 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1de1589cd58fa18f1699c7fe1780adcd5da47a64;p=helm.git better output formatting --- diff --git a/helm/ocaml/cic_notation/print_grammar.ml b/helm/ocaml/cic_notation/print_grammar.ml index 51f7d8668..d7d6f3c96 100644 --- a/helm/ocaml/cic_notation/print_grammar.ml +++ b/helm/ocaml/cic_notation/print_grammar.ml @@ -26,17 +26,19 @@ open Gramext let tex_of_unicode s = - let no_expansion = - ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}";">";"<"] - in - let contractions = - ("\\Longrightarrow","=>") :: [] - in - if List.exists ((=) s) no_expansion then s - else + let contractions = ("\\Longrightarrow","=>") :: [] in + if String.length s <= 1 then s + else (* probably an extended unicode symbol *) let s = Utf8Macro.tex_of_unicode s in try List.assoc s contractions with Not_found -> s +let needs_brackets t = + let rec count_brothers = function + | Node {brother = brother} -> 1 + count_brothers brother + | _ -> 0 + in + count_brothers t > 1 + let visit_description desc fmt self = let skip s = List.mem s [ ] in let inline s = List.mem s [ "int" ] in @@ -83,19 +85,12 @@ let visit_description desc fmt self = | Node _ -> true | _ -> false in - let needs_brackets t = - let rec count_brothers = function - | Node {brother = brother} -> 1 + count_brothers brother - | _ -> 0 - in - count_brothers t > 1 - in let { node = symbol; son = son ; brother = brother } = n in let todo = visit_symbol symbol todo is_son nesting in let todo = if is_tree_printable son then begin - let need_b = is_son && needs_brackets son in + let need_b = needs_brackets son in if not is_son then Format.fprintf fmt "@["; if need_b then @@ -132,35 +127,35 @@ let visit_description desc fmt self = | Snterm entry -> visit_entry entry todo is_son nesting | Snterml (entry,_) -> visit_entry entry todo is_son nesting | Slist0 symbol -> - Format.fprintf fmt "@[{ "; + Format.fprintf fmt "{@[ "; let todo = visit_symbol symbol todo is_son (nesting+1) in - Format.fprintf fmt "}@] @ "; + Format.fprintf fmt "@]} @ "; todo | Slist0sep (symbol,sep) -> - Format.fprintf fmt "@[[ "; + Format.fprintf fmt "[@[ "; let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "@[{ "; + Format.fprintf fmt "{@[ "; let todo = visit_symbol sep todo is_son (nesting + 2) in Format.fprintf fmt " "; let todo = visit_symbol symbol todo is_son (nesting + 2) in - Format.fprintf fmt "}@] @ ]@] @ "; + Format.fprintf fmt "@]} @]] @ "; todo | Slist1 symbol -> - Format.fprintf fmt "@[{ "; + Format.fprintf fmt "{@[ "; let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "}+@] @ "; + Format.fprintf fmt "@]}+ @ "; todo | Slist1sep (symbol,sep) -> let todo = visit_symbol symbol todo is_son nesting in - Format.fprintf fmt " @[{ "; + Format.fprintf fmt "{@[ "; let todo = visit_symbol sep todo is_son (nesting + 1) in let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "}@] @ "; + Format.fprintf fmt "@]} @ "; todo | Sopt symbol -> - Format.fprintf fmt "@[[ "; + Format.fprintf fmt "[@[ "; let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "]@] @ "; + Format.fprintf fmt "@]] @ "; todo | Sself -> Format.fprintf fmt "%s " self; todo | Snext -> Format.fprintf fmt "next "; todo @@ -171,7 +166,16 @@ let visit_description desc fmt self = else Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); todo - | Stree tree -> visit_tree tree todo is_son nesting + | Stree tree -> + if needs_brackets tree then + begin + Format.fprintf fmt "@[( "; + let todo = visit_tree tree todo is_son (nesting + 1) in + Format.fprintf fmt ")@] @ "; + todo + end + else + visit_tree tree todo is_son (nesting + 1) in visit_desc desc [] false 0 ;; @@ -206,8 +210,10 @@ and clean_node = function if bb && bs && bn then DeadEnd else - Node {node=node;son=son;brother=brother} - | x -> Node x + if bn then + Node {node=Sself;son=son;brother=brother} + else + Node {node=node;son=son;brother=brother} and is_level_dummy = function | {lsuffix=lsuffix;lprefix=lprefix} -> @@ -228,8 +234,7 @@ and is_symbol_dummy = function | Slist1 x | Slist0 x -> is_symbol_dummy x | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y | Sopt x -> is_symbol_dummy x - | Sself -> false - | Snext -> true + | Sself | Snext -> false | Stree t -> is_tree_dummy t and is_tree_dummy = function