# HG changeset patch
# User wenzelm
# Date 1680354095 -7200
# Node ID 4b2262cfbf13aeffc9cda9b73267ee049ac26072
# Parent  7e0d920b4e6eb7bb70c3ad09fd7087277f41e418
more uniform treatment of properties (but < 0 should not occur here);

diff -r 7e0d920b4e6e -r 4b2262cfbf13 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 14:59:42 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 15:01:35 2023 +0200
@@ -208,7 +208,7 @@
     end_offset = Properties.get_int props Markup.end_offsetN,
     props = props};
 
-fun int_entry k i = if invalid i then [] else [(k, Value.print_int i)];
+fun int_entry k i = if i = 0 then [] else [(k, Value.print_int i)];
 
 fun properties_of (Pos {line, offset, end_offset, props}) =
   int_entry Markup.lineN line @