more message markup, provided by prover;
authorwenzelm
Mon Aug 05 15:48:13 2013 +0200 (2013-08-05)
changeset 52863acbced24e5fc
parent 52862 930ce8eacb87
child 52864 c2da0d3b974d
more message markup, provided by prover;
src/Pure/Tools/find_theorems.ML
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Aug 05 15:29:10 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 05 15:48:13 2013 +0200
     1.3 @@ -659,11 +659,16 @@
     1.4          print_fn = fn _ => fn state =>
     1.5            let
     1.6              val msg =
     1.7 -              Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query))
     1.8 -                handle exn =>
     1.9 -                  if Exn.is_interrupt exn then reraise exn
    1.10 -                  else ML_Compiler.exn_message exn;  (* FIXME error markup!? *)
    1.11 -          in Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)] msg end}
    1.12 +              XML.Elem ((Markup.writelnN, []),
    1.13 +                [XML.Text
    1.14 +                  (Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query)))])
    1.15 +              handle exn =>
    1.16 +                if Exn.is_interrupt exn then reraise exn
    1.17 +                else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
    1.18 +          in
    1.19 +            Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)]
    1.20 +              (YXML.string_of msg)
    1.21 +          end}
    1.22      | _ => NONE));
    1.23  
    1.24  end;
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:29:10 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 15:48:13 2013 +0200
     2.3 @@ -75,10 +75,11 @@
     2.4  
     2.5      val new_output =
     2.6        (for {
     2.7 -        (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- new_state.results.entries
     2.8 +        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
     2.9 +          new_state.results.entries
    2.10          if props.contains((Markup.KIND, FIND_THEOREMS))
    2.11          if props.contains((Markup.INSTANCE, instance))
    2.12 -      } yield XML.Elem(Markup(Markup.WRITELN_MESSAGE, Nil), body)).toList
    2.13 +      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
    2.14  
    2.15      if (new_output != current_output)
    2.16        pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))