explicit preview request/response;
commands, icons, menus like VSCode markdown preview;
clarified Uri information (again);
tuned;
--- 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
--- /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 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16"><style>.st0{fill:#f6f6f6}.st1{fill:none}.st2{fill:#424242}.st3{fill:#f0eff1}</style><path class="st0" d="M11.949 4C11.697 1.756 9.811 0 7.5 0A4.505 4.505 0 0 0 3 4.5c0 .6.12 1.188.35 1.735L0 9.586v.828l2 2 3-2.999V16h11V4h-4.051z" id="outline" style="display: none;"/><g id="icon_x5F_bg"><circle class="st1" cx="7.5" cy="4.5" r="2.5"/><path class="st2" d="M12 10h1v3h-1zM10 11h1v2h-1zM8 12h1v1H8zM8 9h2v1H8z"/><path class="st2" d="M11.949 5a4.431 4.431 0 0 1-.226 1H14v8H7V8.95a4.447 4.447 0 0 1-1-.227V15h9V5h-3.051z"/><path class="st2" d="M10.294 8H12V7h-.762a4.527 4.527 0 0 1-.944 1zM11 4.5a3.5 3.5 0 1 0-7 0c0 .711.215 1.369.579 1.922L1 10l1 1 3.579-3.578A3.485 3.485 0 0 0 7.5 8 3.5 3.5 0 0 0 11 4.5zm-6 0a2.5 2.5 0 1 1 5 0 2.5 2.5 0 0 1-5 0z"/></g><g id="icon_x5F_fg"><path class="st1" d="M10 11h1v2h-1zM8 12h1v1H8zM8 9h2v1H8zM12 10h1v3h-1z"/><path class="st3" d="M11.724 6a4.469 4.469 0 0 1-.485 1H12v1h-1.706c-.771.616-1.733 1-2.794 1-.169 0-.333-.031-.5-.05V14h7V6h-2.276zM8 9h2v1H8V9zm1 4H8v-1h1v1zm2 0h-1v-2h1v2zm2 0h-1v-3h1v3z"/><circle class="st3" cx="7.5" cy="4.5" r="2.5"/></g></svg>
\ No newline at end of file
--- /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 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!-- Generator: Adobe Illustrator 19.2.0, SVG Export Plug-In . SVG Version: 6.00 Build 0) -->
+<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px"
+ viewBox="0 0 16 16" style="enable-background:new 0 0 16 16;" xml:space="preserve">
+<style type="text/css">
+ .icon_x002D_vs_x002D_bg{fill:#424242;}
+</style>
+<g id="canvas">
+</g>
+<g id="outline">
+</g>
+<g id="iconFg">
+</g>
+<g id="iconBg">
+ <path class="icon_x002D_vs_x002D_bg" d="M9,5h5v2.4c0.4,0.2,0.7,0.4,1,0.7V2H1v12h5.6L9,11.6V5z M2,13V5h5v8H2z M11.3,12.7
+ c0.4,0.2,0.8,0.3,1.2,0.3c1.4,0,2.5-1.1,2.5-2.5C15,9.1,13.9,8,12.5,8C11.1,8,10,9.1,10,10.5c0,0.4,0.1,0.8,0.3,1.2L8,14l1,1
+ L11.3,12.7z M11,10.5C11,9.7,11.7,9,12.5,9c0.8,0,1.5,0.7,1.5,1.5c0,0.8-0.7,1.5-1.5,1.5C11.7,12,11,11.3,11,10.5z"/>
+</g>
+</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 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!-- Generator: Adobe Illustrator 19.2.0, SVG Export Plug-In . SVG Version: 6.00 Build 0) -->
+<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px"
+ viewBox="0 0 16 16" style="enable-background:new 0 0 16 16;" xml:space="preserve">
+<style type="text/css">
+ .st0{fill:#C5C5C5;}
+</style>
+<g id="canvas">
+</g>
+<g id="outline">
+</g>
+<g id="iconFg">
+</g>
+<g id="iconBg">
+ <path class="st0" d="M9,5h5v2.4c0.4,0.2,0.7,0.4,1,0.7V2H1v12h5.6L9,11.6V5z M2,13V5h5v8H2z M11.3,12.7c0.4,0.2,0.8,0.3,1.2,0.3
+ c1.4,0,2.5-1.1,2.5-2.5C15,9.1,13.9,8,12.5,8C11.1,8,10,9.1,10,10.5c0,0.4,0.1,0.8,0.3,1.2L8,14l1,1L11.3,12.7z M11,10.5
+ C11,9.7,11.7,9,12.5,9c0.8,0,1.5,0.7,1.5,1.5c0,0.8-0.7,1.5-1.5,1.5C11.7,12,11,11.3,11,10.5z"/>
+</g>
+</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 @@
+<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16"><style>.st0{fill:#2d2d30}.st1{fill:none}.st2{fill:#c5c5c5}.st3{fill:#2b282e}</style><path class="st0" d="M11.949 4C11.697 1.756 9.811 0 7.5 0A4.505 4.505 0 0 0 3 4.5c0 .6.12 1.188.35 1.735L0 9.586v.828l2 2 3-2.999V16h11V4h-4.051z" id="outline" style="display: none;"/><g id="icon_x5F_bg"><circle class="st1" cx="7.5" cy="4.5" r="2.5"/><path class="st2" d="M12 10h1v3h-1zM10 11h1v2h-1zM8 12h1v1H8zM8 9h2v1H8z"/><path class="st2" d="M11.949 5a4.431 4.431 0 0 1-.226 1H14v8H7V8.95a4.447 4.447 0 0 1-1-.227V15h9V5h-3.051z"/><path class="st2" d="M10.294 8H12V7h-.762a4.527 4.527 0 0 1-.944 1zM11 4.5a3.5 3.5 0 1 0-7 0c0 .711.215 1.369.579 1.922L1 10l1 1 3.579-3.578A3.485 3.485 0 0 0 7.5 8 3.5 3.5 0 0 0 11 4.5zm-6 0a2.5 2.5 0 1 1 5 0 2.5 2.5 0 0 1-5 0z"/></g><g id="icon_x5F_fg"><path class="st1" d="M10 11h1v2h-1zM8 12h1v1H8zM8 9h2v1H8zM12 10h1v3h-1z"/><path class="st3" d="M11.724 6a4.469 4.469 0 0 1-.485 1H12v1h-1.706c-.771.616-1.733 1-2.794 1-.169 0-.333-.031-.5-.05V14h7V6h-2.276zM8 9h2v1H8V9zm1 4H8v-1h1v1zm2 0h-1v-2h1v2zm2 0h-1v-3h1v3z"/><circle class="st3" cx="7.5" cy="4.5" r="2.5"/></g></svg>
\ No newline at end of file
--- /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 @@
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd" [
+ <!ENTITY ns_flows "http://ns.adobe.com/Flows/1.0/">
+]><svg xmlns="http://www.w3.org/2000/svg" width="16" height="16"><polygon fill="#656565" points="10,2 7.414,2 8.414,3 9,3 9,3.586 9,4 9,4.414 9,6 12,6 12,13 4,13 4,8 3,8 3,14 13,14 13,5"/><polygon fill="#00539C" points="5,1 3,1 5,3 1,3 1,5 5,5 3,7 5,7 8,4"/></svg>
\ No newline at end of file
--- /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 @@
+<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16"><polygon fill="#C5C5C5" points="10,2 7.414,2 8.414,3 9,3 9,3.586 9,4 9,4.414 9,6 12,6 12,13 4,13 4,8 3,8 3,14 13,14 13,5"/><polygon fill="#75BEFF" points="5,1 3,1 5,3 1,3 1,5 5,5 3,7 5,7 8,4"/></svg>
\ No newline at end of file
--- 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",
--- 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());
}
}
--- 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<string>(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
-}
--- 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<string, string>()
const default_preview_content =
`<html>
@@ -20,35 +45,86 @@
</body>
</html>`
-let preview_content = default_preview_content
-
class Provider implements TextDocumentContentProvider
{
dispose() { }
private emitter = new EventEmitter<Uri>()
- public update() { this.emitter.fire(preview_uri) }
+ public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
get onDidChange(): Event<Uri> { 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")
+}
--- 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<Dynamic_Output, void>("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<Dynamic_Preview, void>("PIDE/dynamic_preview")
+export const preview_request_type =
+ new NotificationType<Preview_Request, void>("PIDE/preview_request")
+
+export const preview_response_type =
+ new NotificationType<Preview_Response, void>("PIDE/preview_response")
--- 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
- }
-}
--- /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)
+ }
+}
--- 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))
}
}
--- 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")
}
}
