From 8ae0762db0616e1ff177335c9fc73c816634fc89 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Feb 2021 16:20:08 +0100
Subject: [notation] option to fine tune printing of literals

---
 interp/constrextern.ml                 | 15 ++++++++++-----
 interp/constrextern.mli                |  1 +
 test-suite/output/primitive_tokens.out | 29 +++++++++++++++++++++++++++++
 test-suite/output/primitive_tokens.v   | 15 +++++++++++++++
 vernac/vernacentries.ml                |  7 +++++++
 5 files changed, 62 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/output/primitive_tokens.out
 create mode 100644 test-suite/output/primitive_tokens.v

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
@@ -1565,6 +1565,13 @@ let () =
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
+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;
-- 
cgit v1.2.3