# HG changeset patch
# User aspinall
# Date 1169476422 -3600
# Node ID ff4fc4ee9eb0bdd46990beaf9f33c28edb32b712
# Parent  e1d68715ed09d22d2d8ff96381afd39c1f6be081
Add line_of, name_of destructors.

diff -r e1d68715ed09 -r ff4fc4ee9eb0 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Jan 22 15:08:48 2007 +0100
+++ b/src/Pure/General/position.ML	Mon Jan 22 15:33:42 2007 +0100
@@ -14,6 +14,8 @@
   val line_name: int -> string -> T
   val inc: T -> T
   val str_of: T -> string
+  val line_of: T -> int option
+  val name_of: T -> string option
 end;
 
 structure Position: POSITION =
@@ -44,5 +46,10 @@
   | str_of (Pos (NONE, SOME s)) = " (" ^ s ^ ")"
   | str_of (Pos (SOME n, SOME s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
 
+fun line_of (Pos (SOME n,_)) = SOME n
+  | line_of _ = NONE
+
+fun name_of (Pos (_,SOME s)) = SOME s
+  | name_of _ = NONE
 
 end;