src/Pure/Isar/isar_syn.ML
changeset 41435 12585dfb86fe
parent 41270 dea60d052923
child 41536 47fef6afe756
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:17 2011 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 06 21:06:18 2011 +0100
     1.3 @@ -836,10 +836,16 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.improper_command "print_interps"
     1.7 -    "print interpretations of locale for this theory" Keyword.diag
     1.8 +    "print interpretations of locale for this theory or proof context" Keyword.diag
     1.9      (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
    1.10  
    1.11  val _ =
    1.12 +  Outer_Syntax.improper_command "print_dependencies"
    1.13 +    "print dependencies of locale expression" Keyword.diag
    1.14 +    (opt_bang -- Parse_Spec.locale_expression true >>
    1.15 +      (Toplevel.no_timing oo Isar_Cmd.print_dependencies));
    1.16 +
    1.17 +val _ =
    1.18    Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
    1.19      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
    1.20