# HG changeset patch
# User wenzelm
# Date 897472252 -7200
# Node ID 9101b70b696d2255dfbde3dc72fc257d496fd560
# Parent  05b152a419223478b84eced62e5a884d32069d19
moved Thy/position.ML to General/position.ML;

diff -r 05b152a41922 -r 9101b70b696d src/Pure/General/position.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/position.ML	Wed Jun 10 11:50:52 1998 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Pure/Thy/position.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Input positions.
+*)
+
+signature POSITION =
+sig
+  type T
+  val none: T
+  val line: int -> T
+  val name: string -> T
+  val line_name: int -> string -> T
+  val inc: 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);
+
+
+(* increment *)
+
+fun inc (pos as Pos (None, _)) = pos
+  | inc (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;
diff -r 05b152a41922 -r 9101b70b696d src/Pure/Thy/position.ML
--- a/src/Pure/Thy/position.ML	Wed Jun 10 11:50:20 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      Pure/Thy/position.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Input positions.
-*)
-
-signature POSITION =
-sig
-  type T
-  val none: T
-  val line: int -> T
-  val name: string -> T
-  val line_name: int -> string -> T
-  val inc: 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);
-
-
-(* increment *)
-
-fun inc (pos as Pos (None, _)) = pos
-  | inc (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;