added server command "session_build": similar to JEdit_Resources.session_build;
authorwenzelm
Tue Mar 13 19:34:42 2018 +0100 (2018-03-13)
changeset 67848dd83610333de
parent 67847 c61acb4855b6
child 67849 d4c8b2cf685f
added server command "session_build": similar to JEdit_Resources.session_build;
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Tools/server.scala	Tue Mar 13 18:40:25 2018 +0100
     1.2 +++ b/src/Pure/Tools/server.scala	Tue Mar 13 19:34:42 2018 +0100
     1.3 @@ -64,9 +64,13 @@
     1.4  
     1.5      private val table: Map[String, T] =
     1.6        Map(
     1.7 +        "help" -> { case (_, ()) => table.keySet.toList.sorted },
     1.8          "echo" -> { case (_, t) => t },
     1.9 -        "help" -> { case (_, ()) => table.keySet.toList.sorted },
    1.10 -        "shutdown" -> { case (context, ()) => context.shutdown(); () })
    1.11 +        "shutdown" -> { case (context, ()) => context.shutdown(); () },
    1.12 +        "session_build" ->
    1.13 +          { case (context, Server_Commands.Session_Build(args)) =>
    1.14 +             Server_Commands.Session_Build.command(context.progress(), args)._1
    1.15 +          })
    1.16  
    1.17      def unapply(name: String): Option[T] = table.get(name)
    1.18    }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Tue Mar 13 19:34:42 2018 +0100
     2.3 @@ -0,0 +1,70 @@
     2.4 +/*  Title:      Pure/Tools/server_commands.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Miscellaneous Isabelle server commands.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Server_Commands
    2.14 +{
    2.15 +  object Session_Build
    2.16 +  {
    2.17 +    sealed case class Args(
    2.18 +      session: String,
    2.19 +      prefs: String = "",
    2.20 +      opts: List[String] = Nil,
    2.21 +      dirs: List[String] = Nil,
    2.22 +      ancestor_session: String = "",
    2.23 +      all_known: Boolean = false,
    2.24 +      focus_session: Boolean = false,
    2.25 +      required_session: Boolean = false,
    2.26 +      system_mode: Boolean = false)
    2.27 +
    2.28 +    def unapply(json: JSON.T): Option[Args] =
    2.29 +      for {
    2.30 +        session <- JSON.string(json, "session")
    2.31 +        prefs <- JSON.string_default(json, "preferences")
    2.32 +        opts <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
    2.33 +        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
    2.34 +        ancestor_session <- JSON.string_default(json, "ancestor_session")
    2.35 +        all_known <- JSON.bool_default(json, "all_known")
    2.36 +        focus_session <- JSON.bool_default(json, "focus_session")
    2.37 +        required_session <- JSON.bool_default(json, "required_session")
    2.38 +        system_mode <- JSON.bool_default(json, "system_mode")
    2.39 +      }
    2.40 +      yield {
    2.41 +        Args(session, prefs = prefs, opts = opts, dirs = dirs, ancestor_session = ancestor_session,
    2.42 +          all_known = all_known, focus_session = focus_session, required_session = required_session,
    2.43 +          system_mode = system_mode)
    2.44 +      }
    2.45 +
    2.46 +    def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) =
    2.47 +    {
    2.48 +      val options = Options.init(prefs = args.prefs, opts = args.opts)
    2.49 +      val dirs = args.dirs.map(Path.explode(_))
    2.50 +
    2.51 +      val base_info =
    2.52 +        Sessions.base_info(options,
    2.53 +          args.session,
    2.54 +          dirs = dirs,
    2.55 +          ancestor_session = proper_string(args.ancestor_session),
    2.56 +          all_known = args.all_known,
    2.57 +          focus_session = args.focus_session,
    2.58 +          required_session = args.required_session)
    2.59 +      val base = base_info.check_base
    2.60 +
    2.61 +      val results =
    2.62 +        Build.build(options,
    2.63 +          progress = progress,
    2.64 +          build_heap = true,
    2.65 +          system_mode = args.system_mode,
    2.66 +          dirs = dirs,
    2.67 +          infos = base_info.infos,
    2.68 +          sessions = List(args.session))
    2.69 +
    2.70 +      (Map("rc" -> results.rc), base_info, results)
    2.71 +    }
    2.72 +  }
    2.73 +}
     3.1 --- a/src/Pure/build-jars	Tue Mar 13 18:40:25 2018 +0100
     3.2 +++ b/src/Pure/build-jars	Tue Mar 13 19:34:42 2018 +0100
     3.3 @@ -147,6 +147,7 @@
     3.4    Tools/print_operation.scala
     3.5    Tools/profiling_report.scala
     3.6    Tools/server.scala
     3.7 +  Tools/server_commands.scala
     3.8    Tools/simplifier_trace.scala
     3.9    Tools/spell_checker.scala
    3.10    Tools/task_statistics.scala