# HG changeset patch
# User wenzelm
# Date 1375710493 -7200
# Node ID acbced24e5fc968451d2fa953c8775c7862795ff
# Parent  930ce8eacb87b319e6c2aece86f2e8503b2c81b2
more message markup, provided by prover;

diff -r 930ce8eacb87 -r acbced24e5fc src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Aug 05 15:29:10 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 05 15:48:13 2013 +0200
@@ -659,11 +659,16 @@
         print_fn = fn _ => fn state =>
           let
             val msg =
-              Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
-                handle exn =>
-                  if Exn.is_interrupt exn then reraise exn
-                  else ML_Compiler.exn_message exn;  (* FIXME error markup!? *)
-          in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
+              XML.Elem ((Markup.writelnN, []),
+                [XML.Text
+                  (Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query)))])
+              handle exn =>
+                if Exn.is_interrupt exn then reraise exn
+                else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
+          in
+            Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)]
+              (YXML.string_of msg)
+          end}
     | _ => NONE));
 
 end;
diff -r 930ce8eacb87 -r acbced24e5fc src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:29:10 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:48:13 2013 +0200
@@ -75,10 +75,11 @@
 
     val new_output =
       (for {
-        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries
+        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
+          new_state.results.entries
         if props.contains((Markup.KIND, FIND_THEOREMS))
         if props.contains((Markup.INSTANCE, instance))
-      } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList
+      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))