src/Pure/Tools/server_commands.scala
author wenzelm
Sun May 13 16:26:01 2018 +0200 (13 months ago)
changeset 68167 327bb0f5f768
parent 68152 619de043389f
child 68365 f9379279f98c
permissions -rw-r--r--
clarified implicit compression;
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@68152
   159
      unicode_symbols: Boolean = false,
wenzelm@68152
   160
      export_pattern: String = "")
wenzelm@67883
   161
wenzelm@67883
   162
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67883
   163
      for {
wenzelm@67885
   164
        session_id <- JSON.uuid(json, "session_id")
wenzelm@67940
   165
        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
wenzelm@67883
   166
        master_dir <- JSON.string_default(json, "master_dir")
wenzelm@67897
   167
        pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
wenzelm@67897
   168
        unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
wenzelm@68152
   169
        export_pattern <- JSON.string_default(json, "export_pattern")
wenzelm@67883
   170
      }
wenzelm@67897
   171
      yield {
wenzelm@68152
   172
        Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
wenzelm@68152
   173
          unicode_symbols = unicode_symbols, export_pattern = export_pattern)
wenzelm@67897
   174
      }
wenzelm@67883
   175
wenzelm@67884
   176
    def command(args: Args,
wenzelm@67884
   177
      session: Thy_Resources.Session,
wenzelm@67885
   178
      id: UUID = UUID(),
wenzelm@67884
   179
      progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
wenzelm@67883
   180
    {
wenzelm@67883
   181
      val result =
wenzelm@67937
   182
        session.use_theories(args.theories, master_dir = args.master_dir,
wenzelm@67937
   183
          id = id, progress = progress)
wenzelm@67883
   184
wenzelm@67901
   185
      def output_text(s: String): String =
wenzelm@67901
   186
        if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
wenzelm@67897
   187
wenzelm@67897
   188
      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
wenzelm@67897
   189
      {
wenzelm@67897
   190
        val position = "pos" -> Position.JSON(pos)
wenzelm@67897
   191
        tree match {
wenzelm@67901
   192
          case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
wenzelm@67897
   193
          case elem: XML.Elem =>
wenzelm@67897
   194
            val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
wenzelm@67923
   195
            val kind =
wenzelm@67923
   196
              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
wenzelm@67931
   197
                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
wenzelm@67931
   198
            Server.Reply.message(output_text(msg), kind = kind) + position
wenzelm@67897
   199
        }
wenzelm@67897
   200
      }
wenzelm@67897
   201
wenzelm@67883
   202
      val result_json =
wenzelm@67883
   203
        JSON.Object(
wenzelm@67883
   204
          "ok" -> result.ok,
wenzelm@67900
   205
          "errors" ->
wenzelm@67900
   206
            (for {
wenzelm@67900
   207
              (name, status) <- result.nodes if !status.ok
wenzelm@67900
   208
              (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
wenzelm@67900
   209
            } yield output_message(tree, pos)),
wenzelm@67883
   210
          "nodes" ->
wenzelm@67900
   211
            (for ((name, status) <- result.nodes) yield
wenzelm@67943
   212
              name.json +
wenzelm@67943
   213
                ("status" -> status.json) +
wenzelm@67943
   214
                ("messages" ->
wenzelm@67947
   215
                  (for {
wenzelm@67947
   216
                    (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
wenzelm@68106
   217
                  } yield output_message(tree, pos))) +
wenzelm@68106
   218
                ("exports" ->
wenzelm@68152
   219
                  (if (args.export_pattern == "") Nil else {
wenzelm@68152
   220
                    val matcher = Export.make_matcher(args.export_pattern)
wenzelm@68152
   221
                    for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
wenzelm@68152
   222
                    yield {
wenzelm@68167
   223
                      val (base64, body) = entry.uncompressed().maybe_base64
wenzelm@68152
   224
                      JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
wenzelm@68152
   225
                    }
wenzelm@68152
   226
                  }))))
wenzelm@67883
   227
wenzelm@67883
   228
      (result_json, result)
wenzelm@67883
   229
    }
wenzelm@67883
   230
  }
wenzelm@67941
   231
wenzelm@67941
   232
  object Purge_Theories
wenzelm@67941
   233
  {
wenzelm@67941
   234
    sealed case class Args(
wenzelm@67941
   235
      session_id: UUID,
wenzelm@67941
   236
      theories: List[String] = Nil,
wenzelm@67941
   237
      master_dir: String = "",
wenzelm@67941
   238
      all: Boolean = false)
wenzelm@67941
   239
wenzelm@67941
   240
    def unapply(json: JSON.T): Option[Args] =
wenzelm@67941
   241
      for {
wenzelm@67941
   242
        session_id <- JSON.uuid(json, "session_id")
wenzelm@67941
   243
        theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _)
wenzelm@67941
   244
        master_dir <- JSON.string_default(json, "master_dir")
wenzelm@67941
   245
        all <- JSON.bool_default(json, "all")
wenzelm@67941
   246
      }
wenzelm@67941
   247
      yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
wenzelm@67941
   248
wenzelm@67941
   249
    def command(args: Args, session: Thy_Resources.Session)
wenzelm@67943
   250
      : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
wenzelm@67941
   251
    {
wenzelm@67943
   252
      val (purged, retained) =
wenzelm@67941
   253
        session.purge_theories(
wenzelm@67941
   254
          theories = args.theories, master_dir = args.master_dir, all = args.all)
wenzelm@67943
   255
wenzelm@67943
   256
      val result_json =
wenzelm@67943
   257
        JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
wenzelm@67943
   258
wenzelm@67943
   259
      (result_json, (purged, retained))
wenzelm@67941
   260
    }
wenzelm@67941
   261
  }
wenzelm@67848
   262
}