# HG changeset patch
# User wenzelm
# Date 1185394851 -7200
# Node ID d7df8545f9f6d2672bb989cdea9b664fc6f466be
# Parent  aa46577f4f4445b538557f2ce04f88075b405e9c
added command 'print_options';

diff -r aa46577f4f44 -r d7df8545f9f6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 25 22:20:50 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 25 22:20:51 2007 +0200
@@ -78,6 +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_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * (Locale.expr * Element.context list)
@@ -436,6 +437,9 @@
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Toplevel.context_of state));
 
+val print_options = Toplevel.unknown_context o Toplevel.keep (fn state =>
+  Config.print_configs (Toplevel.context_of state));
+
 val print_theorems_proof = Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
diff -r aa46577f4f44 -r d7df8545f9f6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 25 22:20:50 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 25 22:20:51 2007 +0200
@@ -731,6 +731,10 @@
   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_contextP =
   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
@@ -1009,14 +1013,15 @@
   interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_classesP, print_commandsP,
-  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, print_trans_rulesP,
-  print_methodsP, print_antiquotationsP, thy_depsP, class_depsP,
-  thm_depsP, find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
-  print_thmsP, print_prfsP, print_full_prfsP, print_propP,
-  print_termP, print_typeP, print_codesetupP,
+  print_optionsP, 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,
+  print_trans_rulesP, print_methodsP, print_antiquotationsP,
+  thy_depsP, class_depsP, thm_depsP, find_theoremsP, print_bindsP,
+  print_casesP, print_stmtsP, print_thmsP, print_prfsP,
+  print_full_prfsP, print_propP, print_termP, print_typeP,
+  print_codesetupP,
   (*system commands*)
   cdP, pwdP, use_thyP, update_thyP, touch_thyP, touch_all_thysP,
   touch_child_thysP, remove_thyP, kill_thyP, display_draftsP,