# HG changeset patch
# User wenzelm
# Date 1321117531 -3600
# Node ID 2046f8e2ecd782a44c884b38cad691601b28c64d
# Parent  489f27dcc0f44546f232d9647d71691350f79cd1
tuned markup -- prefer user-perspective;

diff -r 489f27dcc0f4 -r 2046f8e2ecd7 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Nov 12 17:53:48 2011 +0100
+++ b/src/Pure/variable.ML	Sat Nov 12 18:05:31 2011 +0100
@@ -297,7 +297,6 @@
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
-val markup_fixed = Name_Space.markup o fixes_space;
 
 fun lookup_fixed ctxt x =
   let val x' = intern_fixed ctxt x
@@ -308,6 +307,10 @@
     SOME x' => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
+fun markup_fixed ctxt x =
+  Name_Space.markup (fixes_space ctxt) x
+  |> Markup.name (revert_fixed ctxt x);
+
 fun dest_fixes ctxt =
   let val (space, tab) = fixes_of ctxt
   in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;