# HG changeset patch
# User wenzelm
# Date 1083845827 -7200
# Node ID 2d6350d7b9b714c12c1c7d6f7560c170442a7579
# Parent  71590b7733b70a5d05e930ad0b672b2e02738957
show_structs option;

diff -r 71590b7733b7 -r 2d6350d7b9b7 NEWS
--- a/NEWS	Thu May 06 14:14:18 2004 +0200
+++ b/NEWS	Thu May 06 14:17:07 2004 +0200
@@ -15,33 +15,34 @@
 identifier.  If all fails, consider to fall back on 'consts' and
 'defs' separately.
 
-* Pure: 'advanced' translation functions (parse_translation etc.) may
-depend on the signature of the theory context being presently used for
-parsing/printing, see also isar-ref manual.
-
-
 * Pure: improved indexed syntax and implicit structures.  First of
 all, indexed syntax provides a notational device for subscripted
 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
 expressions.  Secondly, in a local context with structure
 declarations, number indexes \<^sub>n or the empty index (default
-number 1) refer to a certain fixed variable implicitly.  Typical
+number 1) refer to a certain fixed variable implicitly; option
+show_structs controls printing of implicit structures.  Typical
 applications of these concepts involve record types and locales.
 
+* Pure: 'advanced' translation functions (parse_translation etc.) may
+depend on the signature of the theory context being presently used for
+parsing/printing, see also isar-ref manual.
+
 * Pure: tuned internal renaming of symbolic identifiers -- attach
 primes instead of base 26 numbers.
 
+
 *** HOL ***
 
-* Records:
-   Reimplementation of records to avoid performance problems for
-   type inference. Records are no longer composed of nested field types,
-   but of nested extension types. Therefore the record type only grows
-   linear in the number of extensions and not in the number of fields.
-   The top-level (users) view on records is preserved. 
-   Potential INCOMPATIBILITY only in strange cases, where the theory
-   depends on the old record representation. The type generated for
-   a record is called <record_name>_ext_type.    
+* HOL/record: reimplementation of records to avoid performance
+problems for type inference. Records are no longer composed of nested
+field types, but of nested extension types. Therefore the record type
+only grows linear in the number of extensions and not in the number of
+fields.  The top-level (users) view on records is preserved.
+Potential INCOMPATIBILITY only in strange cases, where the theory
+depends on the old record representation. The type generated for a
+record is called <record_name>_ext_type.
+
 
 *** HOLCF ***
 
diff -r 71590b7733b7 -r 2d6350d7b9b7 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu May 06 14:14:18 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex	Thu May 06 14:17:07 2004 +0200
@@ -516,6 +516,7 @@
 \begin{descr}
 \item[$show_types = bool$ and $show_sorts = bool$] control printing of
   explicit type and sort constraints.
+\item[$show_structs = bool$] controls printing of implicit structures.
 \item[$long_names = bool$] forces names of types and constants etc.\ to be
   printed in their fully qualified internal form.
 \item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
diff -r 71590b7733b7 -r 2d6350d7b9b7 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Thu May 06 14:14:18 2004 +0200
+++ b/src/Pure/Isar/isar_output.ML	Thu May 06 14:17:07 2004 +0200
@@ -262,6 +262,7 @@
 val _ = add_options
  [("show_types", Library.setmp Syntax.show_types o boolean),
   ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
+  ("show_structs", Library.setmp show_structs o boolean),
   ("long_names", Library.setmp NameSpace.long_names o boolean),
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   ("display", Library.setmp display o boolean),
diff -r 71590b7733b7 -r 2d6350d7b9b7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 06 14:14:18 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 06 14:17:07 2004 +0200
@@ -6,6 +6,8 @@
 Proof context information.
 *)
 
+val show_structs = ref false;
+
 signature PROOF_CONTEXT =
 sig
   type context
@@ -317,7 +319,8 @@
       | tr' (t as Free (x, T)) =
           let val i = Library.find_index_eq x structs + 1 in
             if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
-            else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
+            else if i = 1 andalso not (! show_structs) then
+              Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else t
           end
       | tr' a = a;
diff -r 71590b7733b7 -r 2d6350d7b9b7 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu May 06 14:14:18 2004 +0200
+++ b/src/Pure/proof_general.ML	Thu May 06 14:17:07 2004 +0200
@@ -279,6 +279,8 @@
       bool_option show_types)),
    ("show-sorts", ("Whether to show sorts in Isabelle.",
       bool_option show_sorts)),
+   ("show-structs", ("Whether to show implicit structures in Isabelle.",
+      bool_option show_structs)),
    ("show-consts", ("Whether to show types of consts in Isabelle goals.",
       bool_option show_consts)),
    ("long-names", ("Whether to show fully qualified names in Isabelle.",