src/Pure/Isar/locale.ML

--- a/src/Pure/Isar/locale.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -407,8 +407,6 @@
     (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |>
       Pretty.string_of));
 
-(* Declarations, facts and entire locale content *)
-
 fun init_element elem context =
   context
   |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
@@ -417,6 +415,28 @@
       let val ctxt0 = Context.proof_of context
       in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
 
+
+(* Potentially lazy notes *)
+
+fun lazy_notes thy loc =
+  rev (#notes (the_locale thy loc)) |> maps (fn ((kind, notes), _) =>
+    notes |> map (fn ((b, atts), facts) =>
+      if null atts andalso forall (null o #2) facts andalso false (* FIXME *)
+      then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
+      else Notes (kind, [((b, atts), facts)])));
+
+fun consolidate_notes elems =
+  (elems
+    |> map_filter (fn Lazy_Notes (_, (_, ths)) => SOME ths | _ => NONE)
+    |> Lazy.consolidate;
+   elems);
+
+fun force_notes (Lazy_Notes (kind, (b, ths))) = Notes (kind, [((b, []), [(Lazy.force ths, [])])])
+  | force_notes elem = elem;
+
+
+(* Declarations, facts and entire locale content *)
+
 fun activate_syntax_decls (name, morph) context =
   let
     val thy = Context.theory_of context;
@@ -435,15 +455,11 @@
         NONE => Morphism.identity
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
-    val notes' =
-      grouped 100 Par_List.map
-        (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
+    val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
   in
-    input
-    |> fold_rev
-        (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes'
-      handle ERROR msg => activate_err msg (name, morph) context
-  end;
+    (notes', input) |-> fold (fn elem => fn res =>
+      activ_elem (Element.transform_ctxt (transfer res) elem) res)
+  end handle ERROR msg => activate_err msg (name, morph) context;
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
@@ -682,10 +698,13 @@
   let
     val locale_ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
+      | cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
     val elems =
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
-      |> snd |> rev;
+      |> snd |> rev
+      |> consolidate_notes
+      |> map force_notes;
   in
     Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
       maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems