# HG changeset patch # User wenzelm # Date 1489270375 -3600 # Node ID 4c9c83311cad0c27c0de74bc09a4861f4cbb2707 # Parent 0dd2ad9dbfc2ac32ffa1e093b6a5634371ebfeaf dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala); diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Pure/build-jars --- a/src/Pure/build-jars Sat Mar 11 22:19:22 2017 +0100 +++ b/src/Pure/build-jars Sat Mar 11 23:12:55 2017 +0100 @@ -164,6 +164,7 @@ ../Tools/VSCode/src/build_vscode.scala ../Tools/VSCode/src/channel.scala ../Tools/VSCode/src/document_model.scala + ../Tools/VSCode/src/dynamic_output.scala ../Tools/VSCode/src/grammar.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Sat Mar 11 22:19:22 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Sat Mar 11 23:12:55 2017 +0100 @@ -37,8 +37,6 @@ const dynamic_output_type = new NotificationType("PIDE/dynamic_output") let last_caret_update: Caret_Update = {} -let dynamic_output: string = "" - /* activate extension */ @@ -77,6 +75,11 @@ /* caret handling and dynamic output */ + const dynamic_output = vscode.window.createOutputChannel("Isabelle Output") + context.subscriptions.push(dynamic_output) + dynamic_output.show(true) + dynamic_output.hide() + function update_caret() { const editor = vscode.window.activeTextEditor @@ -95,7 +98,13 @@ client.onReady().then(() => { - client.onNotification(dynamic_output_type, body => { dynamic_output = body }) + client.onNotification(dynamic_output_type, + body => { + if (body) { + dynamic_output.clear() + dynamic_output.appendLine(body) + } + }) vscode.window.onDidChangeActiveTextEditor(_ => update_caret()) vscode.window.onDidChangeTextEditorSelection(_ => update_caret()) update_caret() diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sat Mar 11 22:19:22 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sat Mar 11 23:12:55 2017 +0100 @@ -158,6 +158,24 @@ } + /* current command */ + + def current_command(snapshot: Document.Snapshot, current_offset: Text.Offset): Option[Command] = + { + if (is_theory) { + val node = snapshot.version.nodes(node_name) + val caret = snapshot.revert(current_offset) + val caret_command_iterator = node.command_iterator(caret) + if (caret_command_iterator.hasNext) { + val (cmd0, _) = caret_command_iterator.next + node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored) + } + else None + } + else snapshot.version.nodes.commands_loading(node_name).headOption + } + + /* prover session */ def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] @@ -165,5 +183,7 @@ def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) - def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources) + def rendering(snapshot: Document.Snapshot): VSCode_Rendering = + new VSCode_Rendering(this, snapshot, resources) + def rendering(): VSCode_Rendering = rendering(snapshot()) } diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Tools/VSCode/src/dynamic_output.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/dynamic_output.scala Sat Mar 11 23:12:55 2017 +0100 @@ -0,0 +1,88 @@ +/* Title: Tools/VSCode/src/dynamic_output.scala + Author: Makarius + +Dynamic output, depending on caret focus: messages, state etc. +*/ + +package isabelle.vscode + + +import isabelle._ + + +object Dynamic_Output +{ + case class State( + do_update: Boolean = true, + snapshot: Document.Snapshot = Document.Snapshot.init, + command: Command = Command.empty, + results: Command.Results = Command.Results.empty, + output: List[XML.Tree] = Nil) + + def apply(server: Server): Dynamic_Output = new Dynamic_Output(server) +} + + +class Dynamic_Output private(server: Server) +{ + private val state = Synchronized(Dynamic_Output.State()) + + private def handle_update(restriction: Option[Set[Command]]) + { + state.change(st => + { + val resources = server.resources + def init_st = Dynamic_Output.State(st.do_update) + val st1 = + resources.caret_range() match { + case None => init_st + case Some((model, caret_range)) => + val snapshot = model.snapshot() + if (st.do_update && !snapshot.is_outdated) { + model.current_command(snapshot, caret_range.start) match { + case None => init_st + case Some(command) => + val results = snapshot.state.command_results(snapshot.version, command) + val output = + if (!restriction.isDefined || restriction.get.contains(command)) + Rendering.output_messages(results) + else st.output + st.copy( + snapshot = snapshot, command = command, results = results, output = output) + } + } + else st + } + if (st1.output != st.output) { + server.channel.write(Protocol.Dynamic_Output( + resources.output_pretty_message(Pretty.separate(st1.output)))) + } + st1 + }) + } + + + /* main */ + + private val main = + Session.Consumer[Any](getClass.getName) { + case changed: Session.Commands_Changed => + handle_update(if (changed.assignment) None else Some(changed.commands)) + + case Session.Caret_Focus => + handle_update(None) + } + + def init() + { + server.session.commands_changed += main + server.session.caret_focus += main + handle_update(None) + } + + def exit() + { + server.session.commands_changed -= main + server.session.caret_focus -= main + } +} diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sat Mar 11 22:19:22 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Mar 11 23:12:55 2017 +0100 @@ -87,7 +87,7 @@ } class Server( - channel: Channel, + val channel: Channel, options: Options, text_length: Text.Length = Text.Length.encoding(Server.default_text_length), session_name: String = Server.default_logic, @@ -109,6 +109,8 @@ offset <- model.content.doc.offset(node_pos.pos) } yield (rendering, offset) + private val dynamic_output = Dynamic_Output(this) + /* input from client or file-system */ @@ -238,6 +240,8 @@ catch { case ERROR(msg) => reply(msg); None } for (session <- try_session) { + session_.change(_ => Some(session)) + var session_phase: Session.Consumer[Session.Phase] = null session_phase = Session.Consumer(getClass.getName) { @@ -255,11 +259,11 @@ session.commands_changed += prover_output session.all_messages += syslog + dynamic_output.init() + session.start(receiver => Isabelle_Process(options = options, logic = session_name, dirs = session_dirs, modes = modes, receiver = receiver)) - - session_.change(_ => Some(session)) } } @@ -269,6 +273,7 @@ session_.change({ case Some(session) => + dynamic_output.exit() var session_phase: Session.Consumer[Session.Phase] = null session_phase = Session.Consumer(getClass.getName) { diff -r 0dd2ad9dbfc2 -r 4c9c83311cad src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sat Mar 11 22:19:22 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Mar 11 23:12:55 2017 +0100 @@ -277,17 +277,19 @@ /* caret handling */ - def update_caret(new_caret: Option[(JFile, Line.Position)]) - { state.change(_.copy(caret = new_caret)) } + def update_caret(caret: Option[(JFile, Line.Position)]) + { state.change(_.copy(caret = caret)) } - def caret_position: Option[(Document_Model, Line.Position)] = + def caret_range(): Option[(Document_Model, Text.Range)] = { val st = state.value for { (file, pos) <- st.caret model <- st.models.get(file) + offset <- model.content.doc.offset(pos) + if offset < model.content.doc.text_range.stop } - yield (model, pos) + yield (model, Text.Range(offset, offset + 1)) }