equal
deleted
inserted
replaced
13 object State_Panel |
13 object State_Panel |
14 { |
14 { |
15 private val make_id = Counter.make() |
15 private val make_id = Counter.make() |
16 private val instances = Synchronized(Map.empty[Counter.ID, State_Panel]) |
16 private val instances = Synchronized(Map.empty[Counter.ID, State_Panel]) |
17 |
17 |
18 def init(server: Server) |
18 def init(server: Language_Server) |
19 { |
19 { |
20 val instance = new State_Panel(server) |
20 val instance = new State_Panel(server) |
21 instances.change(_ + (instance.id -> instance)) |
21 instances.change(_ + (instance.id -> instance)) |
22 instance.init() |
22 instance.init() |
23 } |
23 } |
43 instances.value.get(id).foreach(state => |
43 instances.value.get(id).foreach(state => |
44 state.server.editor.send_dispatcher(state.auto_update(Some(enabled)))) |
44 state.server.editor.send_dispatcher(state.auto_update(Some(enabled)))) |
45 } |
45 } |
46 |
46 |
47 |
47 |
48 class State_Panel private(val server: Server) |
48 class State_Panel private(val server: Language_Server) |
49 { |
49 { |
50 /* output */ |
50 /* output */ |
51 |
51 |
52 val id: Counter.ID = State_Panel.make_id() |
52 val id: Counter.ID = State_Panel.make_id() |
53 |
53 |
54 private def output(content: String): Unit = |
54 private def output(content: String): Unit = |
55 server.channel.write(Protocol.State_Output(id, content)) |
55 server.channel.write(LSP.State_Output(id, content)) |
56 |
56 |
57 |
57 |
58 /* query operation */ |
58 /* query operation */ |
59 |
59 |
60 private val output_active = Synchronized(true) |
60 private val output_active = Synchronized(true) |