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