src/Pure/PIDE/markup.ML
changeset 77772 7e0d920b4e6e
parent 77028 f5896dea6fce
child 78021 ce6e3bc34343
--- a/src/Pure/PIDE/markup.ML	Sat Apr 01 14:50:43 2023 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Apr 01 14:59:42 2023 +0200
@@ -674,7 +674,7 @@
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
-        Properties.seconds props elapsedN)
+        Properties.get_seconds props elapsedN)
   | _ => NONE);