--- 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);
--- 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;
--- 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
--- 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;
--- 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
--- 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 =
--- 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)
--- 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