# HG changeset patch
# User wenzelm
# Date 1629809815 -7200
# Node ID af81e4a307be6b8b239d457ac58bbe8eabf47070
# Parent  72bb7e9143f794fb238e955568a539d58a512865
clarified signature;

diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/General/name_space.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -112,7 +112,7 @@
   serial: serial};
 
 fun entry_markup def kind (name, {pos, serial, ...}: entry) =
-  Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
+  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);
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 24 14:56:55 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 entity_properties_of: bool -> serial -> T -> Properties.T
+  val make_entity_markup: 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,9 +215,12 @@
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
-fun entity_properties_of def serial pos =
-  if def then (Markup.defN, Value.print_int serial) :: properties_of pos
-  else (Markup.refN, Value.print_int serial) :: def_properties_of 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
+      else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+  in Markup.entity kind name |> Markup.properties props end;
 
 val markup = Markup.properties o properties_of;
 
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -68,8 +68,7 @@
     fun report def serial pos =
       Context_Position.report (Proof.context_of state)
         (Position.thread_data ())
-          (Markup.entity calculationN ""
-            |> Markup.properties (Position.entity_properties_of def serial pos));
+        (Position.make_entity_markup def serial calculationN ("", pos));
     val calculation =
       (case calc of
         NONE => NONE
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/Isar/keyword.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -216,8 +216,7 @@
 fun command_markup keywords name =
   lookup_command keywords name
   |> Option.map (fn {pos, id, ...} =>
-      Markup.properties (Position.entity_properties_of false id pos)
-        (Markup.entity Markup.command_keywordN name));
+      Position.make_entity_markup false id Markup.command_keywordN (name, pos));
 
 fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -65,8 +65,7 @@
 fun command_pos (Command {pos, ...}) = pos;
 
 fun command_markup def (name, Command {pos, id, ...}) =
-  Markup.properties (Position.entity_properties_of def id pos)
-    (Markup.entity Markup.commandN name);
+  Position.make_entity_markup def id Markup.commandN (name, pos);
 
 fun pretty_command (cmd as (name, Command {comment, ...})) =
   Pretty.block
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -168,8 +168,7 @@
 fun check_session ctxt arg =
   Completion.check_item "session"
     (fn (name, {pos, serial}) =>
-      Markup.entity Markup.sessionN name
-      |> Markup.properties (Position.entity_properties_of false serial pos))
+      Position.make_entity_markup false serial Markup.sessionN (name, pos))
     (get_session_base1 #session_positions) ctxt arg;
 
 fun session_chapter name =
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -60,10 +60,7 @@
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
 fun markup_bound def ps (name, id) =
-  let val entity = Markup.entity Markup.boundN name in
-    Markup.bound ::
-      map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
-  end;
+  Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
   (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
@@ -84,7 +81,7 @@
   | reports_of_scope (def_pos :: ps) =
       let
         val id = serial ();
-        fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos);
+        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)
diff -r 72bb7e9143f7 -r af81e4a307be src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/theory.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -120,9 +120,7 @@
 
 fun theory_markup def name id pos =
   if id = 0 then Markup.empty
-  else
-    Markup.properties (Position.entity_properties_of def id pos)
-      (Markup.entity Markup.theoryN name);
+  else Position.make_entity_markup def id Markup.theoryN (name, pos);
 
 fun init_markup (name, pos) thy =
   let