added print_locales, print_locale;
authorwenzelm
Tue, 06 Nov 2001 01:15:08 +0100
changeset 12060 f85eddf6a4fb
parent 12059 c224c941769f
child 12061 1b77d46d0fd1
added print_locales, print_locale;
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);