# HG changeset patch
# User wenzelm
# Date 1631044070 -7200
# Node ID 839a6e284545fad6a7bc7daf50999b1406e7a288
# Parent  d28a51dd9da65923347f17f10312b4baee7e4179
tuned signature;

diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/General/name_space.ML
--- 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;
 
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -42,7 +42,7 @@
   val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
-  val make_entity_markup: bool -> serial -> string -> string * T -> Markup.T
+  val make_entity_markup: {def: bool} -> serial -> string -> string * T -> Markup.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
@@ -215,7 +215,7 @@
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
-fun make_entity_markup def serial kind (name, pos) =
+fun make_entity_markup {def} serial kind (name, pos) =
   let
     val props =
       if def then (Markup.defN, Value.print_int serial) :: properties_of pos
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -79,10 +79,10 @@
                 val level = Proof.level state;
                 val serial = serial ();
                 val pos = Position.thread_data ();
-                val _ = report true serial pos;
+                val _ = report {def = true} serial pos;
               in SOME {result = result, level = level, serial = serial, pos = pos} end
           | SOME {level, serial, pos, ...} =>
-              (report false serial pos;
+              (report {def = false} serial pos;
                 SOME {result = result, level = level, serial = serial, pos = pos})));
   in
     state
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/Isar/keyword.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -216,7 +216,7 @@
 fun command_markup keywords name =
   lookup_command keywords name
   |> Option.map (fn {pos, id, ...} =>
-      Position.make_entity_markup false id Markup.command_keywordN (name, pos));
+      Position.make_entity_markup {def = false} id Markup.command_keywordN (name, pos));
 
 fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -71,7 +71,8 @@
   Pretty.block
     (Pretty.marks_str
       ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
-        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
+        command_markup {def = false} cmd], name) :: Pretty.str ":" ::
+        Pretty.brk 2 :: Pretty.text comment);
 
 
 (* theory data *)
@@ -124,7 +125,7 @@
         | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
       val _ =
         Context_Position.report_generic (Context.the_generic_context ())
-          (command_pos cmd) (command_markup true (name, cmd));
+          (command_pos cmd) (command_markup {def = true} (name, cmd));
     in Data.map (Symtab.update (name, cmd)) thy end;
 
 val _ = Theory.setup (Theory.at_end (fn thy =>
@@ -288,7 +289,7 @@
     let val name = Token.content_of tok in
       (case lookup_commands thy name of
         NONE => []
-      | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
+      | SOME cmd => [((Token.pos_of tok, command_markup {def = false} (name, cmd)), "")])
     end
   else [];
 
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -168,7 +168,7 @@
 fun check_session ctxt arg =
   Completion.check_item "session"
     (fn (name, {pos, serial}) =>
-      Position.make_entity_markup false serial Markup.sessionN (name, pos))
+      Position.make_entity_markup {def = false} serial Markup.sessionN (name, pos))
     (get_session_base1 #session_positions) ctxt arg;
 
 fun session_chapter name =
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -84,7 +84,7 @@
         fun entity def = Position.make_entity_markup def id "" ("", def_pos);
       in
         map (rpair Markup.bound) (def_pos :: ps) @
-        ((def_pos, entity true) :: map (rpair (entity false)) ps)
+        ((def_pos, entity {def = true}) :: map (rpair (entity {def = false})) ps)
       end;
 
 
@@ -279,7 +279,7 @@
           | decode _ qs bs (Abs (x, T, t)) =
               let
                 val id = serial ();
-                val _ = report qs (markup_bound true qs) (x, id);
+                val _ = report qs (markup_bound {def = true} qs) (x, id);
               in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
           | decode ps _ _ (Const (a, T)) =
@@ -306,7 +306,7 @@
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
-                SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
+                SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t)
               | NONE => t);
 
         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
diff -r d28a51dd9da6 -r 839a6e284545 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 07 21:16:22 2021 +0200
+++ b/src/Pure/theory.ML	Tue Sep 07 21:47:50 2021 +0200
@@ -125,12 +125,12 @@
 fun init_markup (name, pos) thy =
   let
     val id = serial ();
-    val _ = Context_Position.reports_global thy [(pos, theory_markup true name id pos)];
+    val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)];
   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
 
 fun get_markup thy =
   let val {pos, id, ...} = rep_theory thy
-  in theory_markup false (Context.theory_long_name thy) id pos end;
+  in theory_markup {def = false} (Context.theory_long_name thy) id pos end;
 
 fun check long ctxt (name, pos) =
   let