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