--- 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;