1/*  Title:      Pure/Tools/server_commands.scala
2    Author:     Makarius
3
4Miscellaneous Isabelle server commands.
5*/
6
7package isabelle
8
9
10object Server_Commands
11{
12  def default_preferences: String = Options.read_prefs()
13
14  object Cancel
15  {
16    sealed case class Args(task: UUID.T)
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      verbose: Boolean = false)
33
34    def unapply(json: JSON.T): Option[Args] =
35      for {
36        session <- JSON.string(json, "session")
37        preferences <- JSON.string_default(json, "preferences", default_preferences)
38        options <- JSON.strings_default(json, "options")
39        dirs <- JSON.strings_default(json, "dirs")
40        include_sessions <- JSON.strings_default(json, "include_sessions")
41        verbose <- JSON.bool_default(json, "verbose")
42      }
43      yield {
44        Args(session, preferences = preferences, options = options, dirs = dirs,
45          include_sessions = include_sessions, verbose = verbose)
46      }
47
48    def command(args: Args, progress: Progress = No_Progress)
49      : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
50    {
51      val options = Options.init(prefs = args.preferences, opts = args.options)
52      val dirs = args.dirs.map(Path.explode(_))
53
54      val base_info =
55        Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
56          include_sessions = args.include_sessions)
57      val base = base_info.check_base
58
59      val results =
60        Build.build(options,
61          progress = progress,
62          build_heap = true,
63          dirs = dirs,
64          infos = base_info.infos,
65          verbose = args.verbose,
66          sessions = List(args.session))
67
68      val sessions_order =
69        base_info.sessions_structure.imports_topological_order.zipWithIndex.
70          toMap.withDefaultValue(-1)
71
72      val results_json =
73        JSON.Object(
74          "ok" -> results.ok,
75          "return_code" -> results.rc,
76          "sessions" ->
77            results.sessions.toList.sortBy(sessions_order).map(session =>
78              {
79                val result = results(session)
80                JSON.Object(
81                  "session" -> session,
82                  "ok" -> result.ok,
83                  "return_code" -> result.rc,
84                  "timeout" -> result.timeout,
85                  "timing" -> result.timing.json)
86              }))
87
88      if (results.ok) (results_json, results, base_info)
89      else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
90    }
91  }
92
93  object Session_Start
94  {
95    sealed case class Args(
96      build: Session_Build.Args,
97      print_mode: List[String] = Nil)
98
99    def unapply(json: JSON.T): Option[Args] =
100      for {
101        build <- Session_Build.unapply(json)
102        print_mode <- JSON.strings_default(json, "print_mode")
103      }
104      yield Args(build = build, print_mode = print_mode)
105
106    def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
107      : (JSON.Object.T, (UUID.T, Headless.Session)) =
108    {
109      val base_info =
110        try { Session_Build.command(args.build, progress = progress)._3 }
111        catch { case exn: Server.Error => error(exn.message) }
112
113      val resources = Headless.Resources(base_info, log = log)
114
115      val session = resources.start_session(print_mode = args.print_mode, progress = progress)
116
117      val id = UUID.random()
118
119      val res =
120        JSON.Object(
121          "session_id" -> id.toString,
122          "tmp_dir" -> File.path(session.tmp_dir).implode)
123
124      (res, id -> session)
125    }
126  }
127
128  object Session_Stop
129  {
130    def unapply(json: JSON.T): Option[UUID.T] =
131      JSON.uuid(json, "session_id")
132
133    def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
134    {
135      val result = session.stop()
136      val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
137
138      if (result.ok) (result_json, result)
139      else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
140    }
141  }
142
143  object Use_Theories
144  {
145    sealed case class Args(
146      session_id: UUID.T,
147      theories: List[String],
148      master_dir: String = "",
149      pretty_margin: Double = Pretty.default_margin,
150      unicode_symbols: Boolean = false,
151      export_pattern: String = "",
152      check_delay: Option[Time] = None,
153      check_limit: Option[Int] = None,
154      watchdog_timeout: Option[Time] = None,
155      nodes_status_delay: Option[Time] = None,
156      commit_cleanup_delay: Option[Time] = None)
157
158    def unapply(json: JSON.T): Option[Args] =
159      for {
160        session_id <- JSON.uuid(json, "session_id")
161        theories <- JSON.strings(json, "theories")
162        master_dir <- JSON.string_default(json, "master_dir")
163        pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
164        unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
165        export_pattern <- JSON.string_default(json, "export_pattern")
166        check_delay = JSON.seconds(json, "check_delay")
167        check_limit = JSON.int(json, "check_limit")
168        watchdog_timeout = JSON.seconds(json, "watchdog_timeout")
169        nodes_status_delay = JSON.seconds(json, "nodes_status_delay")
170        commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay")
171      }
172      yield {
173        Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
174          unicode_symbols = unicode_symbols, export_pattern = export_pattern,
175          check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout,
176          nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay)
177      }
178
179    def command(args: Args,
180      session: Headless.Session,
181      id: UUID.T = UUID.random(),
182      progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
183    {
184      val result =
185        session.use_theories(args.theories, master_dir = args.master_dir,
186          check_delay = args.check_delay.getOrElse(session.default_check_delay),
187          check_limit = args.check_limit.getOrElse(session.default_check_limit),
188          watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),
189          nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay),
190          commit_cleanup_delay =
191            args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
192          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 =
205              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
206                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
207            Server.Reply.message(output_text(msg), kind = kind) + position
208        }
209      }
210
211      val result_json =
212        JSON.Object(
213          "ok" -> result.ok,
214          "errors" ->
215            (for {
216              (name, status) <- result.nodes if !status.ok
217              (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree)
218            } yield output_message(tree, pos)),
219          "nodes" ->
220            (for ((name, status) <- result.nodes) yield {
221              val snapshot = result.snapshot(name)
222              name.json +
223                ("status" -> status.json) +
224                ("messages" ->
225                  (for {
226                    (tree, pos) <- snapshot.messages if Protocol.is_exported(tree)
227                  } yield output_message(tree, pos))) +
228                ("exports" ->
229                  (if (args.export_pattern == "") Nil else {
230                    val matcher = Export.make_matcher(args.export_pattern)
231                    for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
232                    yield {
233                      val (base64, body) = entry.uncompressed().maybe_base64
234                      JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
235                    }
236                  }))
237            }))
238
239      (result_json, result)
240    }
241  }
242
243  object Purge_Theories
244  {
245    sealed case class Args(
246      session_id: UUID.T,
247      theories: List[String] = Nil,
248      master_dir: String = "",
249      all: Boolean = false)
250
251    def unapply(json: JSON.T): Option[Args] =
252      for {
253        session_id <- JSON.uuid(json, "session_id")
254        theories <- JSON.strings_default(json, "theories")
255        master_dir <- JSON.string_default(json, "master_dir")
256        all <- JSON.bool_default(json, "all")
257      }
258      yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
259
260    def command(args: Args, session: Headless.Session)
261      : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
262    {
263      val (purged, retained) =
264        session.purge_theories(
265          theories = args.theories, master_dir = args.master_dir, all = args.all)
266
267      val result_json =
268        JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
269
270      (result_json, (purged, retained))
271    }
272  }
273}
274