# HG changeset patch
# User wenzelm
# Date 1393788851 -3600
# Node ID 2982d233d798c348af37e31b5989f0b5f6992cdf
# Parent  ee71b2687c4bfa3c3efdc4a0865a2b95840599f1
consider completion report as part of error message -- less stateful, may get handled;

diff -r ee71b2687c4b -r 2982d233d798 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Sun Mar 02 20:20:20 2014 +0100
+++ b/src/Pure/General/completion.ML	Sun Mar 02 20:34:11 2014 +0100
@@ -9,6 +9,7 @@
   type T
   val names: Position.T -> (string * string) list -> T
   val none: T
+  val reported_text: T -> string
   val report: T -> unit
 end;
 
@@ -30,15 +31,17 @@
 
 val none = names Position.none [];
 
-fun report completion =
+fun reported_text completion =
   let val {pos, total, names} = dest completion in
     if Position.is_reported pos andalso not (null names) then
       let
         val markup = Position.markup pos Markup.completion;
         val body = (total, names) |>
           let open XML.Encode in pair int (list (pair string string)) end;
-      in Output.report (YXML.string_of (XML.Elem (markup, body))) end
-    else ()
+      in YXML.string_of (XML.Elem (markup, body)) end
+    else ""
   end;
 
+val report = Output.report o reported_text;
+
 end;
diff -r ee71b2687c4b -r 2982d233d798 src/Pure/General/name_space.ML
--- 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 =
diff -r ee71b2687c4b -r 2982d233d798 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 20:20:20 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 20:34:11 2014 +0100
@@ -382,8 +382,10 @@
     val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
     val name = Type.cert_class tsig (Type.intern_class tsig xname)
       handle TYPE (msg, _, _) =>
-       (Completion.report (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos));
-        error (msg ^ Position.here pos));
+        error (msg ^ Position.here pos ^
+          Markup.markup Markup.report
+            (Completion.reported_text
+              (Name_Space.completion (Context.Proof ctxt) class_space (xname, pos))));
     val _ = Context_Position.report ctxt pos (Name_Space.markup class_space name);
   in name end;