[gramlib] Remove unused function `gram_reinit`.

5 files changed, 42 insertions, 33 deletions

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 6a5c16fcc6..c35c4bd18e 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -103,14 +103,16 @@ let insert_tree ~warning entry_name gsymbols action tree =
           Node {node = s; son = son; brother = bro} ->
             Node {node = s; son = son; brother = insert [] bro}
         | LocAct (old_action, action_list) ->
-            if warning then
-              begin
-                eprintf "<W> Grammar extension: ";
-                if entry_name <> "" then eprintf "in [%s], " entry_name;
-                eprintf "some rule has been masked\n";
-                flush stderr
-              end;
-            LocAct (action, old_action :: action_list)
+          begin match warning with
+            | None -> ()
+            | Some warn_fn ->
+              let msg =
+                "<W> Grammar extension: " ^
+                (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^
+                "some rule has been masked" in
+              warn_fn msg
+          end;
+          LocAct (action, old_action :: action_list)
         | DeadEnd -> LocAct (action, [])
   and insert_in_tree s sl tree =
     match try_insert s sl tree with
@@ -196,17 +198,23 @@ let change_lev ~warning lev n lname assoc =
     match assoc with
       None -> lev.assoc
     | Some a ->
-        if a <> lev.assoc && warning then
-          begin
-            eprintf "<W> Changing associativity of level \"%s\"\n" n;
-            flush stderr
-          end;
+      if a <> lev.assoc then
+        begin
+          match warning with
+          | None -> ()
+          | Some warn_fn ->
+            warn_fn ("<W> Changing associativity of level \""^n^"\"")
+        end;
         a
   in
   begin match lname with
     Some n ->
-      if lname <> lev.lname && warning then
-        begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end
+      if lname <> lev.lname then
+        begin match warning with
+          | None -> ()
+          | Some warn_fn ->
+            warn_fn ("<W> Level label \""^n^"\" ignored")
+        end;
   | None -> ()
   end;
   {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index a9c20d012b..ecb95ec61b 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -53,13 +53,13 @@ type position =
   | Like of string
   | Level of string
 
-val levels_of_rules : warning:bool ->
+val levels_of_rules : warning:(string -> unit) option ->
   'te g_entry -> position option ->
     (string option * g_assoc option * ('te g_symbol list * g_action) list)
       list ->
     'te g_level list
 
-val srules : warning:bool -> ('te g_symbol list * g_action) list -> 'te g_symbol
+val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol
 val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool
 
 val delete_rule_in_level_list :
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 520170962d..285c14ec62 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -841,8 +841,6 @@ let clear_entry e =
     Dlevels _ -> e.edesc <- Dlevels []
   | Dparser _ -> ()
 
-let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer
-
 (* Functorial interface *)
 
 module type GLexerType = sig type te val lexer : te Plexing.lexer end
@@ -881,7 +879,7 @@ module type S =
     val s_self : ('self, 'self) ty_symbol
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : warning:bool -> 'a ty_production list -> ('self, 'a) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
@@ -889,10 +887,9 @@ module type S =
     val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
-        val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val safe_extend : warning:bool ->
+    val safe_extend : warning:(string -> unit) option ->
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
@@ -953,7 +950,6 @@ module GMake (L : GLexerType) =
       Obj.magic p
     module Unsafe =
       struct
-        let gram_reinit = gram_reinit gram
         let clear_entry = clear_entry
       end
     let safe_extend ~warning e pos
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 0748f5a65d..0c585a7c0d 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -53,7 +53,7 @@ module type S =
     val s_self : ('self, 'self) ty_symbol
     val s_next : ('self, 'self) ty_symbol
     val s_token : Plexing.pattern -> ('self, string) ty_symbol
-    val s_rules : warning:bool -> 'a ty_production list -> ('self, 'a) ty_symbol
+    val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
     val r_stop : ('self, 'r, 'r) ty_rule
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
@@ -62,10 +62,9 @@ module type S =
 
     module Unsafe :
       sig
-        val gram_reinit : te Plexing.lexer -> unit
         val clear_entry : 'a Entry.e -> unit
       end
-    val safe_extend : warning:bool ->
+    val safe_extend : warning:(string -> unit) option ->
       'a Entry.e -> Gramext.position option ->
         (string option * Gramext.g_assoc option * 'a ty_production list)
           list ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index ddad5aed61..816a02a6aa 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -193,7 +193,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol
 | Anext -> G.s_next
 | Aentry e -> G.s_nterm e
 | Aentryl (e, n) -> G.s_nterml e n
-| Arules rs -> G.s_rules ~warning:true (List.map symbol_of_rules rs)
+| Arules rs ->
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
 
 and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function
 | Stop -> Casted (G.r_stop, fun act loc -> act (!@loc))
@@ -261,7 +263,8 @@ let grammar_delete e reinit (pos,rls) =
     | Some (Gramext.Level n) -> n
     | _ -> assert false
     in
-    (G.safe_extend ~warning:true e) (Some ext) [Some lev,Some a,[]]
+    let warning msg = Feedback.msg_warning Pp.(str msg) in
+    (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
   | None -> ()
 
 (** Extension *)
@@ -270,14 +273,14 @@ let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e reinit ext in
   let pos, ext = fix_extend_statement ext in
-  let redo () = G.safe_extend ~warning:false e pos ext in
+  let redo () = G.safe_extend ~warning:None e pos ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e reinit ext =
   camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
   let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
-  G.safe_extend ~warning:false e pos ext
+  G.safe_extend ~warning:None e pos ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -325,14 +328,16 @@ let eoi_entry en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
   let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in
   let act = fun _ x loc -> x in
-  Gram.safe_extend ~warning:true e None (make_rule [G.production (symbs, act)]);
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
   e
 
 let map_entry f en =
   let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
   let symbs = G.r_next G.r_stop (G.s_nterm en) in
   let act = fun x loc -> f x in
-  Gram.safe_extend ~warning:true e None (make_rule [G.production (symbs, act)]);
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -462,7 +467,8 @@ let epsilon_value f e =
   let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
   let ext = [None, None, [r]] in
   let entry = Gram.entry_create "epsilon" in
-  let () = G.safe_extend ~warning:true entry None ext in
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  let () = G.safe_extend ~warning:(Some warning) entry None ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)