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