src/Pure/General/position.ML
author wenzelm
Wed, 13 Jan 1999 15:18:02 +0100
changeset 6118 caa439435666
parent 5010 9101b70b696d
child 8806 a202293db3f6
permissions -rw-r--r--
fixed titles;
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
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     5
Input positions.
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
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    11
  val none: T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    12
  val line: int -> T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    13
  val name: string -> T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    14
  val line_name: int -> string -> T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    15
  val inc: T -> T
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    16
  val str_of: T -> string
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    17
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    18
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    19
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    20
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    21
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
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    24
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    25
datatype T =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    26
  Pos of int option * string option;
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
val none = Pos (None, None);
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    29
fun line n = Pos (Some n, None);
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    30
fun name s = Pos (None, Some s);
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    31
fun line_name n s = Pos (Some n, Some s);
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    32
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    33
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    34
(* increment *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    35
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    36
fun inc (pos as Pos (None, _)) = pos
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    37
  | inc (Pos (Some n, opt_s)) = Pos (Some (n + 1), opt_s);
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    38
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    39
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    40
(* str_of *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    41
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    42
fun str_of (Pos (None, None)) = ""
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    43
  | str_of (Pos (Some n, None)) = " (line " ^ string_of_int n ^ ")"
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    44
  | str_of (Pos (None, Some s)) = " (" ^ s ^ ")"
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    45
  | str_of (Pos (Some n, Some s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    46
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    47
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    48
end;