# 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