X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2Fprint_grammar.ml;h=893a3f53c9ef2a72e93f57d7ed9187e7901ad18a;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=bb2a68b326ae39bf631c095dcb58d1fadce6f11e;hpb=01001c883a8151edba81cd03a6f254d24a81c867;p=helm.git

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index bb2a68b32..893a3f53c 100644
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -108,17 +108,19 @@ let visit_description desc fmt self =
   let skip s = true in
   let inline s = List.mem s [ "int" ] in
   
-  let rec visit_entry e todo is_son  =
+  let rec visit_entry e ?level todo is_son  =
     let { ename = ename; edesc = desc } = e in 
     if inline ename then 
       visit_desc desc todo is_son 
     else
       begin
-        Format.fprintf fmt "%s " ename;
-        if skip ename then
-          todo
-        else
-          todo @ [e]
+       (match level with
+       | None -> Format.fprintf fmt "%s " ename;
+       | Some _ -> Format.fprintf fmt "%s " ename;);
+          if skip ename then
+            todo
+          else
+            todo @ [e]
       end
       
   and visit_desc d todo is_son  =
@@ -178,7 +180,7 @@ let visit_description desc fmt self =
             todo) 
         todo sl
     | Snterm entry -> visit_entry entry todo is_son  
-    | Snterml (entry,_) -> visit_entry entry todo is_son 
+    | Snterml (entry,level) -> visit_entry entry ~level todo is_son 
     | Slist0 symbol -> 
         Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in