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