# HG changeset patch
# User wenzelm
# Date 1368816808 -7200
# Node ID 179236c82c2a588884d38eba251260507a1c51ac
# Parent  2f970c7f722bc43b5f836d8fc6a64bebfa70951b
renamed 'print_configs' to 'print_options';

diff -r 2f970c7f722b -r 179236c82c2a NEWS
--- 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
diff -r 2f970c7f722b -r 179236c82c2a etc/isar-keywords-ZF.el
--- 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"
diff -r 2f970c7f722b -r 179236c82c2a etc/isar-keywords.el
--- 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"
diff -r 2f970c7f722b -r 179236c82c2a src/Doc/IsarRef/Generic.thy
--- 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
diff -r 2f970c7f722b -r 179236c82c2a src/Pure/Isar/attrib.ML
--- 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) =
diff -r 2f970c7f722b -r 179236c82c2a src/Pure/Isar/isar_syn.ML
--- 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"
diff -r 2f970c7f722b -r 179236c82c2a src/Pure/Pure.thy
--- 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"