X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2Fprint_grammar.ml;h=9951402820b473f2758d798145af2ec3a1c2a412;hb=ae88c7c1481ac9ddf5d55e2144b6db418a25fdd1;hp=893a3f53c9ef2a72e93f57d7ed9187e7901ad18a;hpb=e14fdca3a845ad0b88a34497f41472c3e7f8473b;p=helm.git

diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml
index 893a3f53c..995140282 100644
--- a/matita/components/grafite_parser/print_grammar.ml
+++ b/matita/components/grafite_parser/print_grammar.ml
@@ -84,10 +84,9 @@ and is_entry_dummy = function
 and is_symbol_dummy = function
   | Stoken ("DUMMY", _) -> true
   | Stoken _ -> false
-  | 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
@@ -105,7 +104,7 @@ let needs_brackets t =
   count_brothers t > 1
 
 let visit_description desc fmt self = 
-  let skip s = true in
+  let skip _s = true in
   let inline s = List.mem s [ "int" ] in
   
   let rec visit_entry e ?level todo is_son  =
@@ -140,7 +139,7 @@ let visit_description desc fmt self =
             (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
           todo is_son  
     
-  and visit_tree name t todo is_son  = 
+  and visit_tree name t todo _is_son  = 
     if List.for_all (List.for_all is_symbol_dummy) t then todo else (
     Format.fprintf fmt "@[<v>";
     (match name with 
@@ -170,15 +169,6 @@ let visit_description desc fmt self =
     
   and visit_symbol s todo is_son  =
     match s with
-    | Smeta (name, sl, _) -> 
-        Format.fprintf fmt "%s " name;
-        List.fold_left (
-          fun acc s -> 
-            let todo = visit_symbol s acc is_son  in
-            if is_son then
-              Format.fprintf fmt "@ ";
-            todo) 
-        todo sl
     | Snterm entry -> visit_entry entry todo is_son  
     | Snterml (entry,level) -> visit_entry entry ~level todo is_son 
     | Slist0 symbol -> 
@@ -186,7 +176,7 @@ let visit_description desc fmt self =
         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> ";
@@ -200,7 +190,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
@@ -256,7 +246,7 @@ let rec visit_entries fmt todo pped =
           ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
           (List.sort 
             (fun e1 e2 -> 
-              Pervasives.compare (name_of_entry e1) (name_of_entry e2))
+              Stdlib.compare (name_of_entry e1) (name_of_entry e2))
             todo),
         pped
       in
@@ -264,8 +254,8 @@ let rec visit_entries fmt todo pped =
       visit_entries fmt todo pped
 ;;
 
-let ebnf_of_term () =
-  let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
+let ebnf_of_term status =
+  let g_entry = Grammar.Entry.obj (CicNotationParser.term status) in
   let buff = Buffer.create 100 in
   let fmt = Format.formatter_of_buffer buff in
   visit_entries fmt [g_entry] [];