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