X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2Fprint_grammar.ml;h=47f42356f4854e8f2f08242a9f8d7ec7fb4f3115;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hp=d2eb817adce30991523ee61908d9180cf51764b3;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index d2eb817ad..47f42356f 100644
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -87,7 +87,7 @@ and is_symbol_dummy = function
   | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
   | Snterm e | Snterml (e, _) -> is_entry_dummy e
   | Slist1 x | Slist0 x -> is_symbol_dummy x
-  | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+  | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
   | Sopt x -> is_symbol_dummy x
   | Sself | Snext -> false
   | Stree t -> is_tree_dummy t
@@ -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,13 +180,13 @@ 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
         Format.fprintf fmt "@]} @ ";
         todo
-    | Slist0sep (symbol,sep) ->
+    | Slist0sep (symbol,sep,false) ->
         Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "{@[<hov2> ";
@@ -198,7 +200,7 @@ let visit_description desc fmt self =
         let todo = visit_symbol symbol todo is_son in
         Format.fprintf fmt "@]}+ @ ";
         todo 
-    | Slist1sep (symbol,sep) ->
+    | Slist1sep (symbol,sep,false) ->
         let todo = visit_symbol symbol todo is_son  in
         Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol sep todo is_son in
@@ -263,7 +265,7 @@ let rec visit_entries fmt todo pped =
 ;;
 
 let ebnf_of_term () =
-  let g_entry = Grammar.Entry.obj CicNotationParser.term in
+  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
   let buff = Buffer.create 100 in
   let fmt = Format.formatter_of_buffer buff in
   visit_entries fmt [g_entry] [];