# HG changeset patch # User wenzelm # Date 1183803375 -7200 # Node ID f543538866a2ec970b24788064a69de718aef208 # Parent 5e6c5388e836710d2a825e986eb17d366a0883fb added property conversions; tuned; diff -r 5e6c5388e836 -r f543538866a2 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sat Jul 07 12:16:14 2007 +0200 +++ b/src/Pure/General/position.ML Sat Jul 07 12:16:15 2007 +0200 @@ -12,10 +12,12 @@ val line: int -> T val name: string -> T val line_name: int -> string -> T + val line_of: T -> int option + val name_of: T -> string option val inc: T -> T val str_of: T -> string - val line_of: T -> int option - val name_of: T -> string option + val of_properties: Markup.property list -> T + val properties_of: T -> Markup.property list end; structure Position: POSITION = @@ -32,6 +34,9 @@ fun name s = Pos (NONE, SOME s); fun line_name n s = Pos (SOME n, SOME s); +fun line_of (Pos (opt_n, _)) = opt_n; +fun name_of (Pos (_, opt_s)) = opt_s; + (* increment *) @@ -46,10 +51,21 @@ | str_of (Pos (NONE, SOME s)) = " (" ^ s ^ ")" | str_of (Pos (SOME n, SOME s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")"; -fun line_of (Pos (SOME n,_)) = SOME n - | line_of _ = NONE + +(* markup properties *) -fun name_of (Pos (_,SOME s)) = SOME s - | name_of _ = NONE +fun of_properties ps = + let + val lookup = AList.lookup (op =) ps; + val opt_n = + (case lookup Markup.pos_lineN of + SOME s => Int.fromString s + | NONE => NONE); + val opt_s = lookup Markup.pos_nameN; + in Pos (opt_n, opt_s) end; + +fun properties_of (Pos (opt_n, opt_s)) = + (case opt_n of SOME n => [(Markup.pos_lineN, string_of_int n)] | NONE => []) @ + (case opt_s of SOME s => [(Markup.pos_nameN, s)] | NONE => []); end;