renamed 'print_options' to 'print_configs';
authorwenzelm
Wed, 01 Aug 2007 16:55:43 +0200
changeset 24115 39b407fd6e82
parent 24114 1b0bc10019a5
child 24116 9915c39e0820
renamed 'print_options' to 'print_configs';
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Aug 01 16:55:42 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Aug 01 16:55:43 2007 +0200
@@ -78,7 +78,7 @@
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_abbrevs: Toplevel.transition -> Toplevel.transition
   val print_facts: Toplevel.transition -> Toplevel.transition
-  val print_options: Toplevel.transition -> Toplevel.transition
+  val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * (Locale.expr * Element.context list)
@@ -437,8 +437,8 @@
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Toplevel.context_of state));
 
-val print_options = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ConfigOption.print_options (Toplevel.context_of state));
+val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
+  Attrib.print_configs (Toplevel.context_of state));
 
 val print_theorems_proof = Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 01 16:55:42 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 01 16:55:43 2007 +0200
@@ -731,9 +731,9 @@
   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
 
-val print_optionsP =
-  OuterSyntax.improper_command "print_options" "print configuration options" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_options));
+val print_configsP =
+  OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
 
 val print_contextP =
   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
@@ -1013,7 +1013,7 @@
   interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_classesP, print_commandsP,
-  print_optionsP, print_contextP, print_theoryP, print_syntaxP,
+  print_configsP, print_contextP, print_theoryP, print_syntaxP,
   print_abbrevsP, print_factsP, print_theoremsP, print_localesP,
   print_localeP, print_registrationsP, print_attributesP,
   print_simpsetP, print_rulesP, print_induct_rulesP,