From: Stefano Zacchiroli <zack@upsilon.cc>
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/?p=helm.git;a=commitdiff_plain;h=1de1589cd58fa18f1699c7fe1780adcd5da47a64

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 "@[<hov2>";
           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 "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting+1) in
-        Format.fprintf fmt "}@] @ ";
+        Format.fprintf fmt "@]} @ ";
         todo
     | Slist0sep (symbol,sep) ->
-        Format.fprintf fmt "@[<hov2>[ ";
+        Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting + 1) in
-        Format.fprintf fmt "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         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 "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         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 " @[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         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 "@[<hov2>[ ";
+        Format.fprintf fmt "[@[<hov2> ";
         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 "@[<hov2>( ";
+            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