output result messages;
authorwenzelm
Sat Mar 17 20:49:28 2018 +0100 (14 months ago)
changeset 67897a5b9d1f51b04
parent 67896 00797fb82869
child 67898 736673784fac
output result messages;
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 20:35:23 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 20:49:28 2018 +0100
     1.3 @@ -56,6 +56,17 @@
     1.4      val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
     1.5    {
     1.6      def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
     1.7 +
     1.8 +    def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
     1.9 +    {
    1.10 +      val node = version.nodes(node_name)
    1.11 +      (for {
    1.12 +        (command, start) <-
    1.13 +          Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
    1.14 +        pos = command.span.keyword_pos(start).position(command.span.name)
    1.15 +        (_, tree) <- state.command_results(version, command).iterator
    1.16 +       } yield (tree, pos)).toList
    1.17 +    }
    1.18    }
    1.19  
    1.20    class Session private[Thy_Resources](
     2.1 --- a/src/Pure/Tools/server_commands.scala	Sat Mar 17 20:35:23 2018 +0100
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Mar 17 20:49:28 2018 +0100
     2.3 @@ -159,7 +159,9 @@
     2.4        session_id: UUID,
     2.5        theories: List[(String, Position.T)],
     2.6        qualifier: String = default_qualifier,
     2.7 -      master_dir: String = "")
     2.8 +      master_dir: String = "",
     2.9 +      pretty_margin: Double = Pretty.default_margin,
    2.10 +      unicode_symbols: Boolean = false)
    2.11  
    2.12      def unapply(json: JSON.T): Option[Args] =
    2.13        for {
    2.14 @@ -167,8 +169,13 @@
    2.15          theories <- JSON.list(json, "theories", unapply_name_pos _)
    2.16          qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
    2.17          master_dir <- JSON.string_default(json, "master_dir")
    2.18 +        pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    2.19 +        unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    2.20        }
    2.21 -      yield Args(session_id, theories, qualifier = qualifier, master_dir = master_dir)
    2.22 +      yield {
    2.23 +        Args(session_id, theories, qualifier = qualifier, master_dir = master_dir,
    2.24 +          pretty_margin = pretty_margin, unicode_symbols)
    2.25 +      }
    2.26  
    2.27      def command(args: Args,
    2.28        session: Thy_Resources.Session,
    2.29 @@ -179,12 +186,34 @@
    2.30          session.use_theories(args.theories, qualifier = args.qualifier,
    2.31            master_dir = args.master_dir, id = id, progress = progress)
    2.32  
    2.33 +      def output_text(s: String): JSON.Object.Entry =
    2.34 +        Server.Reply.message(if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s))
    2.35 +
    2.36 +      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
    2.37 +      {
    2.38 +        val position = "pos" -> Position.JSON(pos)
    2.39 +        tree match {
    2.40 +          case XML.Text(msg) => JSON.Object(output_text(msg), position)
    2.41 +          case elem: XML.Elem =>
    2.42 +            val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
    2.43 +            Markup.messages.collectFirst({ case (a, b) if b == elem.name => a }) match {
    2.44 +              case None => JSON.Object(output_text(msg), position)
    2.45 +              case Some(kind) => JSON.Object(Markup.KIND -> kind, output_text(msg), position)
    2.46 +            }
    2.47 +        }
    2.48 +      }
    2.49 +
    2.50        val result_json =
    2.51          JSON.Object(
    2.52            "ok" -> result.ok,
    2.53            "nodes" ->
    2.54              (for ((name, st) <- result.nodes) yield
    2.55 -              JSON.Object("node_name" -> name.node, "theory" -> name.theory, "status" -> st.json)))
    2.56 +              JSON.Object(
    2.57 +                "node_name" -> name.node,
    2.58 +                "theory" -> name.theory,
    2.59 +                "status" -> st.json,
    2.60 +                "messages" ->
    2.61 +                  (for ((tree, pos) <- result.messages(name)) yield output_message(tree, pos)))))
    2.62  
    2.63        (result_json, result)
    2.64      }