# HG changeset patch
# User haftmann
# Date 1277053361 -7200
# Node ID 907e130726750f24a1fedda4f3625b75845c0bad
# Parent  fcc768dc9dd0d51f0233d7efe868548c5fd9cde7
separate section for diagnostic commands

diff -r fcc768dc9dd0 -r 907e13072675 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Jun 19 09:50:30 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Jun 20 19:02:41 2010 +0200
@@ -73,6 +73,7 @@
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
+  val all_locales: theory -> string list
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
   val print_registrations: theory -> string -> unit
@@ -149,10 +150,6 @@
 fun change_locale name =
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
 
-fun print_locales thy =
-  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
-  |> Pretty.writeln;
-
 
 (*** Primitive operations ***)
 
@@ -343,20 +340,6 @@
   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
     ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
 
-fun print_locale thy show_facts raw_name =
-  let
-    val name = intern thy raw_name;
-    val ctxt = init name thy;
-    fun cons_elem (elem as Notes _) = show_facts ? cons elem
-      | cons_elem elem = cons elem;
-    val elems =
-      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
-      |> snd |> rev;
-  in
-    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
-    |> Pretty.writeln
-  end;
-
 
 (*** Registrations: interpretations in theories ***)
 
@@ -458,15 +441,6 @@
   in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
 
 
-(* Diagnostic *)
-
-fun print_registrations thy raw_name =
-  (case these_registrations thy (intern thy raw_name) of
-      [] => Pretty.str ("no interpretations")
-    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
-  |> Pretty.writeln;
-
-
 (* Add and extend registrations *)
 
 fun amend_registration (name, morph) mixin export thy =
@@ -595,4 +569,33 @@
   Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
     "back-chain all introduction rules of locales"));
 
+
+(*** diagnostic commands and interfaces ***)
+
+fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy));
+
+fun print_locales thy =
+  Pretty.strs ("locales:" :: all_locales thy)
+  |> Pretty.writeln;
+
+fun print_locale thy show_facts raw_name =
+  let
+    val name = intern thy raw_name;
+    val ctxt = init name thy;
+    fun cons_elem (elem as Notes _) = show_facts ? cons elem
+      | cons_elem elem = cons elem;
+    val elems =
+      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
+      |> snd |> rev;
+  in
+    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
+    |> Pretty.writeln
+  end;
+
+fun print_registrations thy raw_name =
+  (case these_registrations thy (intern thy raw_name) of
+      [] => Pretty.str ("no interpretations")
+    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+  |> Pretty.writeln;
+
 end;