--- 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 ***
--- 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.
--- 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),
--- 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;
--- 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.",