src/Pure/Tools/server_commands.scala
author wenzelm
Fri Mar 23 22:53:32 2018 +0100 (14 months ago)
changeset 67940 b4e80f062fbf
parent 67937 91eb307511bb
child 67941 49a34b2fa788
permissions -rw-r--r--
clarified signature -- eliminated somewhat pointless positions;
wenzelm@67848
     1
/*  Title:      Pure/Tools/server_commands.scala
wenzelm@67848
     2
    Author:     Makarius
wenzelm@67848
     3
wenzelm@67848
     4
Miscellaneous Isabelle server commands.
wenzelm@67848
     5
*/
wenzelm@67848
     6
wenzelm@67848
     7
package isabelle
wenzelm@67848
     8
wenzelm@67848
     9
wenzelm@67848
    10
object Server_Commands
wenzelm@67848
    11
{
wenzelm@67863
    12
  def default_preferences: String = Options.read_prefs()
wenzelm@67883
    13
wenzelm@67920
    14
  object Cancel
wenzelm@67920
    15
  {
wenzelm@67920
    16
    sealed case class Args(task: UUID)
wenzelm@67920
    17
wenzelm@67920
    18
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67920
    19
      for { task <- JSON.uuid(json, "task") }
wenzelm@67920
    20
      yield Args(task)
wenzelm@67920
    21
  }
wenzelm@67920
    22
wenzelm@67920
    23
wenzelm@67848
    24
  object Session_Build
wenzelm@67848
    25
  {
wenzelm@67848
    26
    sealed case class Args(
wenzelm@67848
    27
      session: String,
wenzelm@67863
    28
      preferences: String = default_preferences,
wenzelm@67862
    29
      options: List[String] = Nil,
wenzelm@67848
    30
      dirs: List[String] = Nil,
wenzelm@67922
    31
      include_sessions: List[String] = Nil,
wenzelm@67853
    32
      system_mode: Boolean = false,
wenzelm@67853
    33
      verbose: Boolean = false)
wenzelm@67848
    34
wenzelm@67848
    35
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67848
    36
      for {
wenzelm@67848
    37
        session <- JSON.string(json, "session")
wenzelm@67863
    38
        preferences <- JSON.string_default(json, "preferences", default_preferences)
wenzelm@67862
    39
        options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
wenzelm@67848
    40
        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
wenzelm@67922
    41
        include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
wenzelm@67848
    42
        system_mode <- JSON.bool_default(json, "system_mode")
wenzelm@67853
    43
        verbose <- JSON.bool_default(json, "verbose")
wenzelm@67848
    44
      }
wenzelm@67848
    45
      yield {
wenzelm@67862
    46
        Args(session, preferences = preferences, options = options, dirs = dirs,
wenzelm@67922
    47
          include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
wenzelm@67848
    48
      }
wenzelm@67848
    49
wenzelm@67886
    50
    def command(args: Args, progress: Progress = No_Progress)
wenzelm@67861
    51
      : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
wenzelm@67848
    52
    {
wenzelm@67862
    53
      val options = Options.init(prefs = args.preferences, opts = args.options)
wenzelm@67848
    54
      val dirs = args.dirs.map(Path.explode(_))
wenzelm@67848
    55
wenzelm@67848
    56
      val base_info =
wenzelm@67919
    57
        Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
wenzelm@67922
    58
          include_sessions = args.include_sessions)
wenzelm@67848
    59
      val base = base_info.check_base
wenzelm@67848
    60
wenzelm@67848
    61
      val results =
wenzelm@67848
    62
        Build.build(options,
wenzelm@67848
    63
          progress = progress,
wenzelm@67848
    64
          build_heap = true,
wenzelm@67848
    65
          system_mode = args.system_mode,
wenzelm@67848
    66
          dirs = dirs,
wenzelm@67848
    67
          infos = base_info.infos,
wenzelm@67853
    68
          verbose = args.verbose,
wenzelm@67848
    69
          sessions = List(args.session))
wenzelm@67848
    70
wenzelm@67858
    71
      val sessions_order =
wenzelm@67858
    72
        base_info.sessions_structure.imports_topological_order.zipWithIndex.
wenzelm@67858
    73
          toMap.withDefaultValue(-1)
wenzelm@67858
    74
wenzelm@67858
    75
      val results_json =
wenzelm@67858
    76
        JSON.Object(
wenzelm@67912
    77
          "ok" -> results.ok,
wenzelm@67858
    78
          "return_code" -> results.rc,
wenzelm@67858
    79
          "sessions" ->
wenzelm@67858
    80
            results.sessions.toList.sortBy(sessions_order).map(session =>
wenzelm@67912
    81
              {
wenzelm@67912
    82
                val result = results(session)
wenzelm@67912
    83
                JSON.Object(
wenzelm@67912
    84
                  "session" -> session,
wenzelm@67912
    85
                  "ok" -> result.ok,
wenzelm@67912
    86
                  "return_code" -> result.rc,
wenzelm@67912
    87
                  "timeout" -> result.timeout,
wenzelm@67912
    88
                  "timing" -> result.timing.json)
wenzelm@67912
    89
              }))
wenzelm@67858
    90
wenzelm@67858
    91
      if (results.ok) (results_json, results, base_info)
wenzelm@67858
    92
      else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
wenzelm@67848
    93
    }
wenzelm@67848
    94
  }
wenzelm@67869
    95
wenzelm@67869
    96
  object Session_Start
wenzelm@67869
    97
  {
wenzelm@67869
    98
    sealed case class Args(
wenzelm@67869
    99
      build: Session_Build.Args,
wenzelm@67869
   100
      print_mode: List[String] = Nil)
wenzelm@67869
   101
wenzelm@67869
   102
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67869
   103
      for {
wenzelm@67869
   104
        build <- Session_Build.unapply(json)
wenzelm@67869
   105
        print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _)
wenzelm@67869
   106
      }
wenzelm@67869
   107
      yield Args(build = build, print_mode = print_mode)
wenzelm@67869
   108
wenzelm@67886
   109
    def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
wenzelm@67885
   110
      : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
wenzelm@67869
   111
    {
wenzelm@67914
   112
      val base_info =
wenzelm@67914
   113
        try { Session_Build.command(args.build, progress = progress)._3 }
wenzelm@67914
   114
        catch { case exn: Server.Error => error(exn.message) }
wenzelm@67869
   115
wenzelm@67869
   116
      val session =
wenzelm@67869
   117
        Thy_Resources.start_session(
wenzelm@67869
   118
          base_info.options,
wenzelm@67869
   119
          base_info.session,
wenzelm@67869
   120
          session_dirs = base_info.dirs,
wenzelm@67869
   121
          session_base = Some(base_info.check_base),
wenzelm@67869
   122
          print_mode = args.print_mode,
wenzelm@67869
   123
          progress = progress,
wenzelm@67869
   124
          log = log)
wenzelm@67869
   125
wenzelm@67885
   126
      val id = UUID()
wenzelm@67869
   127
wenzelm@67925
   128
      val res =
wenzelm@67925
   129
        JSON.Object(
wenzelm@67925
   130
          "session_id" -> id.toString,
wenzelm@67925
   131
          "tmp_dir" -> File.path(session.tmp_dir).implode)
wenzelm@67925
   132
wenzelm@67925
   133
      (res, id -> session)
wenzelm@67871
   134
    }
wenzelm@67871
   135
  }
wenzelm@67871
   136
wenzelm@67871
   137
  object Session_Stop
wenzelm@67871
   138
  {
wenzelm@67885
   139
    def unapply(json: JSON.T): Option[UUID] =
wenzelm@67885
   140
      JSON.uuid(json, "session_id")
wenzelm@67871
   141
wenzelm@67878
   142
    def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
wenzelm@67871
   143
    {
wenzelm@67871
   144
      val result = session.stop()
wenzelm@67916
   145
      val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
wenzelm@67871
   146
wenzelm@67871
   147
      if (result.ok) (result_json, result)
wenzelm@67871
   148
      else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
wenzelm@67869
   149
    }
wenzelm@67869
   150
  }
wenzelm@67883
   151
wenzelm@67883
   152
  object Use_Theories
wenzelm@67883
   153
  {
wenzelm@67883
   154
    sealed case class Args(
wenzelm@67885
   155
      session_id: UUID,
wenzelm@67940
   156
      theories: List[String],
wenzelm@67897
   157
      master_dir: String = "",
wenzelm@67897
   158
      pretty_margin: Double = Pretty.default_margin,
wenzelm@67897
   159
      unicode_symbols: Boolean = false)
wenzelm@67883
   160
wenzelm@67883
   161
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67883
   162
      for {
wenzelm@67885
   163
        session_id <- JSON.uuid(json, "session_id")
wenzelm@67940
   164
        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
wenzelm@67883
   165
        master_dir <- JSON.string_default(json, "master_dir")
wenzelm@67897
   166
        pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
wenzelm@67897
   167
        unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
wenzelm@67883
   168
      }
wenzelm@67897
   169
      yield {
wenzelm@67937
   170
        Args(session_id, theories, master_dir = master_dir,
wenzelm@67897
   171
          pretty_margin = pretty_margin, unicode_symbols)
wenzelm@67897
   172
      }
wenzelm@67883
   173
wenzelm@67884
   174
    def command(args: Args,
wenzelm@67884
   175
      session: Thy_Resources.Session,
wenzelm@67885
   176
      id: UUID = UUID(),
wenzelm@67884
   177
      progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
wenzelm@67883
   178
    {
wenzelm@67883
   179
      val result =
wenzelm@67937
   180
        session.use_theories(args.theories, master_dir = args.master_dir,
wenzelm@67937
   181
          id = id, progress = progress)
wenzelm@67883
   182
wenzelm@67901
   183
      def output_text(s: String): String =
wenzelm@67901
   184
        if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
wenzelm@67897
   185
wenzelm@67897
   186
      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
wenzelm@67897
   187
      {
wenzelm@67897
   188
        val position = "pos" -> Position.JSON(pos)
wenzelm@67897
   189
        tree match {
wenzelm@67901
   190
          case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
wenzelm@67897
   191
          case elem: XML.Elem =>
wenzelm@67897
   192
            val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
wenzelm@67923
   193
            val kind =
wenzelm@67923
   194
              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
wenzelm@67931
   195
                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
wenzelm@67931
   196
            Server.Reply.message(output_text(msg), kind = kind) + position
wenzelm@67897
   197
        }
wenzelm@67897
   198
      }
wenzelm@67897
   199
wenzelm@67883
   200
      val result_json =
wenzelm@67883
   201
        JSON.Object(
wenzelm@67883
   202
          "ok" -> result.ok,
wenzelm@67900
   203
          "errors" ->
wenzelm@67900
   204
            (for {
wenzelm@67900
   205
              (name, status) <- result.nodes if !status.ok
wenzelm@67900
   206
              (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
wenzelm@67923
   207
              if Protocol.is_exported(tree)
wenzelm@67900
   208
            } yield output_message(tree, pos)),
wenzelm@67883
   209
          "nodes" ->
wenzelm@67900
   210
            (for ((name, status) <- result.nodes) yield
wenzelm@67897
   211
              JSON.Object(
wenzelm@67897
   212
                "node_name" -> name.node,
wenzelm@67897
   213
                "theory" -> name.theory,
wenzelm@67900
   214
                "status" -> status.json,
wenzelm@67897
   215
                "messages" ->
wenzelm@67900
   216
                  (for ((tree, pos) <- result.messages(name))
wenzelm@67900
   217
                    yield output_message(tree, pos)))))
wenzelm@67883
   218
wenzelm@67883
   219
      (result_json, result)
wenzelm@67883
   220
    }
wenzelm@67883
   221
  }
wenzelm@67848
   222
}