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