renamed 'print_configs' to 'print_options';
authorwenzelm
Fri May 17 20:53:28 2013 +0200 (2013-05-17)
changeset 52060179236c82c2a
parent 52059 2f970c7f722b
child 52061 1a52aa84e411
renamed 'print_configs' to 'print_options';
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarRef/Generic.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Fri May 17 20:41:45 2013 +0200
     1.2 +++ b/NEWS	Fri May 17 20:53:28 2013 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  INCOMPATIBILITY, need to use more official Isabelle means to access
     1.5  quick_and_dirty, instead of historical poking into mutable reference.
     1.6  
     1.7 +* Renamed command 'print_configs' to 'print_options'.  Minor
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Sessions may be organized via 'chapter' specifications in the ROOT
    1.11  file, which determines a two-level hierarchy of browser info.  The old
    1.12  tree-like organization via implicit sub-session relation, with its
     2.1 --- a/etc/isar-keywords-ZF.el	Fri May 17 20:41:45 2013 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri May 17 20:53:28 2013 +0200
     2.3 @@ -130,7 +130,6 @@
     2.4      "print_classes"
     2.5      "print_codesetup"
     2.6      "print_commands"
     2.7 -    "print_configs"
     2.8      "print_context"
     2.9      "print_defn_rules"
    2.10      "print_dependencies"
    2.11 @@ -141,6 +140,7 @@
    2.12      "print_locale"
    2.13      "print_locales"
    2.14      "print_methods"
    2.15 +    "print_options"
    2.16      "print_rules"
    2.17      "print_simpset"
    2.18      "print_statement"
    2.19 @@ -299,7 +299,6 @@
    2.20      "print_classes"
    2.21      "print_codesetup"
    2.22      "print_commands"
    2.23 -    "print_configs"
    2.24      "print_context"
    2.25      "print_defn_rules"
    2.26      "print_dependencies"
    2.27 @@ -310,6 +309,7 @@
    2.28      "print_locale"
    2.29      "print_locales"
    2.30      "print_methods"
    2.31 +    "print_options"
    2.32      "print_rules"
    2.33      "print_simpset"
    2.34      "print_statement"
     3.1 --- a/etc/isar-keywords.el	Fri May 17 20:41:45 2013 +0200
     3.2 +++ b/etc/isar-keywords.el	Fri May 17 20:53:28 2013 +0200
     3.3 @@ -184,7 +184,6 @@
     3.4      "print_coercion_maps"
     3.5      "print_coercions"
     3.6      "print_commands"
     3.7 -    "print_configs"
     3.8      "print_context"
     3.9      "print_defn_rules"
    3.10      "print_dependencies"
    3.11 @@ -196,6 +195,7 @@
    3.12      "print_locale"
    3.13      "print_locales"
    3.14      "print_methods"
    3.15 +    "print_options"
    3.16      "print_orders"
    3.17      "print_quotconsts"
    3.18      "print_quotients"
    3.19 @@ -408,7 +408,6 @@
    3.20      "print_coercion_maps"
    3.21      "print_coercions"
    3.22      "print_commands"
    3.23 -    "print_configs"
    3.24      "print_context"
    3.25      "print_defn_rules"
    3.26      "print_dependencies"
    3.27 @@ -420,6 +419,7 @@
    3.28      "print_locale"
    3.29      "print_locales"
    3.30      "print_methods"
    3.31 +    "print_options"
    3.32      "print_orders"
    3.33      "print_quotconsts"
    3.34      "print_quotients"
     4.1 --- a/src/Doc/IsarRef/Generic.thy	Fri May 17 20:41:45 2013 +0200
     4.2 +++ b/src/Doc/IsarRef/Generic.thy	Fri May 17 20:53:28 2013 +0200
     4.3 @@ -31,7 +31,7 @@
     4.4    ``global'', which may not be changed within a local context.
     4.5  
     4.6    \begin{matharray}{rcll}
     4.7 -    @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\
     4.8 +    @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
     4.9    \end{matharray}
    4.10  
    4.11    @{rail "
    4.12 @@ -40,7 +40,7 @@
    4.13  
    4.14    \begin{description}
    4.15    
    4.16 -  \item @{command "print_configs"} prints the available configuration
    4.17 +  \item @{command "print_options"} prints the available configuration
    4.18    options, with names, types, and current values.
    4.19    
    4.20    \item @{text "name = value"} as an attribute expression modifies the
     5.1 --- a/src/Pure/Isar/attrib.ML	Fri May 17 20:41:45 2013 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri May 17 20:53:28 2013 +0200
     5.3 @@ -46,7 +46,7 @@
     5.4      (binding * (thm list * Args.src list) list) list ->
     5.5      (binding * (thm list * Args.src list) list) list
     5.6    val internal: (morphism -> attribute) -> src
     5.7 -  val print_configs: Proof.context -> unit
     5.8 +  val print_options: Proof.context -> unit
     5.9    val config_bool: Binding.binding ->
    5.10      (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    5.11    val config_int: Binding.binding ->
    5.12 @@ -444,7 +444,7 @@
    5.13    fun merge data = Symtab.merge (K true) data;
    5.14  );
    5.15  
    5.16 -fun print_configs ctxt =
    5.17 +fun print_options ctxt =
    5.18    let
    5.19      val thy = Proof_Context.theory_of ctxt;
    5.20      fun prt (name, config) =
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Fri May 17 20:41:45 2013 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri May 17 20:53:28 2013 +0200
     6.3 @@ -762,9 +762,9 @@
     6.4      (Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.improper_command @{command_spec "print_configs"} "print configuration options"
     6.8 +  Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
     6.9      (Scan.succeed (Toplevel.unknown_context o
    6.10 -      Toplevel.keep (Attrib.print_configs o Toplevel.context_of)));
    6.11 +      Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
    6.12  
    6.13  val _ =
    6.14    Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
     7.1 --- a/src/Pure/Pure.thy	Fri May 17 20:41:45 2013 +0200
     7.2 +++ b/src/Pure/Pure.thy	Fri May 17 20:53:28 2013 +0200
     7.3 @@ -74,7 +74,7 @@
     7.4    and "finally" "ultimately" :: prf_chain % "proof"
     7.5    and "back" :: prf_script % "proof"
     7.6    and "Isabelle.command" :: control
     7.7 -  and "help" "print_commands" "print_configs"
     7.8 +  and "help" "print_commands" "print_options"
     7.9      "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
    7.10      "print_theorems" "print_locales" "print_classes" "print_locale"
    7.11      "print_interps" "print_dependencies" "print_attributes"