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