diff options
| -rw-r--r-- | interp/constrextern.ml | 15 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 | ||||
| -rw-r--r-- | test-suite/output/primitive_tokens.out | 29 | ||||
| -rw-r--r-- | test-suite/output/primitive_tokens.v | 15 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
5 files changed, 62 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4fb7861ca6..3cabf52197 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -64,7 +64,7 @@ let print_parentheses = Notation_ops.print_parentheses (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes -(* This suppresses printing of primitive tokens (e.g. numeral) and notations *) +(* This suppresses printing of notations *) let print_no_symbol = ref false (* This tells to skip types if a variable has this type by default *) @@ -74,6 +74,9 @@ let print_use_implicit_types = ~key:["Printing";"Use";"Implicit";"Types"] ~value:true +(* Print primitive tokens, like strings *) +let print_raw_literal = ref false + (**********************************************************************) let hole = CAst.make @@ CHole (None, IntroAnonymous, None) @@ -434,7 +437,7 @@ let extern_record_pattern cstrsp args = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try - if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match; let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -853,6 +856,7 @@ let same_binder_type ty nal c = (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = + if !print_raw_literal then raise No_match; let (n,key) = uninterp_prim_token r scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -1261,11 +1265,12 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.raw_print then raise No_match; try extern_possible_prim_token scopes t with No_match -> - let t = flatten_application t in - extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t)) + if !print_no_symbol then raise No_match; + let t = flatten_application t in + extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t)) and extern_notation inctx (custom,scopes as allscopes) vars t rules = match rules with diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 298b52f0be..bb49c8697d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,7 @@ val print_parentheses : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref +val print_raw_literal : bool ref (** Customization of the global_reference printer *) val set_extern_reference : diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out new file mode 100644 index 0000000000..cbed08c0ca --- /dev/null +++ b/test-suite/output/primitive_tokens.out @@ -0,0 +1,29 @@ +"foo" + : string +1234 + : nat +String (Ascii.Ascii false true true false false true true false) + (String (Ascii.Ascii true true true true false true true false) + (String (Ascii.Ascii true true true true false true true false) + EmptyString)) + : string +S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S (S (S (S (S (S ...))))))))))))))))))))))) + : nat diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v new file mode 100644 index 0000000000..fe31107744 --- /dev/null +++ b/test-suite/output/primitive_tokens.v @@ -0,0 +1,15 @@ +Require Import String. + +Open Scope string_scope. + +Unset Printing Notations. + +Check "foo". +Check 1234. +Check 1 + 2. + +Unset Printing Primitive Tokens. + +Check "foo". +Check 1234. +Check 1 + 2. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 38ca836b32..e8d84a67a3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1568,6 +1568,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Raw";"Literals"]; + optread = (fun () -> !Constrextern.print_raw_literal); + optwrite = (fun b -> Constrextern.print_raw_literal := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } |