# HG changeset patch
# User wenzelm
# Date 1251903079 -7200
# Node ID 9d49a280f3f904daa8104baae4cfd00edc5d8dd1
# Parent  d5d8bea0cd94683533d6d6f6efbb297276eb9f05
eval/location_props: always produce YXML markup, independent of print_mode;

diff -r d5d8bea0cd94 -r 9d49a280f3f9 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 02 16:25:44 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 02 16:51:19 2009 +0200
@@ -74,8 +74,8 @@
     (* input *)
 
     val location_props =
-      Markup.markup (Markup.position |> Markup.properties
-          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) "";
+      op ^ (YXML.output_markup (Markup.position |> Markup.properties
+            (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
 
     val input = toks |> maps (fn tok =>
       let