src/Pure/General/position.ML

filtering out some package theorems

(*  Title:      Pure/General/position.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Source positions.
*)

signature POSITION =
sig
  type T
  val line_of: T -> int option
  val file_of: T -> string option
  val inc: T -> T
  val none: T
  val line: int -> T
  val file: string -> T
  val path: Path.T -> T
  val of_properties: Markup.property list -> T
  val properties_of: T -> Markup.property list
  val str_of: T -> string
end;

structure Position: POSITION =
struct

(* datatype position *)

datatype T =
  Pos of int option * string option;

fun line_of (Pos (opt_n, _)) = opt_n;
fun file_of (Pos (_, opt_s)) = opt_s;

fun inc (pos as Pos (NONE, _)) = pos
  | inc (Pos (SOME n, opt_s)) = Pos (SOME (n + 1), opt_s);

val none = Pos (NONE, NONE);
fun line n = Pos (SOME n, NONE);
fun file s = Pos (SOME 1, SOME s);

val path = file o Path.implode o Path.expand;


(* markup properties *)

fun of_properties ps =
  let
    val lookup = AList.lookup (op =) ps;
    val opt_n =
      (case lookup Markup.lineN of
        SOME s => Int.fromString s
      | NONE => NONE);
    val opt_s = lookup Markup.fileN;
  in Pos (opt_n, opt_s) end;

fun properties_of (Pos (opt_n, opt_s)) =
  (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @
  (case opt_s of SOME s => [(Markup.fileN, s)] | NONE => []);


(* str_of *)

fun print (Pos (SOME n, NONE)) = "(line " ^ string_of_int n ^ ")"
  | print (Pos (NONE, SOME s)) = "(" ^ s ^ ")"
  | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";

fun str_of (Pos (NONE, NONE)) = ""
  | str_of pos =
      " " ^ Markup.enclose (Markup.properties (properties_of pos) Markup.position) (print pos);

end;