--- a/src/Pure/Isar/isar_syn.ML Thu Jan 06 21:06:17 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Jan 06 21:06:18 2011 +0100
@@ -836,10 +836,16 @@
val _ =
Outer_Syntax.improper_command "print_interps"
- "print interpretations of locale for this theory" Keyword.diag
+ "print interpretations of locale for this theory or proof context" Keyword.diag
(Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
val _ =
+ Outer_Syntax.improper_command "print_dependencies"
+ "print dependencies of locale expression" Keyword.diag
+ (opt_bang -- Parse_Spec.locale_expression true >>
+ (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
+
+val _ =
Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));