# HG changeset patch # User wenzelm # Date 1520966082 -3600 # Node ID dd83610333de1c57a629e9378f6816c62d045330 # Parent c61acb4855b68ae766ae27145f07b32f963fe425 added server command "session_build": similar to JEdit_Resources.session_build; diff -r c61acb4855b6 -r dd83610333de src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Tue Mar 13 18:40:25 2018 +0100 +++ b/src/Pure/Tools/server.scala Tue Mar 13 19:34:42 2018 +0100 @@ -64,9 +64,13 @@ private val table: Map[String, T] = Map( + "help" -> { case (_, ()) => table.keySet.toList.sorted }, "echo" -> { case (_, t) => t }, - "help" -> { case (_, ()) => table.keySet.toList.sorted }, - "shutdown" -> { case (context, ()) => context.shutdown(); () }) + "shutdown" -> { case (context, ()) => context.shutdown(); () }, + "session_build" -> + { case (context, Server_Commands.Session_Build(args)) => + Server_Commands.Session_Build.command(context.progress(), args)._1 + }) def unapply(name: String): Option[T] = table.get(name) } diff -r c61acb4855b6 -r dd83610333de src/Pure/Tools/server_commands.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/server_commands.scala Tue Mar 13 19:34:42 2018 +0100 @@ -0,0 +1,70 @@ +/* Title: Pure/Tools/server_commands.scala + Author: Makarius + +Miscellaneous Isabelle server commands. +*/ + +package isabelle + + +object Server_Commands +{ + object Session_Build + { + sealed case class Args( + session: String, + prefs: String = "", + opts: List[String] = Nil, + dirs: List[String] = Nil, + ancestor_session: String = "", + all_known: Boolean = false, + focus_session: Boolean = false, + required_session: Boolean = false, + system_mode: Boolean = false) + + def unapply(json: JSON.T): Option[Args] = + for { + session <- JSON.string(json, "session") + prefs <- JSON.string_default(json, "preferences") + opts <- JSON.list_default(json, "options", JSON.Value.String.unapply _) + dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _) + ancestor_session <- JSON.string_default(json, "ancestor_session") + all_known <- JSON.bool_default(json, "all_known") + focus_session <- JSON.bool_default(json, "focus_session") + required_session <- JSON.bool_default(json, "required_session") + system_mode <- JSON.bool_default(json, "system_mode") + } + yield { + Args(session, prefs = prefs, opts = opts, dirs = dirs, ancestor_session = ancestor_session, + all_known = all_known, focus_session = focus_session, required_session = required_session, + system_mode = system_mode) + } + + def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) = + { + val options = Options.init(prefs = args.prefs, opts = args.opts) + val dirs = args.dirs.map(Path.explode(_)) + + val base_info = + Sessions.base_info(options, + args.session, + dirs = dirs, + ancestor_session = proper_string(args.ancestor_session), + all_known = args.all_known, + focus_session = args.focus_session, + required_session = args.required_session) + val base = base_info.check_base + + val results = + Build.build(options, + progress = progress, + build_heap = true, + system_mode = args.system_mode, + dirs = dirs, + infos = base_info.infos, + sessions = List(args.session)) + + (Map("rc" -> results.rc), base_info, results) + } + } +} diff -r c61acb4855b6 -r dd83610333de src/Pure/build-jars --- a/src/Pure/build-jars Tue Mar 13 18:40:25 2018 +0100 +++ b/src/Pure/build-jars Tue Mar 13 19:34:42 2018 +0100 @@ -147,6 +147,7 @@ Tools/print_operation.scala Tools/profiling_report.scala Tools/server.scala + Tools/server_commands.scala Tools/simplifier_trace.scala Tools/spell_checker.scala Tools/task_statistics.scala