src/Pure/Tools/server_commands.scala
author wenzelm
Thu, 15 Mar 2018 21:26:39 +0100
changeset 67869 8cb4fef58379
parent 67863 1805960b4a9f
child 67871 195ff117894c
permissions -rw-r--r--
support for "session_start";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/server_commands.scala
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     3
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     4
Miscellaneous Isabelle server commands.
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     5
*/
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     6
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     7
package isabelle
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     8
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
     9
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    10
object Server_Commands
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    11
{
67863
1805960b4a9f clarified default;
wenzelm
parents: 67862
diff changeset
    12
  def default_preferences: String = Options.read_prefs()
1805960b4a9f clarified default;
wenzelm
parents: 67862
diff changeset
    13
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    14
  object Session_Build
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    15
  {
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    16
    sealed case class Args(
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    17
      session: String,
67863
1805960b4a9f clarified default;
wenzelm
parents: 67862
diff changeset
    18
      preferences: String = default_preferences,
67862
wenzelm
parents: 67861
diff changeset
    19
      options: List[String] = Nil,
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    20
      dirs: List[String] = Nil,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    21
      ancestor_session: String = "",
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    22
      all_known: Boolean = false,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    23
      focus_session: Boolean = false,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    24
      required_session: Boolean = false,
67853
74e2a4b62826 more options;
wenzelm
parents: 67852
diff changeset
    25
      system_mode: Boolean = false,
74e2a4b62826 more options;
wenzelm
parents: 67852
diff changeset
    26
      verbose: Boolean = false)
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    27
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    28
    def unapply(json: JSON.T): Option[Args] =
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    29
      for {
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    30
        session <- JSON.string(json, "session")
67863
1805960b4a9f clarified default;
wenzelm
parents: 67862
diff changeset
    31
        preferences <- JSON.string_default(json, "preferences", default_preferences)
67862
wenzelm
parents: 67861
diff changeset
    32
        options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    33
        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    34
        ancestor_session <- JSON.string_default(json, "ancestor_session")
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    35
        all_known <- JSON.bool_default(json, "all_known")
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    36
        focus_session <- JSON.bool_default(json, "focus_session")
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    37
        required_session <- JSON.bool_default(json, "required_session")
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    38
        system_mode <- JSON.bool_default(json, "system_mode")
67853
74e2a4b62826 more options;
wenzelm
parents: 67852
diff changeset
    39
        verbose <- JSON.bool_default(json, "verbose")
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    40
      }
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    41
      yield {
67862
wenzelm
parents: 67861
diff changeset
    42
        Args(session, preferences = preferences, options = options, dirs = dirs,
wenzelm
parents: 67861
diff changeset
    43
          ancestor_session = ancestor_session, all_known = all_known, focus_session = focus_session,
wenzelm
parents: 67861
diff changeset
    44
          required_session = required_session, system_mode = system_mode, verbose = verbose)
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    45
      }
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    46
67861
cd1cac824ef8 asynchronous "session_build";
wenzelm
parents: 67858
diff changeset
    47
    def command(progress: Progress, args: Args)
cd1cac824ef8 asynchronous "session_build";
wenzelm
parents: 67858
diff changeset
    48
      : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    49
    {
67862
wenzelm
parents: 67861
diff changeset
    50
      val options = Options.init(prefs = args.preferences, opts = args.options)
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    51
      val dirs = args.dirs.map(Path.explode(_))
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    52
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    53
      val base_info =
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    54
        Sessions.base_info(options,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    55
          args.session,
67852
f701a1d5d852 allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
wenzelm
parents: 67850
diff changeset
    56
          progress = progress,
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    57
          dirs = dirs,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    58
          ancestor_session = proper_string(args.ancestor_session),
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    59
          all_known = args.all_known,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    60
          focus_session = args.focus_session,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    61
          required_session = args.required_session)
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    62
      val base = base_info.check_base
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    63
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    64
      val results =
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    65
        Build.build(options,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    66
          progress = progress,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    67
          build_heap = true,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    68
          system_mode = args.system_mode,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    69
          dirs = dirs,
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    70
          infos = base_info.infos,
67853
74e2a4b62826 more options;
wenzelm
parents: 67852
diff changeset
    71
          verbose = args.verbose,
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    72
          sessions = List(args.session))
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    73
67858
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    74
      val sessions_order =
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    75
        base_info.sessions_structure.imports_topological_order.zipWithIndex.
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    76
          toMap.withDefaultValue(-1)
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    77
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    78
      val results_json =
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    79
        JSON.Object(
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    80
          "return_code" -> results.rc,
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    81
          "sessions" ->
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    82
            results.sessions.toList.sortBy(sessions_order).map(session =>
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    83
              JSON.Object(
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    84
                "session" -> session,
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    85
                "return_code" -> results(session).rc,
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    86
                "timeout" -> results(session).timeout,
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    87
                "timing" -> results(session).timing.json)))
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    88
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    89
      if (results.ok) (results_json, results, base_info)
cba5c5657378 more informative JSON results;
wenzelm
parents: 67853
diff changeset
    90
      else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    91
    }
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
    92
  }
67869
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    93
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    94
  object Session_Start
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    95
  {
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    96
    sealed case class Args(
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    97
      build: Session_Build.Args,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    98
      print_mode: List[String] = Nil)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
    99
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   100
    def unapply(json: JSON.T): Option[Args] =
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   101
      for {
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   102
        build <- Session_Build.unapply(json)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   103
        print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   104
      }
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   105
      yield Args(build = build, print_mode = print_mode)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   106
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   107
    def command(progress: Progress, args: Args, log: Logger = No_Logger)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   108
      : (JSON.Object.T, String, Session) =
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   109
    {
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   110
      val base_info = Session_Build.command(progress, args.build)._3
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   111
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   112
      val session =
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   113
        Thy_Resources.start_session(
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   114
          base_info.options,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   115
          base_info.session,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   116
          session_dirs = base_info.dirs,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   117
          session_base = Some(base_info.check_base),
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   118
          print_mode = args.print_mode,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   119
          progress = progress,
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   120
          log = log)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   121
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   122
      val id = Library.UUID()
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   123
      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   124
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   125
      (res, id, session)
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   126
    }
8cb4fef58379 support for "session_start";
wenzelm
parents: 67863
diff changeset
   127
  }
67848
dd83610333de added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff changeset
   128
}