# HG changeset patch
# User wenzelm
# Date 1680377124 -7200
# Node ID 13cee8c2ed8dc8bcdb9346ad559a085b6eed8ccc
# Parent  58e53c61f15f238b9dd4c31f64195e408edda919
clarified signature;

diff -r 58e53c61f15f -r 13cee8c2ed8d src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 21:12:44 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 21:25:24 2023 +0200
@@ -212,15 +212,12 @@
     end_offset = Properties.get_int props Markup.end_offsetN,
     props = props};
 
-fun string_entry k s = if s = "" then [] else [(k, s)];
-fun int_entry k i = if i = 0 then [] else [(k, Value.print_int i)];
-
 fun properties_of (Pos {line, offset, end_offset, props = {file, id}}) =
-  int_entry Markup.lineN line @
-  int_entry Markup.offsetN offset @
-  int_entry Markup.end_offsetN end_offset @
-  string_entry Markup.fileN file @
-  string_entry Markup.idN id;
+  Properties.make_int Markup.lineN line @
+  Properties.make_int Markup.offsetN offset @
+  Properties.make_int Markup.end_offsetN end_offset @
+  Properties.make_string Markup.fileN file @
+  Properties.make_string Markup.idN id;
 
 val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
@@ -310,7 +307,7 @@
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
-  properties_of pos @ int_entry Markup.end_lineN (the_default 0 (line_of pos'));
+  properties_of pos @ Properties.make_int Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
diff -r 58e53c61f15f -r 13cee8c2ed8d src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Sat Apr 01 21:12:44 2023 +0200
+++ b/src/Pure/General/properties.ML	Sat Apr 01 21:25:24 2023 +0200
@@ -14,6 +14,8 @@
   val get: T -> string -> string option
   val put: entry -> T -> T
   val remove: string -> T -> T
+  val make_string: string -> string -> T
+  val make_int: string -> int -> T
   val get_string: T -> string -> string
   val get_int: T -> string -> int
   val get_seconds: T -> string -> Time.time
@@ -33,6 +35,9 @@
 fun put entry (props: T) = AList.update (op =) entry props;
 fun remove name (props: T) = AList.delete (op =) name props;
 
+fun make_string k s = if s = "" then [] else [(k, s)];
+fun make_int k i = if i = 0 then [] else [(k, Value.print_int i)];
+
 val get_string = the_default "" oo get;
 
 fun get_int props name =