src/Pure/Isar/isar_syn.ML
changeset 7308 e01aab03a2a1
parent 7269 8aa45a40c87a
child 7368 6b1b6b7c1df0
--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:43:25 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:44:29 1999 +0200
@@ -440,6 +440,10 @@
   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
 
+val print_contextP =
+  OuterSyntax.improper_command "print_context" "print theory context name" K.diag
+    (Scan.succeed IsarCmd.print_context);
+
 val print_theoryP =
   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
     (Scan.succeed IsarCmd.print_theory);
@@ -587,9 +591,10 @@
   skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
   cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
-  pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
-  print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
-  print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
+  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
+  print_syntaxP, print_attributesP, print_methodsP, print_theoremsP,
+  print_bindsP, print_lthmsP, print_thmsP, print_propP, print_termP,
+  print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,