of_properties: observe Markup.position_properties';
authorwenzelm
Wed, 06 Aug 2008 00:10:13 +0200
changeset 27749 24f2b57a34ea
parent 27748 c421ee0d2350
child 27750 7f5fb39c6362
of_properties: observe Markup.position_properties';
src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Aug 06 00:10:08 2008 +0200
+++ b/src/Pure/General/position.ML	Wed Aug 06 00:10:13 2008 +0200
@@ -81,7 +81,7 @@
         NONE => NONE
       | SOME m => SOME (m, the_default 1 (get_int props Markup.columnN)));
     fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
-  in (Pos (count, property Markup.fileN @ property Markup.idN)) end;
+  in Pos (count, maps property Markup.position_properties') end;
 
 fun properties_of (Pos (count, props)) =
   (case count of