# HG changeset patch # User wenzelm # Date 1496244326 -7200 # Node ID d8c5603c17327dcade187da07f96520def713594 # Parent 5b8fafde7d64526b27a5fbb1e1274f311c439239 explicit preview request/response; commands, icons, menus like VSCode markdown preview; clarified Uri information (again); tuned; diff -r 5b8fafde7d64 -r d8c5603c1732 src/Pure/build-jars --- a/src/Pure/build-jars Wed May 31 11:49:29 2017 +0200 +++ b/src/Pure/build-jars Wed May 31 17:25:26 2017 +0200 @@ -167,8 +167,8 @@ ../Tools/VSCode/src/channel.scala ../Tools/VSCode/src/document_model.scala ../Tools/VSCode/src/dynamic_output.scala - ../Tools/VSCode/src/dynamic_preview.scala ../Tools/VSCode/src/grammar.scala + ../Tools/VSCode/src/preview.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala ../Tools/VSCode/src/vscode_rendering.scala diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/Preview.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/Preview.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,1 @@ + \ No newline at end of file diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/PreviewOnRightPane_16x.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/PreviewOnRightPane_16x.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/PreviewOnRightPane_16x_dark.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/PreviewOnRightPane_16x_dark.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/Preview_inverse.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/Preview_inverse.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,1 @@ + \ No newline at end of file diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/ViewSource.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/ViewSource.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,3 @@ + +]> \ No newline at end of file diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/media/ViewSource_inverse.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/media/ViewSource_inverse.svg Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,1 @@ + \ No newline at end of file diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Wed May 31 17:25:26 2017 +0200 @@ -18,16 +18,64 @@ "categories": ["Languages"], "activationEvents": [ "onLanguage:isabelle", - "onLanguage:isabelle-ml" + "onLanguage:isabelle-ml", + "onCommand:isabelle.preview", + "onCommand:isabelle.preview-side", + "onCommand:isabelle.preview-source" ], "main": "./out/src/extension", "contributes": { "commands": [ { - "command": "isabelle.preview", - "title": "Isabelle Document Preview" + "command": "isabelle.preview", + "title": "Open Preview", + "category": "Isabelle", + "icon": { + "light": "./media/Preview.svg", + "dark": "./media/Preview_inverse.svg" + } + }, + { + "command": "isabelle.preview-side", + "title": "Open Preview to the Side", + "category": "Isabelle", + "icon": { + "light": "./media/PreviewOnRightPane_16x.svg", + "dark": "./media/PreviewOnRightPane_16x_dark.svg" + } + }, + { + "command": "isabelle.preview-source", + "title": "Show Source", + "category": "Isabelle", + "icon": { + "light": "./media/ViewSource.svg", + "dark": "./media/ViewSource_inverse.svg" + } } ], + "menus": { + "editor/title": [ + { + "when": "editorLangId == isabelle", + "command": "isabelle.preview-side", + "alt": "isabelle.preview", + "group": "navigation" + }, + { + "when": "resourceScheme == isabelle-preview", + "command": "isabelle.preview-source", + "group": "navigation" + } + ], + "explorer/context": [ + { + "when": "resourceLangId == isabelle", + "command": "isabelle.preview", + "group": "navigation" + } + ] + }, "languages": [ { "id": "isabelle", diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Wed May 31 17:25:26 2017 +0200 @@ -36,11 +36,12 @@ args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } : { command: isabelle_tool, args: ["vscode_server"].concat(standard_args, isabelle_args) }; - const client_options: LanguageClientOptions = { + const language_client_options: LanguageClientOptions = { documentSelector: ["isabelle", "isabelle-ml", "bibtex"] }; - const client = new LanguageClient("Isabelle", server_options, client_options, false) + const language_client = + new LanguageClient("Isabelle", server_options, language_client_options, false) /* decorations */ @@ -52,8 +53,8 @@ window.onDidChangeActiveTextEditor(decorations.update_editor), workspace.onDidCloseTextDocument(decorations.close_document)) - client.onReady().then(() => - client.onNotification(protocol.decoration_type, decorations.apply_decoration)) + language_client.onReady().then(() => + language_client.onNotification(protocol.decoration_type, decorations.apply_decoration)) /* caret handling */ @@ -70,12 +71,12 @@ } if (last_caret_update !== caret_update) { if (caret_update.uri) - client.sendNotification(protocol.caret_update_type, caret_update) + language_client.sendNotification(protocol.caret_update_type, caret_update) last_caret_update = caret_update } } - client.onReady().then(() => + language_client.onReady().then(() => { context.subscriptions.push( window.onDidChangeActiveTextEditor(_ => update_caret()), @@ -91,23 +92,21 @@ dynamic_output.show(true) dynamic_output.hide() - client.onReady().then(() => + language_client.onReady().then(() => { - client.onNotification(protocol.dynamic_output_type, + language_client.onNotification(protocol.dynamic_output_type, params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) }) }) - /* dynamic preview */ + /* preview */ - preview.init(context) - client.onReady().then(() => - client.onNotification(protocol.dynamic_preview_type, params => preview.update(params.content))) + language_client.onReady().then(() => preview.init(context, language_client)) /* start server */ - context.subscriptions.push(client.start()); + context.subscriptions.push(language_client.start()); } } diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/src/library.ts --- a/src/Tools/VSCode/extension/src/library.ts Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/extension/src/library.ts Wed May 31 17:25:26 2017 +0200 @@ -1,7 +1,7 @@ 'use strict'; import * as os from 'os'; -import { ViewColumn, TextEditor, Uri, workspace } from 'vscode' +import { TextEditor, Uri, workspace } from 'vscode' /* platform information */ @@ -32,13 +32,3 @@ const config = color + (light ? "_light" : "_dark") + "_color" return get_configuration(config) } - - -/* text editor column */ - -export function other_column(active_editor: TextEditor | null): ViewColumn -{ - if (!active_editor || active_editor.viewColumn === ViewColumn.Three) return ViewColumn.One - else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two - else return ViewColumn.Three -} diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/src/preview.ts --- a/src/Tools/VSCode/extension/src/preview.ts Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/extension/src/preview.ts Wed May 31 17:25:26 2017 +0200 @@ -1,14 +1,39 @@ 'use strict'; import * as timers from 'timers' -import { TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext, - Event, EventEmitter, Uri, Position, workspace, window, commands } from 'vscode' +import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider, + ExtensionContext, Event, EventEmitter, Uri, Position, workspace, + window, commands } from 'vscode' +import { LanguageClient } from 'vscode-languageclient'; import * as library from './library' +import * as protocol from './protocol'; + + +/* Uri information */ + +const preview_uri_template = Uri.parse("isabelle-preview:Preview") +const preview_uri_scheme = preview_uri_template.scheme + +function encode_preview(document_uri: Uri | undefined): Uri | undefined +{ + if (document_uri && library.is_file(document_uri)) { + return preview_uri_template.with({ query: document_uri.fsPath }) + } + else undefined +} + +function decode_preview(preview_uri: Uri | undefined): Uri | undefined +{ + if (preview_uri && preview_uri.scheme === preview_uri_scheme) { + return Uri.file(preview_uri.query) + } + else undefined +} /* HTML content */ -const preview_uri = Uri.parse("isabelle-preview:Preview") +const preview_content = new Map() const default_preview_content = ` @@ -20,35 +45,86 @@ ` -let preview_content = default_preview_content - class Provider implements TextDocumentContentProvider { dispose() { } private emitter = new EventEmitter() - public update() { this.emitter.fire(preview_uri) } + public update(preview_uri: Uri) { this.emitter.fire(preview_uri) } get onDidChange(): Event { return this.emitter.event } - provideTextDocumentContent(uri: Uri): string { return preview_content } -} - -export function update(content: string) -{ - preview_content = content === "" ? default_preview_content : content - provider.update() - commands.executeCommand("vscode.previewHtml", preview_uri, - library.other_column(window.activeTextEditor), "Isabelle Preview") + provideTextDocumentContent(preview_uri: Uri): string + { + return preview_content.get(preview_uri.toString()) || default_preview_content + } } /* init */ +let language_client: LanguageClient let provider: Provider -export function init(context: ExtensionContext) +export function init(context: ExtensionContext, client: LanguageClient) { + language_client = client + provider = new Provider() - context.subscriptions.push(workspace.registerTextDocumentContentProvider(preview_uri.scheme, provider)) - context.subscriptions.push(provider) + context.subscriptions.push( + workspace.registerTextDocumentContentProvider(preview_uri_scheme, provider), + provider) + + context.subscriptions.push( + commands.registerCommand("isabelle.preview", uri => request_preview(uri, false)), + commands.registerCommand("isabelle.preview-side", uri => request_preview(uri, true)), + commands.registerCommand("isabelle.preview-source", show_source)) + + language_client.onNotification(protocol.preview_response_type, + params => show_preview(Uri.parse(params.uri), params.column, params.label, params.content)) +} + + +/* commands */ + +function preview_column(side: boolean): ViewColumn +{ + const active_editor = window.activeTextEditor + + if (!active_editor) return ViewColumn.One + else if (!side) return active_editor.viewColumn + else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two + else return ViewColumn.Three } + +function request_preview(uri?: Uri, side: boolean = false) +{ + const document_uri = uri || window.activeTextEditor.document.uri + const preview_uri = encode_preview(document_uri) + if (preview_uri) { + language_client.sendNotification(protocol.preview_request_type, + {uri: document_uri.toString(), column: preview_column(side) }) + } +} + +function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string) +{ + const preview_uri = encode_preview(document_uri) + if (preview_uri) { + preview_content.set(preview_uri.toString(), content) + commands.executeCommand("vscode.previewHtml", preview_uri, column, label) + } +} + +function show_source(preview_uri: Uri) +{ + const document_uri = decode_preview(preview_uri) + if (document_uri) { + const editor = + window.visibleTextEditors.find(editor => + editor.document.uri.scheme === document_uri.scheme && + editor.document.uri.fsPath === document_uri.fsPath) + if (editor) window.showTextDocument(editor.document, editor.viewColumn) + else workspace.openTextDocument(document_uri).then(window.showTextDocument) + } + else commands.executeCommand("workbench.action.navigateBack") +} diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/extension/src/protocol.ts --- a/src/Tools/VSCode/extension/src/protocol.ts Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/extension/src/protocol.ts Wed May 31 17:25:26 2017 +0200 @@ -46,12 +46,24 @@ new NotificationType("PIDE/dynamic_output") -/* dynamic preview */ +/* preview */ -export interface Dynamic_Preview +export interface Preview_Request { + uri: string + column: number +} + +export interface Preview_Response +{ + uri: string + column: number + label: string content: string } -export const dynamic_preview_type = - new NotificationType("PIDE/dynamic_preview") +export const preview_request_type = + new NotificationType("PIDE/preview_request") + +export const preview_response_type = + new NotificationType("PIDE/preview_response") diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/src/dynamic_preview.scala --- a/src/Tools/VSCode/src/dynamic_preview.scala Wed May 31 11:49:29 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -/* Title: Tools/VSCode/src/dynamic_preview.scala - Author: Makarius - -Dynamic preview, depending on caret document node. -*/ - -package isabelle.vscode - - -import isabelle._ - -import java.io.{File => JFile} - - -object Dynamic_Preview -{ - def make_preview(model: Document_Model, snapshot: Document.Snapshot): XML.Body = - List( - HTML.chapter("Preview " + model.node_name), - HTML.itemize( - snapshot.node.commands.toList.flatMap( - command => - if (command.span.name == "") None - else Some(HTML.text(command.span.name))))) - - object State - { - val init: State = State() - } - - sealed case class State(file: Option[JFile] = None, body: XML.Body = Nil) - { - def handle_update( - resources: VSCode_Resources, - channel: Channel, - changed: Option[Set[Document.Node.Name]]): State = - { - val st1 = - if (resources.options.bool("vscode_caret_preview")) { - resources.get_caret() match { - case Some((caret_file, caret_model, _)) => - if (file != Some(caret_file) || - changed.isDefined && changed.get.contains(caret_model.node_name)) - { - val snapshot = caret_model.snapshot() - if (!snapshot.is_outdated) - State(Some(caret_file), make_preview(caret_model, snapshot)) - else this - } - else this - case None => State.init - } - } - else State.init - - if (st1.body != body) { - val content = - if (st1.body.isEmpty) "" - else HTML.output_document(Nil, st1.body, css = "") - channel.write(Protocol.Dynamic_Preview(content)) - } - - st1 - } - } - - def apply(server: Server): Dynamic_Preview = new Dynamic_Preview(server) -} - - -class Dynamic_Preview private(server: Server) -{ - private val state = Synchronized(Dynamic_Preview.State.init) - - private def handle_update(changed: Option[Set[Document.Node.Name]]) - { state.change(_.handle_update(server.resources, server.channel, changed)) } - - - /* main */ - - private val main = - Session.Consumer[Any](getClass.getName) { - case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) - 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 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/src/preview.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/preview.scala Wed May 31 17:25:26 2017 +0200 @@ -0,0 +1,58 @@ +/* Title: Tools/VSCode/src/preview.scala + Author: Makarius + +HTML document preview. +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{File => JFile} + + +class Preview(resources: VSCode_Resources) +{ + private val pending = Synchronized(Map.empty[JFile, Int]) + + def request(file: JFile, column: Int): Unit = + pending.change(map => map + (file -> column)) + + def flush(channel: Channel): Boolean = + { + pending.change_result(map => + { + val map1 = + (map /: map.iterator)({ case (m, (file, column)) => + resources.get_model(file) match { + case Some(model) => + val snapshot = model.snapshot() + if (snapshot.is_outdated) m + else { + val (label, content) = make_preview(model, snapshot) + channel.write(Protocol.Preview_Response(file, column, label, content)) + m - file + } + case None => m - file + } + }) + (map1.nonEmpty, map1) + }) + } + + def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) = + { + val label = "Preview " + quote(model.node_name.toString) + val content = + HTML.output_document(head = Nil, css = "", body = + List( + HTML.chapter(label), + HTML.itemize( + snapshot.node.commands.toList.flatMap( + command => + if (command.span.name == "") None + else Some(HTML.text(command.span.name)))))) + (label, content) + } +} diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Wed May 31 17:25:26 2017 +0200 @@ -465,11 +465,30 @@ } - /* dynamic preview */ + /* preview */ - object Dynamic_Preview + object Preview_Request { - def apply(content: String): JSON.T = - Notification("PIDE/dynamic_preview", Map("content" -> content)) + def unapply(json: JSON.T): Option[(JFile, Int)] = + json match { + case Notification("PIDE/preview_request", Some(params)) => + for { + uri <- JSON.string(params, "uri") + if Url.is_wellformed_file(uri) + column <- JSON.int(params, "column") + } yield (Url.canonical_file(uri), column) + case _ => None + } + } + + object Preview_Response + { + def apply(file: JFile, column: Int, label: String, content: String): JSON.T = + Notification("PIDE/preview_response", + Map( + "uri" -> Url.print_file(file), + "column" -> column, + "label" -> label, + "content" -> content)) } } diff -r 5b8fafde7d64 -r d8c5603c1732 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed May 31 11:49:29 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Wed May 31 17:25:26 2017 +0200 @@ -105,7 +105,6 @@ } yield (rendering, offset) private val dynamic_output = Dynamic_Output(this) - private val dynamic_preview = Dynamic_Preview(this) /* input from client or file-system */ @@ -177,6 +176,23 @@ } + /* preview */ + + private lazy val preview = new Preview(resources) + + private lazy val delay_preview: Standard_Thread.Delay = + Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger) + { + if (preview.flush(channel)) delay_preview.invoke() + } + + private def request_preview(file: JFile, column: Int) + { + preview.request(file, column) + delay_preview.invoke() + } + + /* output to client */ private val delay_output: Standard_Thread.Delay = @@ -251,7 +267,6 @@ session.all_messages += syslog dynamic_output.init() - dynamic_preview.init() var session_phase: Session.Consumer[Session.Phase] = null session_phase = @@ -281,13 +296,13 @@ session.all_messages -= syslog dynamic_output.exit() - dynamic_preview.exit() delay_load.revoke() file_watcher.shutdown() delay_input.revoke() delay_output.revoke() delay_caret_update.revoke() + delay_preview.revoke() val rc = session.stop() if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc) @@ -382,6 +397,7 @@ case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) + case Protocol.Preview_Request(file, column) => request_preview(file, column) case _ => log("### IGNORED") } }