# HG changeset patch # User wenzelm # Date 1680038187 -7200 # Node ID e64428b6b170aa763adbda917f8f16bb9c87cc34 # Parent 81d553e9428d1034074d2c9a0232fb7d5c93197e more operations, notably for profiling; diff -r 81d553e9428d -r e64428b6b170 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Mar 28 22:46:38 2023 +0200 +++ b/src/Pure/Isar/locale.ML Tue Mar 28 23:16:27 2023 +0200 @@ -84,6 +84,7 @@ (* Diagnostic *) val get_locales: theory -> string list + val locale_notes: theory -> string -> (string * Attrib.fact list) list val pretty_locales: theory -> bool -> Pretty.T val pretty_locale: theory -> bool -> string -> Pretty.T val pretty_registrations: Proof.context -> string -> Pretty.T @@ -453,9 +454,12 @@ then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts))) else Notes (kind, [((b, atts), facts)])); +fun locale_notes thy loc = + fold (cons o #1) (#notes (the_locale thy loc)) []; + fun lazy_notes thy loc = - rev (#notes (the_locale thy loc)) - |> maps (fn ((kind, notes), _) => make_notes kind notes); + locale_notes thy loc + |> maps (fn (kind, notes) => make_notes kind notes); fun consolidate_notes elems = elems