--- a/NEWS Fri May 17 20:41:45 2013 +0200
+++ b/NEWS Fri May 17 20:53:28 2013 +0200
@@ -12,6 +12,9 @@
INCOMPATIBILITY, need to use more official Isabelle means to access
quick_and_dirty, instead of historical poking into mutable reference.
+* Renamed command 'print_configs' to 'print_options'. Minor
+INCOMPATIBILITY.
+
* Sessions may be organized via 'chapter' specifications in the ROOT
file, which determines a two-level hierarchy of browser info. The old
tree-like organization via implicit sub-session relation, with its
--- a/etc/isar-keywords-ZF.el Fri May 17 20:41:45 2013 +0200
+++ b/etc/isar-keywords-ZF.el Fri May 17 20:53:28 2013 +0200
@@ -130,7 +130,6 @@
"print_classes"
"print_codesetup"
"print_commands"
- "print_configs"
"print_context"
"print_defn_rules"
"print_dependencies"
@@ -141,6 +140,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_options"
"print_rules"
"print_simpset"
"print_statement"
@@ -299,7 +299,6 @@
"print_classes"
"print_codesetup"
"print_commands"
- "print_configs"
"print_context"
"print_defn_rules"
"print_dependencies"
@@ -310,6 +309,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_options"
"print_rules"
"print_simpset"
"print_statement"
--- a/etc/isar-keywords.el Fri May 17 20:41:45 2013 +0200
+++ b/etc/isar-keywords.el Fri May 17 20:53:28 2013 +0200
@@ -184,7 +184,6 @@
"print_coercion_maps"
"print_coercions"
"print_commands"
- "print_configs"
"print_context"
"print_defn_rules"
"print_dependencies"
@@ -196,6 +195,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_options"
"print_orders"
"print_quotconsts"
"print_quotients"
@@ -408,7 +408,6 @@
"print_coercion_maps"
"print_coercions"
"print_commands"
- "print_configs"
"print_context"
"print_defn_rules"
"print_dependencies"
@@ -420,6 +419,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_options"
"print_orders"
"print_quotconsts"
"print_quotients"
--- a/src/Doc/IsarRef/Generic.thy Fri May 17 20:41:45 2013 +0200
+++ b/src/Doc/IsarRef/Generic.thy Fri May 17 20:53:28 2013 +0200
@@ -31,7 +31,7 @@
``global'', which may not be changed within a local context.
\begin{matharray}{rcll}
- @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@{rail "
@@ -40,7 +40,7 @@
\begin{description}
- \item @{command "print_configs"} prints the available configuration
+ \item @{command "print_options"} prints the available configuration
options, with names, types, and current values.
\item @{text "name = value"} as an attribute expression modifies the
--- a/src/Pure/Isar/attrib.ML Fri May 17 20:41:45 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Fri May 17 20:53:28 2013 +0200
@@ -46,7 +46,7 @@
(binding * (thm list * Args.src list) list) list ->
(binding * (thm list * Args.src list) list) list
val internal: (morphism -> attribute) -> src
- val print_configs: Proof.context -> unit
+ val print_options: Proof.context -> unit
val config_bool: Binding.binding ->
(Context.generic -> bool) -> bool Config.T * (theory -> theory)
val config_int: Binding.binding ->
@@ -444,7 +444,7 @@
fun merge data = Symtab.merge (K true) data;
);
-fun print_configs ctxt =
+fun print_options ctxt =
let
val thy = Proof_Context.theory_of ctxt;
fun prt (name, config) =
--- a/src/Pure/Isar/isar_syn.ML Fri May 17 20:41:45 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri May 17 20:53:28 2013 +0200
@@ -762,9 +762,9 @@
(Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
+ Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
(Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
+ Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
--- a/src/Pure/Pure.thy Fri May 17 20:41:45 2013 +0200
+++ b/src/Pure/Pure.thy Fri May 17 20:53:28 2013 +0200
@@ -74,7 +74,7 @@
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
and "Isabelle.command" :: control
- and "help" "print_commands" "print_configs"
+ and "help" "print_commands" "print_options"
"print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"