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
---
 parsing/g_natsyntax.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 448c8dc2ca..8b8761cb18 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -32,11 +32,12 @@ open Names
 
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than (of_string "5000") n & Options.is_verbose () then begin
-	warning ("You may experience stack overflow and segmentation fault\
-                  \nwhile parsing numbers in nat greater than 5000");
-	flush_all ()
-      end;
+      if less_than (of_string "5000") n then
+	Options.if_warn msg_warning 
+	  (strbrk "Stack overflow or segmentation fault happens when " ++
+	   strbrk "working with large numbers in nat (observed threshold " ++
+	   strbrk "may vary from 5000 to 70000 depending on your system " ++
+	   strbrk "limits and on the command executed).");
       let ref_O = RRef (dloc, glob_O) in
       let ref_S = RRef (dloc, glob_S) in
       let rec mk_nat acc n =
-- 
cgit v1.2.3