more explicit errors;
authorwenzelm
Sun Mar 18 11:42:57 2018 +0100 (14 months ago)
changeset 679005a1b0076d7f0
parent 67899 730fa992da38
child 67901 3e6864cf387f
more explicit errors;
tuned;
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Tools/server_commands.scala	Sat Mar 17 18:51:56 2018 +1100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Sun Mar 18 11:42:57 2018 +0100
     1.3 @@ -206,14 +206,20 @@
     1.4        val result_json =
     1.5          JSON.Object(
     1.6            "ok" -> result.ok,
     1.7 +          "errors" ->
     1.8 +            (for {
     1.9 +              (name, status) <- result.nodes if !status.ok
    1.10 +              (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
    1.11 +            } yield output_message(tree, pos)),
    1.12            "nodes" ->
    1.13 -            (for ((name, st) <- result.nodes) yield
    1.14 +            (for ((name, status) <- result.nodes) yield
    1.15                JSON.Object(
    1.16                  "node_name" -> name.node,
    1.17                  "theory" -> name.theory,
    1.18 -                "status" -> st.json,
    1.19 +                "status" -> status.json,
    1.20                  "messages" ->
    1.21 -                  (for ((tree, pos) <- result.messages(name)) yield output_message(tree, pos)))))
    1.22 +                  (for ((tree, pos) <- result.messages(name))
    1.23 +                    yield output_message(tree, pos)))))
    1.24  
    1.25        (result_json, result)
    1.26      }