--- a/src/Pure/General/name_space.ML Sun Mar 02 20:20:20 2014 +0100
+++ b/src/Pure/General/name_space.ML Sun Mar 02 20:34:11 2014 +0100
@@ -451,8 +451,9 @@
(Context_Position.report_generic context pos (markup space name);
(name, x))
| NONE =>
- (Completion.report (completion context space (xname, pos));
- error (undefined (kind_of space) name ^ Position.here pos)))
+ error (undefined (kind_of space) name ^ Position.here pos ^
+ Markup.markup Markup.report
+ (Completion.reported_text (completion context space (xname, pos)))))
end;
fun get (space, tab) name =