1/*  Title:      Tools/VSCode/src/dynamic_output.scala
2    Author:     Makarius
3
4Dynamic output, depending on caret focus: messages, state etc.
5*/
6
7package isabelle.vscode
8
9
10import isabelle._
11
12
13object Dynamic_Output
14{
15  sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil)
16  {
17    def handle_update(
18      resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =
19    {
20      val st1 =
21        resources.get_caret() match {
22          case None => copy(output = Nil)
23          case Some(caret) =>
24            val snapshot = caret.model.snapshot()
25            if (do_update && !snapshot.is_outdated) {
26              snapshot.current_command(caret.node_name, caret.offset) match {
27                case None => copy(output = Nil)
28                case Some(command) =>
29                  copy(output =
30                    if (!restriction.isDefined || restriction.get.contains(command))
31                      Rendering.output_messages(snapshot.command_results(command))
32                    else output)
33              }
34            }
35            else this
36        }
37      if (st1.output != output) {
38        channel.write(Protocol.Dynamic_Output(
39          resources.output_pretty_message(Pretty.separate(st1.output))))
40      }
41      st1
42    }
43  }
44
45  def apply(server: Server): Dynamic_Output = new Dynamic_Output(server)
46}
47
48
49class Dynamic_Output private(server: Server)
50{
51  private val state = Synchronized(Dynamic_Output.State())
52
53  private def handle_update(restriction: Option[Set[Command]])
54  { state.change(_.handle_update(server.resources, server.channel, restriction)) }
55
56
57  /* main */
58
59  private val main =
60    Session.Consumer[Any](getClass.getName) {
61      case changed: Session.Commands_Changed =>
62        handle_update(if (changed.assignment) None else Some(changed.commands))
63
64      case Session.Caret_Focus =>
65        handle_update(None)
66    }
67
68  def init()
69  {
70    server.session.commands_changed += main
71    server.session.caret_focus += main
72    handle_update(None)
73  }
74
75  def exit()
76  {
77    server.session.commands_changed -= main
78    server.session.caret_focus -= main
79  }
80}
81