# HG changeset patch
# User wenzelm
# Date 1680353982 -7200
# Node ID 7e0d920b4e6eb7bb70c3ad09fd7087277f41e418
# Parent  279b18bb4059cdae77576de5720807fbb4154ae1
tuned signature;

diff -r 279b18bb4059 -r 7e0d920b4e6e src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 01 14:50:43 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 14:59:42 2023 +0200
@@ -201,16 +201,11 @@
 
 (* markup properties *)
 
-fun get_int props name =
-  (case Properties.get props name of
-    NONE => 0
-  | SOME s => Value.parse_int s);
-
 fun of_properties props =
   make {
-    line = get_int props Markup.lineN,
-    offset = get_int props Markup.offsetN,
-    end_offset = get_int props Markup.end_offsetN,
+    line = Properties.get_int props Markup.lineN,
+    offset = Properties.get_int props Markup.offsetN,
+    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)];
@@ -301,8 +296,8 @@
   let
     val pos = of_properties props;
     val pos' =
-      make {line = get_int props Markup.end_lineN,
-        offset = get_int props Markup.end_offsetN,
+      make {line = Properties.get_int props Markup.end_lineN,
+        offset = Properties.get_int props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
diff -r 279b18bb4059 -r 7e0d920b4e6e src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Sat Apr 01 14:50:43 2023 +0200
+++ b/src/Pure/General/properties.ML	Sat Apr 01 14:59:42 2023 +0200
@@ -14,7 +14,9 @@
   val get: T -> string -> string option
   val put: entry -> T -> T
   val remove: string -> T -> T
-  val seconds: T -> string -> Time.time
+  val get_string: T -> string -> string
+  val get_int: T -> string -> int
+  val get_seconds: T -> string -> Time.time
 end;
 
 structure Properties: PROPERTIES =
@@ -31,8 +33,15 @@
 fun put entry (props: T) = AList.update (op =) entry props;
 fun remove name (props: T) = AList.delete (op =) name props;
 
-fun seconds props name =
-  (case AList.lookup (op =) props name of
+val get_string = the_default "" oo get;
+
+fun get_int props name =
+  (case get props name of
+    NONE => 0
+  | SOME s => Value.parse_int s);
+
+fun get_seconds props name =
+  (case get props name of
     NONE => Time.zeroTime
   | SOME s => Time.fromReal (the_default 0.0 (Real.fromString s)));
 
diff -r 279b18bb4059 -r 7e0d920b4e6e src/Pure/PIDE/markup.ML
--- 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);