Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalite de haut niveau de l'affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 31 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 14a5e43034..933fd33cab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1156,7 +1156,7 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope scopes vars pat =
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     let (sc,n) = Symbols.uninterp_cases_numeral pat in
     match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
     | None -> raise No_match
@@ -1165,7 +1165,7 @@ let rec extern_cases_pattern_in_scope scopes vars pat =
         insert_pat_delimiters (CPatNumeral (loc,n)) key
   with No_match ->
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol_pattern scopes vars pat
       (Symbols.uninterp_cases_pattern_notations pat)
   with No_match ->
@@ -1222,7 +1222,7 @@ let occur_name na aty =
     | Anonymous -> false
 
 let is_projection nargs = function
-  | Some r when !print_projections ->
+  | Some r when not !Options.raw_print & !print_projections ->
       (try 
 	let n = Recordops.find_projection_nparams r + 1 in
 	if n <= nargs then Some n else None
@@ -1260,6 +1260,7 @@ let explicitize loc inctx impl (cf,f) args =
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
         let visible =
+          !Options.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or 
 	  (is_significant_implicit a impl tail &
 	  (not (is_inferable_implicit inctx n imp) or
@@ -1285,7 +1286,7 @@ let explicitize loc inctx impl (cf,f) args =
 	if args = [] then f else CApp (loc, (None, f), args)
 
 let rec skip_coercion dest_ref (f,args as app) =
-  if !print_coercions or Options.do_translate () then app
+  if !Options.raw_print or !print_coercions or Options.do_translate () then app
   else
     try
       match dest_ref f with
@@ -1310,9 +1311,9 @@ let extern_app loc inctx impl (cf,f) args =
   if args = [] (* maybe caused by a hidden coercion *) then
     extern_global loc impl f
   else
-  if !print_implicits &
-    not !print_implicits_explicit_args &
-    List.exists is_status_implicit impl
+  if !Options.raw_print or 
+    (!print_implicits & not !print_implicits_explicit_args &
+     List.exists is_status_implicit impl)
   then 
     CAppExpl (loc, (is_projection (List.length args) cf, f), args)
   else
@@ -1332,13 +1333,13 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec extern inctx scopes vars r =
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_numeral (Rawterm.loc_of_rawconstr r)
       scopes (Symbols.uninterp_numeral r)
   with No_match ->
 
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r (Symbols.uninterp_notations r)
   with No_match -> match r with
   | RRef (loc,ref) ->
diff --git a/lib/options.ml b/lib/options.ml
index 80b4631233..afa419d679 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -10,6 +10,11 @@
 
 open Util
 
+let with_option o f x =
+  let old = !o in o:=true;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
 let boot = ref false
 
 let batch_mode = ref false
@@ -26,6 +31,8 @@ let xml_export = ref false
 
 let dont_load_proofs = ref false
 
+let raw_print = ref false
+
 let v7 =
   let transl = array_exists ((=) "-translate") Sys.argv in
   let v7 = array_exists ((=) "-v7") Sys.argv in
@@ -66,11 +73,6 @@ let silently f x =
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
-let with_option o f x =
-  let old = !o in o:=true;
-  try let r = f x in o := old; r
-  with e -> o := old; raise e
-
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
diff --git a/lib/options.mli b/lib/options.mli
index 41e8dea844..395efc649a 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -25,6 +25,8 @@ val xml_export : bool ref
 
 val dont_load_proofs : bool ref
 
+val raw_print : bool ref
+
 val v7 : bool ref
 val v7_only : bool ref
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 748901e29a..06ae24175c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -243,7 +243,9 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
   let eqnl = Array.to_list eqnv in
   let tag =
     try 
-      if PrintingLet.active (indsp,consnargsl) then
+      if !Options.raw_print then
+        st
+      else if PrintingLet.active (indsp,consnargsl) then
 	LetStyle
       else if PrintingIf.active (indsp,consnargsl) then 
 	IfStyle
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33b1952c7d..307e1026b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -736,12 +736,20 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "symbols printing";
+      optname  = "notations printing";
       optkey   = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
 let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "raw printing";
+      optkey   = (SecondaryTable ("Printing","All"));
+      optread  = (fun () -> !Options.raw_print);
+      optwrite = (fun b -> Options.raw_print := b) }
+
+let _ =
   declare_int_option
     { optsync=false;
       optkey=PrimaryTable("Undo");