Quelle server_commands.scala Sprache: Scala

/*  Title:      Pure/Tools/server_commands.scala
    Author:     Makarius

Miscellaneous Isabelle server commands.
*/

package isabelle

object Server_Commands {
  def default_preferences: String = Options.read_prefs()

  object Help extends Server.Command("help") {
    override val command_body: Server.Command_Body =
      { case (context, ()) => context.command_list }
  }

  object Echo extends Server.Command("echo") {
    override val command_body: Server.Command_Body =
      { case (_, t) => t }
  }

  object Cancel extends Server.Command("cancel") {
    sealed case class Args(task: UUID.T)

    def unapply(json: JSON.T): Option[Args] =
      for { task <- JSON.uuid(json, "task") }
      yield Args(task)

    override val command_body: Server.Command_Body =
      { case (context, Cancel(args)) => context.cancel_task(args.task) }
  }

  object Shutdown extends Server.Command("shutdown") {
    override val command_body: Server.Command_Body =
      { case (context, ()) => context.server.shutdown() }
  }

  object Session_Build extends Server.Command("session_build") {
    sealed case class Args(
      session: String,
      preferences: String = default_preferences,
      options: List[String] = Nil,
      dirs: List[String] = Nil,
      include_sessions: List[String] = Nil)

    def unapply(json: JSON.T): Option[Args] =
      for {
        session <- JSON.string(json, "session")
        preferences <- JSON.string_default(json, "preferences", default_preferences)
        options <- JSON.strings_default(json, "options")
        dirs <- JSON.strings_default(json, "dirs")
        include_sessions <- JSON.strings_default(json, "include_sessions")
      }
      yield {
        Args(session, preferences = preferences, options = options, dirs = dirs,
          include_sessions = include_sessions)
      }

    def command(
      args: Args,
      progress: Progress = new Progress
    ) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
      val options =
        Options.init(prefs = args.preferences, specs = args.options.map(Options.Spec.make))
      val dirs = args.dirs.map(Path.explode)

      val session_background =
        Sessions.background(options, args.session, progress = progress, dirs = dirs,
          include_sessions = args.include_sessions).check_errors

      val results =
        Build.build(options,
          selection = Sessions.Selection.session(args.session),
          progress = progress,
          build_heap = true,
          dirs = dirs,
          infos = session_background.infos)

      val sessions_order =
        session_background.sessions_structure.imports_topological_order.zipWithIndex.
          toMap.withDefaultValue(-1)

      val results_json =
        JSON.Object(
          "ok" -> results.ok,
          "return_code" -> results.rc,
          "sessions" ->
            results.sessions.toList.sortBy(sessions_order).map { session =>
              val result = results(session)
              JSON.Object(
                "session" -> session,
                "ok" -> result.ok,
                "return_code" -> result.rc,
                "timeout" -> result.timeout,
                "timing" -> result.timing.json)
            })

      if (results.ok) (results_json, results, options, session_background)
      else {
        throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
          results_json)
      }
    }

    override val command_body: Server.Command_Body =
      { case (context, Session_Build(args)) =>
        context.make_task(task => Session_Build.command(args, progress = task.progress)._1) }
  }

  object Session_Start extends Server.Command("session_start") {
    sealed case class Args(
      build: Session_Build.Args,
      print_mode: List[String] = Nil)

    def unapply(json: JSON.T): Option[Args] =
      for {
        build <- Session_Build.unapply(json)
        print_mode <- JSON.strings_default(json, "print_mode")
      }
      yield Args(build = build, print_mode = print_mode)

    def command(
      args: Args,
      progress: Progress = new Progress,
      log: Logger = new Logger
    ) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
      val (_, _, options, session_background) =
        try { Session_Build.command(args.build, progress = progress) }
        catch { case exn: Server.Error => error(exn.message) }

      val resources = Headless.Resources(options, session_background, log = log)

      val session = resources.start_session(print_mode = args.print_mode, progress = progress)

      val id = UUID.random()

      val res =
        JSON.Object(
          "session_id" -> id.toString,
          "tmp_dir" -> session.tmp_dir_name)

      (res, id -> session)
    }

    override val command_body: Server.Command_Body =
      { case (context, Session_Start(args)) =>
          context.make_task { task =>
            val (res, entry) =
              Session_Start.command(args, progress = task.progress, log = context.server.log)
            context.server.add_session(entry)
            res
          }
      }
  }

  object Session_Stop extends Server.Command("session_stop") {
    def unapply(json: JSON.T): Option[UUID.T] =
      JSON.uuid(json, "session_id")

    def command(session: Headless.Session): (JSON.Object.T, Process_Result) = {
      val result = session.stop()
      val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)

      if (result.ok) (result_json, result)
      else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)
    }

    override val command_body: Server.Command_Body =
      { case (context, Session_Stop(id)) =>
        context.make_task(_ =>
        {
          val session = context.server.remove_session(id)
          Session_Stop.command(session)._1
        })
      }
  }

  object Use_Theories extends Server.Command("use_theories") {
    sealed case class Args(
      session_id: UUID.T,
      theories: List[String],
      master_dir: String = "",
      pretty_margin: Double = Pretty.default_margin,
      unicode_symbols: Boolean = false,
      export_pattern: String = "",
      check_delay: Option[Time] = None,
      check_limit: Option[Int] = None,
      watchdog_timeout: Option[Time] = None,
      nodes_status_delay: Option[Time] = None,
      commit_cleanup_delay: Option[Time] = None)

    def unapply(json: JSON.T): Option[Args] =
      for {
        session_id <- JSON.uuid(json, "session_id")
        theories <- JSON.strings(json, "theories")
        master_dir <- JSON.string_default(json, "master_dir")
        pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
        unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
        export_pattern <- JSON.string_default(json, "export_pattern")
        check_delay = JSON.seconds(json, "check_delay")
        check_limit = JSON.int(json, "check_limit")
        watchdog_timeout = JSON.seconds(json, "watchdog_timeout")
        nodes_status_delay = JSON.seconds(json, "nodes_status_delay")
        commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay")
      }
      yield {
        Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
          unicode_symbols = unicode_symbols, export_pattern = export_pattern,
          check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
          nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
      }

    def command(args: Args,
      session: Headless.Session,
      id: UUID.T = UUID.random(),
      progress: Progress = new Progress
    ): (JSON.Object.T, Headless.Use_Theories_Result) = {
      val result =
        session.use_theories(args.theories, master_dir = args.master_dir,
          check_delay = args.check_delay.getOrElse(session.default_check_delay),
          check_limit = args.check_limit.getOrElse(session.default_check_limit),
          watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),
          nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay),
          commit_cleanup_delay =
            args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
          id = id, progress = progress)

      def output_text(text: String): String =
        Symbol.output(args.unicode_symbols, text)

      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = {
        val position = "pos" -> Position.JSON(pos)
        tree match {
          case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
          case elem: XML.Elem =>
            val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
            val kind =
              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
            Server.Reply.message(output_text(msg), kind = kind) + position
        }
      }

      def show_message(tree: XML.Tree): Boolean =
        Protocol.is_exported(tree) || session.show_states && Protocol.is_state(tree)

      val result_json =
        JSON.Object(
          "ok" -> result.ok,
          "errors" ->
            (for {
              (name, status) <- result.nodes if !status.ok
              (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree)
            } yield output_message(tree, pos)),
          "nodes" ->
            (for ((name, status) <- result.nodes) yield {
              val snapshot = result.snapshot(name)
              name.json +
                ("status" -> status.json) +
                ("messages" ->
                  (for {
                    (tree, pos) <- snapshot.messages if show_message(tree)
                  } yield output_message(tree, pos))) +
                ("exports" ->
                  (if (args.export_pattern == "") Nil else {
                    val matcher = Export.make_matcher(List(args.export_pattern))
                    for { entry <- snapshot.exports if matcher(entry.entry_name) }
                    yield {
                      val (base64, body) = entry.bytes.maybe_encode_base64
                      JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
                    }
                  }))
            }))

      (result_json, result)
    }

    override val command_body: Server.Command_Body =
      { case (context, Use_Theories(args)) =>
          context.make_task { task =>
            val session = context.server.the_session(args.session_id)
            Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
          }
      }
  }

  object Purge_Theories extends Server.Command("purge_theories") {
    sealed case class Args(
      session_id: UUID.T,
      theories: List[String] = Nil,
      master_dir: String = "",
      all: Boolean = false)

    def unapply(json: JSON.T): Option[Args] =
      for {
        session_id <- JSON.uuid(json, "session_id")
        theories <- JSON.strings_default(json, "theories")
        master_dir <- JSON.string_default(json, "master_dir")
        all <- JSON.bool_default(json, "all")
      }
      yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }

    def command(
      args: Args,
      session: Headless.Session
    ) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = {
      val (purged, retained) =
        session.purge_theories(
          theories = args.theories, master_dir = args.master_dir, all = args.all)

      val result_json =
        JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))

      (result_json, (purged, retained))
    }

    override val command_body: Server.Command_Body =
      { case (context, Purge_Theories(args)) =>
          val session = context.server.the_session(args.session_id)
          command(args, session)._1
      }
  }
}

class Server_Commands extends Server.Commands(
  Server_Commands.Help,
  Server_Commands.Echo,
  Server_Commands.Cancel,
  Server_Commands.Shutdown,
  Server_Commands.Session_Build,
  Server_Commands.Session_Start,
  Server_Commands.Session_Stop,
  Server_Commands.Use_Theories,
  Server_Commands.Purge_Theories)

quality97%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.