This adds two option tables 'Printing Record' and 'Printing Constructor'

that forces a given type to always be printed as a record, or with a
constructor, regardless of the setting of 'Printing Records'.

And this is that patch that controls printing by type.

(patch from Tom Prince)

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

7 files changed, 106 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 909151f3c..98a8c78d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,8 @@ Specification language and notations
 - Added support for recursive notations with binders (allows for instance
   to write "exists x y z, P").
 - Structure/Record printing can be disable by "Unset Printing Records".
+  In addition, it can be controlled on type by type basis using
+  "Add Printing Record" or "Add Printing Constructor".
 
 Tactics
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 182a50959..3429bafab 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -200,10 +200,19 @@ Definition b := {| x := 5; y := 3 |}.
 Definition c := {| y := 3; x := 5 |}.
 \end{coq_example}
 
-This syntax can be disabled for printing by
+This syntax can be disabled globally for printing by
 \begin{quote}
 {\tt Unset Printing Records.}
 \end{quote}
+For a given type, one can override this using either
+\begin{quote}
+{\tt Add Printing Record {\ident}.}
+\end{quote}
+to get record syntax or
+\begin{quote}
+{\tt Add Printing Constructor {\ident}.}
+\end{quote}
+to get constructor syntax.
 
 This syntax can also be used for pattern matching.
 
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 623b334e0..b9e141455 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -14,8 +14,10 @@ let commands = [
    "Add LoadPath";
    "Add ML Path";
    "Add Morphism";
+   "Add Printing Constructor";
    "Add Printing If";
    "Add Printing Let";
+   "Add Printing Record";
    "Add Rec LoadPath";
    "Add Rec ML Path";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
@@ -92,8 +94,10 @@ let commands = [
    "Record";
    "Remark";
    "Remove LoadPath";
+   "Remove Printing Constructor";
    "Remove Printing If";
    "Remove Printing Let";
+   "Remove Printing Record";
    "Require";
    "Require Export";
    "Require Import";
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f23f9750c..fa92f9221 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -74,6 +74,49 @@ let without_symbols f = Flags.with_option print_no_symbol f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 
 (**********************************************************************)
+(* Control printing of records *)
+
+let is_record indsp =
+  try
+    let _ = Recordops.lookup_structure indsp in
+    true
+  with Not_found -> false
+
+let encode_record r =
+  let indsp = global_inductive r in
+  if not (is_record indsp) then
+    user_err_loc (loc_of_reference r,"encode_record",
+    str "This type is not a structure type.");
+  indsp
+
+module PrintingRecordRecord =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Record"
+    let title = "Types leading to pretty-printing using record notation: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using record notation"
+      else " are not printed using record notation")
+  end)
+
+module PrintingRecordConstructor =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Constructor"
+    let title = "Types leading to pretty-printing using constructor form: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using constructor form"
+      else " are not printed using constructor form")
+  end)
+
+module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord)
+module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
+
+(**********************************************************************)
 (* Various externalisation functions *)
 
 let insert_delimiters e = function
@@ -299,7 +342,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       let p =
 	try
-	  if !Flags.raw_print then raise Exit;
+          if !Flags.raw_print then raise Exit;
 	  let projs = Recordops.lookup_projections (fst cstrsp) in
 	  let rec ip projs args acc =
 	    match projs with
@@ -550,9 +593,15 @@ let rec extern inctx scopes vars r =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     begin
 	       try
-		 if !Flags.raw_print or not !Flags.record_print then raise Exit;
+                 if !Flags.raw_print then raise Exit;
 		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
 		 let struc = Recordops.lookup_structure (fst cstrsp) in
+                 if PrintingRecord.active (fst cstrsp) then
+                   ()
+                 else if PrintingConstructor.active (fst cstrsp) then
+                   raise Exit
+                 else if not !Flags.record_print then
+                   raise Exit;
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
 		 let rec cut args n =
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
new file mode 100644
index 000000000..36d643a44
--- /dev/null
+++ b/test-suite/output/Record.out
@@ -0,0 +1,16 @@
+{| field := 5 |}
+     : test
+{| field := 5 |}
+     : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
+build 5
+     : test
+build 5
+     : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
new file mode 100644
index 000000000..6aa3df983
--- /dev/null
+++ b/test-suite/output/Record.v
@@ -0,0 +1,21 @@
+Record test := build { field : nat }.
+Record test_r := build_r { field_r : nat }.
+Record test_c := build_c { field_c : nat }.
+
+Add Printing Constructor test_c.
+Add Printing Record test_r.
+
+Set Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
+
+Check build_r 5.
+Check build_c 5.
+
+Unset Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
+Check build_r 5.
+Check build_c 5.
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index bc0e18e57..8630fb3a9 100644
--- a/tools/coq-syntax.el
+++ b/tools/coq-syntax.el
@@ -417,8 +417,10 @@
      ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
      ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism")
      ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
+     ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor")
      ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
      ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let")
+     ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record")
      ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath")
      ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path")
      ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")