diff options
| -rw-r--r-- | interp/constrextern.ml | 19 | ||||
| -rw-r--r-- | lib/options.ml | 12 | ||||
| -rw-r--r-- | lib/options.mli | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 10 |
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"); |