# HG changeset patch
# User wenzelm
# Date 1199311251 -3600
# Node ID c7125b591885161bef14e7b8f2cc5749296a6b7c
# Parent  a918133cd8a32048b0d0c2f3865e864c41125c81
of_properties: return filtered result;

diff -r a918133cd8a3 -r c7125b591885 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Jan 02 23:00:49 2008 +0100
+++ b/src/Pure/General/position.ML	Wed Jan 02 23:00:51 2008 +0100
@@ -15,7 +15,7 @@
   val line: int -> T
   val file: string -> T
   val path: Path.T -> T
-  val of_properties: Markup.property list -> T
+  val of_properties: Markup.property list -> T * Markup.property list
   val properties_of: T -> Markup.property list
   val str_of: T -> string
 end;
@@ -51,7 +51,8 @@
         SOME s => Int.fromString s
       | NONE => NONE);
     val opt_s = lookup Markup.fileN;
-  in Pos (opt_n, opt_s) end;
+    val ps' = filter_out (fn (x, _) => x = Markup.lineN orelse x = Markup.fileN) ps;
+  in (Pos (opt_n, opt_s), ps') end;
 
 fun properties_of (Pos (opt_n, opt_s)) =
   (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @