# HG changeset patch
# User wenzelm
# Date 1590602522 -7200
# Node ID f8b0271cc744efa7fbca17c19d9b3e02ea94df38
# Parent  cdcf2fcf3f5433792661cc271140849c10f46290
tuned signature;

diff -r cdcf2fcf3f54 -r f8b0271cc744 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/General/position.ML	Wed May 27 20:02:02 2020 +0200
@@ -38,6 +38,7 @@
   val properties_of: T -> Properties.T
   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 default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
@@ -203,6 +204,9 @@
 
 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
+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;
diff -r cdcf2fcf3f54 -r f8b0271cc744 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/Isar/method.ML	Wed May 27 20:02:02 2020 +0200
@@ -607,8 +607,7 @@
 
                 val modifier_report =
                   (#1 (Token.range_of modifier_toks),
-                    Markup.properties (Position.def_properties_of pos)
-                      (Markup.entity Markup.method_modifierN ""));
+                    Position.entity_markup Markup.method_modifierN ("", pos));
                 val _ =
                   Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0);
                 val _ = Token.assign (SOME (Token.Declaration decl)) tok0;
diff -r cdcf2fcf3f54 -r f8b0271cc744 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed May 27 20:02:02 2020 +0200
@@ -979,9 +979,7 @@
           | [] => err [] "Failed to retrieve literal fact"
           | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
 
-        val markup =
-          Markup.entity Markup.literal_factN ""
-          |> Markup.properties (Position.def_properties_of thm_pos);
+        val markup = Position.entity_markup Markup.literal_factN ("", thm_pos);
         val _ = Context_Position.report_generic context pos markup;
       in pick true ("", thm_pos) [thm] end
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
diff -r cdcf2fcf3f54 -r f8b0271cc744 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 27 20:02:02 2020 +0200
@@ -76,10 +76,7 @@
         val def_pos = Exn_Properties.position_of_polyml_location decl;
       in
         (is_reported pos andalso pos <> def_pos) ?
-          let
-            fun markup () =
-              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
-          in cons (pos, markup, fn () => "") end
+          cons (pos, fn () => Position.entity_markup kind ("", def_pos), fn () => "")
       end;
 
     fun reported_entity_id def id loc =