From f7a82d5f7edcce7ef70b99a10b92d8dcd5cfea70 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 24 Feb 2007 15:22:07 +0000
Subject: Une passe sur les warnings (ajout Options.warn déclenchée par
 compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles +
 messages divers).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 5 +++--
 toplevel/himsg.ml   | 2 --
 toplevel/vernac.ml  | 1 +
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d9c91808f7..739a7b47f7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -144,8 +144,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
         let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
         definition_message ident;
         if Pfedit.refining () then 
-          msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
-          str" is not visible from current goals");
+          Options.if_verbose msg_warning 
+	    (str"Local definition " ++ pr_id ident ++ 
+             str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
         declare_global_definition ident ce' local in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3560bea4ff..305685cc7b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -29,8 +29,6 @@ open Printer
 open Rawterm
 open Evd
 
-let quote s = h 0 (str "\"" ++ s ++ str "\"")
-
 let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e c = quote (pr_lconstr_env e c)
 let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4090748b3b..eec73e3900 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -174,6 +174,7 @@ and vernac interpfun input =
   vernac_com interpfun (parse_phrase input)
 
 and read_vernac_file verbosely s =
+  Options.make_warn verbosely;
   let interpfun =
     if verbosely then 
       Vernacentries.interp
-- 
cgit v1.2.3