replaced name by file (unquoted);
authorwenzelm
Mon Jul 09 23:12:37 2007 +0200 (2007-07-09)
changeset 2367367c748e5ae54
parent 23672 3fd7770f6795
child 23674 c7cbab93f1d9
replaced name by file (unquoted);
str_of: markup;
misc cleanup;
src/Pure/General/position.ML
     1.1 --- a/src/Pure/General/position.ML	Mon Jul 09 23:12:36 2007 +0200
     1.2 +++ b/src/Pure/General/position.ML	Mon Jul 09 23:12:37 2007 +0200
     1.3 @@ -2,54 +2,43 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Input positions.
     1.8 +Source positions.
     1.9  *)
    1.10  
    1.11  signature POSITION =
    1.12  sig
    1.13    type T
    1.14 +  val line_of: T -> int option
    1.15 +  val file_of: T -> string option
    1.16 +  val inc: T -> T
    1.17    val none: T
    1.18    val line: int -> T
    1.19 -  val name: string -> T
    1.20 -  val line_name: int -> string -> T
    1.21 -  val line_of: T -> int option
    1.22 -  val name_of: T -> string option
    1.23 -  val inc: T -> T
    1.24 -  val str_of: T -> string
    1.25 +  val file: string -> T
    1.26 +  val path: Path.T -> T
    1.27    val of_properties: Markup.property list -> T
    1.28    val properties_of: T -> Markup.property list
    1.29 +  val str_of: T -> string
    1.30  end;
    1.31  
    1.32  structure Position: POSITION =
    1.33  struct
    1.34  
    1.35 -
    1.36  (* datatype position *)
    1.37  
    1.38  datatype T =
    1.39    Pos of int option * string option;
    1.40  
    1.41 -val none = Pos (NONE, NONE);
    1.42 -fun line n = Pos (SOME n, NONE);
    1.43 -fun name s = Pos (NONE, SOME s);
    1.44 -fun line_name n s = Pos (SOME n, SOME s);
    1.45 -
    1.46  fun line_of (Pos (opt_n, _)) = opt_n;
    1.47 -fun name_of (Pos (_, opt_s)) = opt_s;
    1.48 -
    1.49 -
    1.50 -(* increment *)
    1.51 +fun file_of (Pos (_, opt_s)) = opt_s;
    1.52  
    1.53  fun inc (pos as Pos (NONE, _)) = pos
    1.54    | inc (Pos (SOME n, opt_s)) = Pos (SOME (n + 1), opt_s);
    1.55  
    1.56 -
    1.57 -(* str_of *)
    1.58 +val none = Pos (NONE, NONE);
    1.59 +fun line n = Pos (SOME n, NONE);
    1.60 +fun file s = Pos (SOME 1, SOME s);
    1.61  
    1.62 -fun str_of (Pos (NONE, NONE)) = ""
    1.63 -  | str_of (Pos (SOME n, NONE)) = " (line " ^ string_of_int n ^ ")"
    1.64 -  | str_of (Pos (NONE, SOME s)) = " (" ^ s ^ ")"
    1.65 -  | str_of (Pos (SOME n, SOME s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
    1.66 +val path = file o Path.implode o Path.expand;
    1.67  
    1.68  
    1.69  (* markup properties *)
    1.70 @@ -58,14 +47,25 @@
    1.71    let
    1.72      val lookup = AList.lookup (op =) ps;
    1.73      val opt_n =
    1.74 -      (case lookup Markup.pos_lineN of
    1.75 +      (case lookup Markup.lineN of
    1.76          SOME s => Int.fromString s
    1.77        | NONE => NONE);
    1.78 -    val opt_s = lookup Markup.pos_nameN;
    1.79 +    val opt_s = lookup Markup.fileN;
    1.80    in Pos (opt_n, opt_s) end;
    1.81  
    1.82  fun properties_of (Pos (opt_n, opt_s)) =
    1.83 -  (case opt_n of SOME n => [(Markup.pos_lineN, string_of_int n)] | NONE => []) @
    1.84 -  (case opt_s of SOME s => [(Markup.pos_nameN, s)] | NONE => []);
    1.85 +  (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @
    1.86 +  (case opt_s of SOME s => [(Markup.fileN, s)] | NONE => []);
    1.87 +
    1.88 +
    1.89 +(* str_of *)
    1.90 +
    1.91 +fun print (Pos (SOME n, NONE)) = "(line " ^ string_of_int n ^ ")"
    1.92 +  | print (Pos (NONE, SOME s)) = "(" ^ s ^ ")"
    1.93 +  | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
    1.94 +
    1.95 +fun str_of (Pos (NONE, NONE)) = ""
    1.96 +  | str_of pos = " " ^ Pretty.string_of (Pretty.markup
    1.97 +        (Markup.properties (properties_of pos) Markup.position) [Pretty.str (print pos)]);
    1.98  
    1.99  end;