--- a/src/Pure/General/name_space.ML Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/General/name_space.ML Tue Sep 07 21:47:50 2021 +0200
@@ -117,7 +117,7 @@
Position.make_entity_markup def serial kind (name, pos);
fun print_entry_ref kind (name, entry) =
- quote (Markup.markup (entry_markup false kind (name, entry)) name);
+ quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
fun err_dup kind entry1 entry2 pos =
error ("Duplicate " ^ plain_words kind ^ " declaration " ^
@@ -170,8 +170,8 @@
NONE => Markup.intensify
| SOME (_, entry) => entry_markup def kind (name, entry));
-val markup = gen_markup false;
-val markup_def = gen_markup true;
+val markup = gen_markup {def = false};
+val markup_def = gen_markup {def = true};
fun undefined (space as Name_Space {kind, entries, ...}) bad =
let
@@ -545,7 +545,7 @@
in (kind, internals', entries') end);
val _ =
if proper_pos andalso Context_Position.is_reported_generic context pos then
- Position.report pos (entry_markup true (kind_of space) (name, entry))
+ Position.report pos (entry_markup {def = true} (kind_of space) (name, entry))
else ();
in (name, space') end;