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