# HG changeset patch # User wenzelm # Date 1185980143 -7200 # Node ID 39b407fd6e8239896b50145d29474a4dd5a25547 # Parent 1b0bc10019a567078e777fd9ffeef46d99d5fd54 renamed 'print_options' to 'print_configs'; diff -r 1b0bc10019a5 -r 39b407fd6e82 src/Pure/Isar/isar_cmd.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 diff -r 1b0bc10019a5 -r 39b407fd6e82 src/Pure/Isar/isar_syn.ML --- 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,