X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fprint_grammar.ml;h=51f7d866895adef204c8225bb04c0c00077658a0;hb=118769957a508c21b72bd7b9d2dbf64f654fe21c;hp=99ab9ad62e658767ecf7e155c121f0891fcf92e8;hpb=3059c9a2b5e06003080c6294bd5ea6687ba80ca1;p=helm.git

diff --git a/helm/ocaml/cic_notation/print_grammar.ml b/helm/ocaml/cic_notation/print_grammar.ml
index 99ab9ad62..51f7d8668 100644
--- a/helm/ocaml/cic_notation/print_grammar.ml
+++ b/helm/ocaml/cic_notation/print_grammar.ml
@@ -26,7 +26,9 @@
 open Gramext 
 
 let tex_of_unicode s =
-  let no_expansion = ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}"] in
+  let no_expansion = 
+    ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}";">";"<"] 
+  in
   let contractions = 
     ("\\Longrightarrow","=>") :: []
   in
@@ -35,7 +37,7 @@ let tex_of_unicode s =
     let s = Utf8Macro.tex_of_unicode s in
     try List.assoc s contractions with Not_found -> s
 
-let visit_description desc fmt = 
+let visit_description desc fmt self = 
   let skip s = List.mem s [ ] in
   let inline s = List.mem s [ "int" ] in
   
@@ -93,7 +95,7 @@ let visit_description desc fmt =
     let todo =
       if is_tree_printable son then
         begin
-          let need_b = needs_brackets son in
+          let need_b = is_son && needs_brackets son in
           if not is_son then
             Format.fprintf fmt "@[<hov2>";
           if need_b then
@@ -160,12 +162,12 @@ let visit_description desc fmt =
         let todo = visit_symbol symbol todo is_son (nesting + 1) in
         Format.fprintf fmt "]@] @ ";
         todo
-    | Sself -> Format.fprintf fmt "self "; todo
+    | Sself -> Format.fprintf fmt "%s " self; todo
     | Snext -> Format.fprintf fmt "next "; todo
     | Stoken pattern -> 
         let constructor, keyword = pattern in
         if keyword = "" then
-          Format.fprintf fmt "'%s' " constructor
+          Format.fprintf fmt "`%s' " constructor
         else
           Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
         todo
@@ -195,10 +197,16 @@ and clean_tree = function
   | x -> x
   
 and clean_node = function
-  | {node=node;son=son;brother=brother} when 
-      is_symbol_dummy node && 
-      is_tree_dummy son && 
-      is_tree_dummy brother -> DeadEnd
+  | {node=node;son=son;brother=brother} ->
+      let bn = is_symbol_dummy node in
+      let bs = is_tree_dummy son in
+      let bb = is_tree_dummy brother in
+      let son = if bs then DeadEnd else son in
+      let brother = if bb then DeadEnd else brother in
+      if bb && bs && bn then
+        DeadEnd
+      else 
+        Node {node=node;son=son;brother=brother}
   | x -> Node x
 
 and is_level_dummy = function
@@ -241,7 +249,7 @@ let rec visit_entries todo pped =
             let { ename = ename; edesc = desc } = hd in 
             Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
             let desc = clean_dummy_desc desc in 
-            let todo = visit_description desc fmt @ todo in
+            let todo = visit_description desc fmt ename @ todo in
             Format.fprintf fmt "@]";
             Format.pp_print_newline fmt ();
             Format.pp_print_newline fmt ();
@@ -268,6 +276,5 @@ let rec visit_entries todo pped =
 ;;
 
 let _ =
-(*  let g_entry = Grammar.Entry.obj CicNotationParser.term in*)
   let g_entry = Grammar.Entry.obj GrafiteParser.statement in
   visit_entries [g_entry] []