aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-02-22 02:31:16 +0100
committerEmilio Jesus Gallego Arias2017-04-12 16:49:46 +0200
commit55bddb4bf35fa68318aa57a5fa8a113d1fe51159 (patch)
treeba6820b5c2c47bfce0f13ccd194c82f7e017b2bd /interp/constrextern.ml
parent46856a80958f1aaa3242b6d37f018df9528e5e5f (diff)
[flags] Documentation and a minor tweak.
Mostly documentation and making a couple of local flags, local.
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml16
1 files changed, 15 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 925e9517c7..5bf49b7334 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,6 +85,20 @@ let without_specific_symbols l f =
(**********************************************************************)
(* Control printing of records *)
+(* Set Record Printing flag *)
+let record_print = ref true
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "record printing";
+ optkey = ["Printing";"Records"];
+ optread = (fun () -> !record_print);
+ optwrite = (fun b -> record_print := b) }
+
+
let is_record indsp =
try
let _ = Recordops.lookup_structure indsp in
@@ -658,7 +672,7 @@ let rec extern inctx scopes vars r =
()
else if PrintingConstructor.active (fst cstrsp) then
raise Exit
- else if not !Flags.record_print then
+ else if not !record_print then
raise Exit;
let projs = struc.Recordops.s_PROJ in
let locals = struc.Recordops.s_PROJKIND in