src/Pure/General/position.ML
author wenzelm
Tue, 10 Jul 2007 16:45:00 +0200
changeset 23697 63e3b2e383dd
parent 23673 67c748e5ae54
child 23720 d0d583c7a41f
permissions -rw-r--r--
Markup.output;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5010
diff changeset
     1
(*  Title:      Pure/General/position.ML
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     4
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
     5
Source positions.
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     6
*)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     7
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     8
signature POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     9
sig
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    10
  type T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    11
  val line_of: T -> int option
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    12
  val file_of: T -> string option
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    13
  val inc: T -> T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    14
  val none: T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    15
  val line: int -> T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    16
  val file: string -> T
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    17
  val path: Path.T -> T
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    18
  val of_properties: Markup.property list -> T
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    19
  val properties_of: T -> Markup.property list
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    20
  val str_of: T -> string
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    21
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    22
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    23
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    24
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    25
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    26
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    27
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    28
datatype T =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    29
  Pos of int option * string option;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    30
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    31
fun line_of (Pos (opt_n, _)) = opt_n;
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    32
fun file_of (Pos (_, opt_s)) = opt_s;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    33
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    34
fun inc (pos as Pos (NONE, _)) = pos
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    35
  | inc (Pos (SOME n, opt_s)) = Pos (SOME (n + 1), opt_s);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    36
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    37
val none = Pos (NONE, NONE);
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    38
fun line n = Pos (SOME n, NONE);
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    39
fun file s = Pos (SOME 1, SOME s);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    40
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    41
val path = file o Path.implode o Path.expand;
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    42
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    43
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    44
(* markup properties *)
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
    45
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    46
fun of_properties ps =
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    47
  let
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    48
    val lookup = AList.lookup (op =) ps;
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    49
    val opt_n =
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    50
      (case lookup Markup.lineN of
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    51
        SOME s => Int.fromString s
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    52
      | NONE => NONE);
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    53
    val opt_s = lookup Markup.fileN;
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    54
  in Pos (opt_n, opt_s) end;
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    55
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    56
fun properties_of (Pos (opt_n, opt_s)) =
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    57
  (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    58
  (case opt_s of SOME s => [(Markup.fileN, s)] | NONE => []);
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    59
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    60
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    61
(* str_of *)
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    62
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    63
fun print (Pos (SOME n, NONE)) = "(line " ^ string_of_int n ^ ")"
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    64
  | print (Pos (NONE, SOME s)) = "(" ^ s ^ ")"
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    65
  | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    66
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    67
fun str_of (Pos (NONE, NONE)) = ""
23697
63e3b2e383dd Markup.output;
wenzelm
parents: 23673
diff changeset
    68
  | str_of pos = " " ^
63e3b2e383dd Markup.output;
wenzelm
parents: 23673
diff changeset
    69
      (Markup.output (Markup.properties (properties_of pos) Markup.position) |-> enclose)
63e3b2e383dd Markup.output;
wenzelm
parents: 23673
diff changeset
    70
        (print pos);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    71
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    72
end;