--- a/src/Pure/build-jars Tue May 30 21:38:38 2017 +0200
+++ b/src/Pure/build-jars Tue May 30 22:06:39 2017 +0200
@@ -167,6 +167,7 @@
../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/protocol.scala
../Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/etc/options Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/etc/options Tue May 30 22:06:39 2017 +0200
@@ -26,3 +26,6 @@
option vscode_caret_perspective : int = 50
-- "number of visible lines above and below the caret (0: unrestricted)"
+
+option vscode_caret_preview : bool = false
+ -- "dynamic preview of caret document node"
--- a/src/Tools/VSCode/extension/src/extension.ts Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Tue May 30 22:06:39 2017 +0200
@@ -91,11 +91,11 @@
})
- /* preview */
+ /* dynamic preview */
preview.init(context)
- context.subscriptions.push(
- workspace.onDidChangeTextDocument(event => preview.touch_document(event.document)))
+ client.onReady().then(() =>
+ client.onNotification(protocol.dynamic_preview_type, params => preview.update(params.content)))
/* start server */
--- a/src/Tools/VSCode/extension/src/preview.ts Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue May 30 22:06:39 2017 +0200
@@ -6,49 +6,39 @@
import * as library from './library'
-/* generated content */
+/* HTML content */
-const uri_scheme = 'isabelle-preview';
+const preview_uri = Uri.parse("isabelle-preview:Preview")
-export function encode_preview(document_uri: Uri): Uri
-{
- return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
-}
+const default_preview_content =
+ `<html>
+ <head>
+ <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
+ </head>
+ <body>
+ <h1>Isabelle Preview</h1>
+ </body>
+ </html>`
-export function decode_preview(preview_uri: Uri): Uri
-{
- const [name] = <[string]>JSON.parse(preview_uri.query)
- return Uri.parse(name)
-}
+let preview_content = default_preview_content
class Provider implements TextDocumentContentProvider
{
dispose() { }
private emitter = new EventEmitter<Uri>()
- public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
+ public update() { this.emitter.fire(preview_uri) }
get onDidChange(): Event<Uri> { return this.emitter.event }
- provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
- {
- const document_uri = decode_preview(preview_uri)
- const editor =
- window.visibleTextEditors.find(editor =>
- document_uri.toString() === editor.document.uri.toString())
- return `
- <html>
- <head>
- <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
- </head>
- <body>
- <h1>Isabelle Preview</h1>
- <ul>
- <li><b>file</b> = <code>${document_uri.fsPath}</code></li>` +
- (editor ? `<li><b>line count</b> = ${editor.document.lineCount}</li>` : "") +
- `</ul>
- </body>
- </html>`
- }
+ 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")
}
@@ -59,39 +49,6 @@
export function init(context: ExtensionContext)
{
provider = new Provider()
- context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
+ context.subscriptions.push(workspace.registerTextDocumentContentProvider(preview_uri.scheme, provider))
context.subscriptions.push(provider)
-
- context.subscriptions.push(
- commands.registerTextEditorCommand("isabelle.preview", editor =>
- {
- const preview_uri = encode_preview(editor.document.uri)
- return workspace.openTextDocument(preview_uri).then(doc =>
- commands.executeCommand("vscode.previewHtml", preview_uri,
- library.other_column(window.activeTextEditor), "Isabelle Preview"))
- }))
}
-
-
-/* handle document changes */
-
-const touched_documents = new Set<TextDocument>()
-let touched_timer: NodeJS.Timer
-
-function update_touched_documents()
-{
- if (provider) {
- for (const document of touched_documents) {
- provider.update(encode_preview(document.uri))
- }
- }
-}
-
-export function touch_document(document: TextDocument)
-{
- if (library.is_file(document.uri) && document.languageId === 'isabelle') {
- if (touched_timer) timers.clearTimeout(touched_timer)
- touched_documents.add(document)
- touched_timer = timers.setTimeout(update_touched_documents, 300)
- }
-}
--- a/src/Tools/VSCode/extension/src/protocol.ts Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts Tue May 30 22:06:39 2017 +0200
@@ -44,3 +44,14 @@
export const dynamic_output_type =
new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
+
+
+/* dynamic preview */
+
+export interface Dynamic_Preview
+{
+ content: string
+}
+
+export const dynamic_preview_type =
+ new NotificationType<Dynamic_Preview, void>("PIDE/dynamic_preview")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/dynamic_preview.scala Tue May 30 22:06:39 2017 +0200
@@ -0,0 +1,99 @@
+/* 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
+ }
+}
--- a/src/Tools/VSCode/src/protocol.scala Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala Tue May 30 22:06:39 2017 +0200
@@ -463,4 +463,13 @@
def apply(body: String): JSON.T =
Notification("PIDE/dynamic_output", Map("body" -> body))
}
+
+
+ /* dynamic preview */
+
+ object Dynamic_Preview
+ {
+ def apply(content: String): JSON.T =
+ Notification("PIDE/dynamic_preview", Map("content" -> content))
+ }
}
--- a/src/Tools/VSCode/src/server.scala Tue May 30 21:38:38 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Tue May 30 22:06:39 2017 +0200
@@ -105,6 +105,7 @@
} yield (rendering, offset)
private val dynamic_output = Dynamic_Output(this)
+ private val dynamic_preview = Dynamic_Preview(this)
/* input from client or file-system */
@@ -250,6 +251,7 @@
session.all_messages += syslog
dynamic_output.init()
+ dynamic_preview.init()
var session_phase: Session.Consumer[Session.Phase] = null
session_phase =
@@ -279,6 +281,7 @@
session.all_messages -= syslog
dynamic_output.exit()
+ dynamic_preview.exit()
delay_load.revoke()
file_watcher.shutdown()