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