+/* The global print options set by the user. In general this should
+ not be directly accessed, except by set/show commands. Ordinary
+ code should call get_user_print_options instead. */
+extern struct value_print_options user_print_options;
+
+/* Initialize *OPTS to be a copy of the user print options. */
+extern void get_user_print_options (struct value_print_options *opts);
+
+/* Initialize *OPTS to be a copy of the user print options, but with
+ pretty-printing disabled. */
+extern void get_raw_print_options (struct value_print_options *opts);
+
+/* Initialize *OPTS to be a copy of the user print options, but using
+ FORMAT as the formatting option. */
+extern void get_formatted_print_options (struct value_print_options *opts,
+ char format);
+
+extern int get_array_bounds (struct type *type, LONGEST *low_bound,
+ LONGEST *high_bound);
+
+extern void maybe_print_array_index (struct type *index_type, LONGEST index,
+ struct ui_file *stream,
+ const struct value_print_options *options);
+
+extern void val_print_array_elements (struct type *, const gdb_byte *,
+ CORE_ADDR, struct ui_file *, int,
+ const struct value *,
+ const struct value_print_options *,
+ unsigned int);
+
+extern void val_print_type_code_int (struct type *, const gdb_byte *,