# HG changeset patch
# User wenzelm
# Date 1005005708 -3600
# Node ID f85eddf6a4fbe2094ab0c4d7d4b30923042fac6f
# Parent  c224c941769fdd1280379dc8e72431868117f17b
added print_locales, print_locale;

diff -r c224c941769f -r f85eddf6a4fb src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 06 01:14:46 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 06 01:15:08 2001 +0100
@@ -46,6 +46,8 @@
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
+  val print_locales: Toplevel.transition -> Toplevel.transition
+  val print_locale: xstring -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
@@ -186,6 +188,12 @@
 val print_theorems = Toplevel.unknown_theory o
   Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
 
+val print_locales = Toplevel.unknown_theory o
+  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
+
+fun print_locale name = Toplevel.unknown_theory o
+  Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) name);
+
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);