# HG changeset patch
# User wenzelm
# Date 895590841 -7200
# Node ID 067533f8c41972079ba7e62f543f978aeb309806
# Parent  ac5da3e767b00dbb1b904e465d3b9d272cefa38e
Input positions.

diff -r ac5da3e767b0 -r 067533f8c419 src/Pure/Thy/position.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/position.ML	Tue May 19 17:14:01 1998 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Pure/Thy/position.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Input positions.
+*)
+
+signature POSITION =
+sig
+  eqtype T
+  val none: T
+  val line: int -> T
+  val name: string -> T
+  val line_name: int -> string -> T
+  val incr: T -> T
+  val str_of: T -> string
+end;
+
+structure Position: POSITION =
+struct
+
+
+(* datatype position *)
+
+datatype T =
+  Pos of int option * string option;
+
+val none = Pos (None, None);
+fun line n = Pos (Some n, None);
+fun name s = Pos (None, Some s);
+fun line_name n s = Pos (Some n, Some s);
+
+
+(* incr *)
+
+fun incr (pos as Pos (None, _)) = pos
+  | incr (Pos (Some n, opt_s)) = Pos (Some (n + 1), opt_s);
+
+
+(* str_of *)
+
+fun str_of (Pos (None, None)) = ""
+  | str_of (Pos (Some n, None)) = " (line " ^ string_of_int n ^ ")"
+  | str_of (Pos (None, Some s)) = " (" ^ s ^ ")"
+  | str_of (Pos (Some n, Some s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
+
+
+end;