src/Pure/General/position.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23720 d0d583c7a41f
child 25551 87d89b0f847a
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/position.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Source positions.
     6 *)
     7 
     8 signature POSITION =
     9 sig
    10   type T
    11   val line_of: T -> int option
    12   val file_of: T -> string option
    13   val inc: T -> T
    14   val none: T
    15   val line: int -> T
    16   val file: string -> T
    17   val path: Path.T -> T
    18   val of_properties: Markup.property list -> T
    19   val properties_of: T -> Markup.property list
    20   val str_of: T -> string
    21 end;
    22 
    23 structure Position: POSITION =
    24 struct
    25 
    26 (* datatype position *)
    27 
    28 datatype T =
    29   Pos of int option * string option;
    30 
    31 fun line_of (Pos (opt_n, _)) = opt_n;
    32 fun file_of (Pos (_, opt_s)) = opt_s;
    33 
    34 fun inc (pos as Pos (NONE, _)) = pos
    35   | inc (Pos (SOME n, opt_s)) = Pos (SOME (n + 1), opt_s);
    36 
    37 val none = Pos (NONE, NONE);
    38 fun line n = Pos (SOME n, NONE);
    39 fun file s = Pos (SOME 1, SOME s);
    40 
    41 val path = file o Path.implode o Path.expand;
    42 
    43 
    44 (* markup properties *)
    45 
    46 fun of_properties ps =
    47   let
    48     val lookup = AList.lookup (op =) ps;
    49     val opt_n =
    50       (case lookup Markup.lineN of
    51         SOME s => Int.fromString s
    52       | NONE => NONE);
    53     val opt_s = lookup Markup.fileN;
    54   in Pos (opt_n, opt_s) end;
    55 
    56 fun properties_of (Pos (opt_n, opt_s)) =
    57   (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @
    58   (case opt_s of SOME s => [(Markup.fileN, s)] | NONE => []);
    59 
    60 
    61 (* str_of *)
    62 
    63 fun print (Pos (SOME n, NONE)) = "(line " ^ string_of_int n ^ ")"
    64   | print (Pos (NONE, SOME s)) = "(" ^ s ^ ")"
    65   | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
    66 
    67 fun str_of (Pos (NONE, NONE)) = ""
    68   | str_of pos =
    69       " " ^ Markup.enclose (Markup.properties (properties_of pos) Markup.position) (print pos);
    70 
    71 end;