--- a/src/Pure/build-jars Tue May 30 14:04:48 2017 +0200
+++ b/src/Pure/build-jars Tue May 30 22:39:18 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 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/etc/options Tue May 30 22:39:18 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/decorations.ts Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue May 30 22:39:18 2017 +0200
@@ -1,11 +1,11 @@
'use strict';
-import * as timers from 'timers';
-import * as vscode from 'vscode'
+import * as timers from 'timers'
+import { window, OverviewRulerLane } from 'vscode'
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
-import { get_color } from './extension'
import { Decoration } from './protocol'
+import * as library from './library'
/* known decoration types */
@@ -73,7 +73,7 @@
{
function decoration(options: DecorationRenderOptions): TextEditorDecorationType
{
- const typ = vscode.window.createTextEditorDecorationType(options)
+ const typ = window.createTextEditorDecorationType(options)
context.subscriptions.push(typ)
return typ
}
@@ -81,31 +81,31 @@
function background(color: string): TextEditorDecorationType
{
return decoration(
- { light: { backgroundColor: get_color(color, true) },
- dark: { backgroundColor: get_color(color, false) } })
+ { light: { backgroundColor: library.get_color(color, true) },
+ dark: { backgroundColor: library.get_color(color, false) } })
}
function text_color(color: string): TextEditorDecorationType
{
return decoration(
- { light: { color: get_color(color, true) },
- dark: { color: get_color(color, false) } })
+ { light: { color: library.get_color(color, true) },
+ dark: { color: library.get_color(color, false) } })
}
function text_overview_color(color: string): TextEditorDecorationType
{
return decoration(
- { overviewRulerLane: vscode.OverviewRulerLane.Right,
- light: { overviewRulerColor: get_color(color, true) },
- dark: { overviewRulerColor: get_color(color, false) } })
+ { overviewRulerLane: OverviewRulerLane.Right,
+ light: { overviewRulerColor: library.get_color(color, true) },
+ dark: { overviewRulerColor: library.get_color(color, false) } })
}
function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
{
const border = `${width} none; border-bottom-style: ${style}; border-color: `
return decoration(
- { light: { border: border + get_color(color, true) },
- dark: { border: border + get_color(color, false) } })
+ { light: { border: border + library.get_color(color, true) },
+ dark: { border: border + library.get_color(color, false) } })
}
@@ -113,7 +113,7 @@
types.forEach(typ =>
{
- for (const editor of vscode.window.visibleTextEditors) {
+ for (const editor of window.visibleTextEditors) {
editor.setDecorations(typ, [])
}
const i = context.subscriptions.indexOf(typ)
@@ -145,7 +145,7 @@
/* update editors */
- for (const editor of vscode.window.visibleTextEditors) {
+ for (const editor of window.visibleTextEditors) {
update_editor(editor)
}
}
@@ -179,7 +179,7 @@
document.set(decoration.type, content)
document_decorations.set(uri, document)
- for (const editor of vscode.window.visibleTextEditors) {
+ for (const editor of window.visibleTextEditors) {
if (uri === editor.document.uri.toString()) {
editor.setDecorations(typ, content)
}
@@ -200,14 +200,15 @@
}
-/* decorations vs. document changes */
+/* handle document changes */
const touched_documents = new Set<TextDocument>()
+let touched_timer: NodeJS.Timer
function update_touched_documents()
{
const touched_editors: TextEditor[] = []
- for (const editor of vscode.window.visibleTextEditors) {
+ for (const editor of window.visibleTextEditors) {
if (touched_documents.has(editor.document)) {
touched_editors.push(editor)
}
@@ -216,8 +217,6 @@
touched_editors.forEach(update_editor)
}
-let touched_timer: NodeJS.Timer
-
export function touch_document(document: TextDocument)
{
if (touched_timer) timers.clearTimeout(touched_timer)
--- a/src/Tools/VSCode/extension/src/extension.ts Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Tue May 30 22:39:18 2017 +0200
@@ -1,9 +1,9 @@
'use strict';
-import * as vscode from 'vscode';
+import { ExtensionContext, workspace, window } from 'vscode';
import * as path from 'path';
import * as fs from 'fs';
-import * as os from 'os';
+import * as library from './library'
import * as decorations from './decorations';
import * as preview from './preview';
import * as protocol from './protocol';
@@ -11,43 +11,25 @@
from 'vscode-languageclient';
-/* Isabelle configuration */
-
-export function get_configuration<T>(name: string): T
-{
- return vscode.workspace.getConfiguration("isabelle").get<T>(name)
-}
-
-export function get_color(color: string, light: boolean): string
-{
- const config = color + (light ? "_light" : "_dark") + "_color"
- return get_configuration<string>(config)
-}
-
-
-/* activate extension */
-
let last_caret_update: protocol.Caret_Update = {}
-export function activate(context: vscode.ExtensionContext)
+export function activate(context: ExtensionContext)
{
- const is_windows = os.type().startsWith("Windows")
-
- const isabelle_home = get_configuration<string>("home")
- const isabelle_args = get_configuration<Array<string>>("args")
- const cygwin_root = get_configuration<string>("cygwin_root")
+ const isabelle_home = library.get_configuration<string>("home")
+ const isabelle_args = library.get_configuration<Array<string>>("args")
+ const cygwin_root = library.get_configuration<string>("cygwin_root")
/* server */
if (isabelle_home === "")
- vscode.window.showErrorMessage("Missing user settings: isabelle.home")
+ window.showErrorMessage("Missing user settings: isabelle.home")
else {
const isabelle_tool = isabelle_home + "/bin/isabelle"
const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
const server_options: ServerOptions =
- is_windows ?
+ library.platform_is_windows() ?
{ command:
(cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) +
"/bin/bash",
@@ -64,30 +46,26 @@
/* decorations */
decorations.init(context)
- vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
- vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
- vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
- vscode.workspace.onDidCloseTextDocument(decorations.close_document)
+ context.subscriptions.push(
+ workspace.onDidChangeConfiguration(() => decorations.init(context)),
+ workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)),
+ window.onDidChangeActiveTextEditor(decorations.update_editor),
+ workspace.onDidCloseTextDocument(decorations.close_document))
client.onReady().then(() =>
client.onNotification(protocol.decoration_type, decorations.apply_decoration))
- /* 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()
+ /* caret handling */
function update_caret()
{
- const editor = vscode.window.activeTextEditor
+ const editor = window.activeTextEditor
let caret_update: protocol.Caret_Update = {}
if (editor) {
const uri = editor.document.uri
const cursor = editor.selection.active
- if (uri.scheme === "file" && cursor)
+ if (library.is_file(uri) && cursor)
caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
}
if (last_caret_update !== caret_update) {
@@ -99,17 +77,32 @@
client.onReady().then(() =>
{
- client.onNotification(protocol.dynamic_output_type,
- params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
- vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
- vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
+ context.subscriptions.push(
+ window.onDidChangeActiveTextEditor(_ => update_caret()),
+ window.onDidChangeTextEditorSelection(_ => update_caret()))
update_caret()
})
- /* preview */
+ /* dynamic output */
+
+ const dynamic_output = window.createOutputChannel("Isabelle Output")
+ context.subscriptions.push(dynamic_output)
+ dynamic_output.show(true)
+ dynamic_output.hide()
+
+ client.onReady().then(() =>
+ {
+ client.onNotification(protocol.dynamic_output_type,
+ params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
+ })
+
+
+ /* dynamic preview */
preview.init(context)
+ client.onReady().then(() =>
+ client.onNotification(protocol.dynamic_preview_type, params => preview.update(params.content)))
/* start server */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/library.ts Tue May 30 22:39:18 2017 +0200
@@ -0,0 +1,44 @@
+'use strict';
+
+import * as os from 'os';
+import { ViewColumn, TextEditor, Uri, workspace } from 'vscode'
+
+
+/* platform information */
+
+export function platform_is_windows(): boolean
+{
+ return os.type().startsWith("Windows")
+}
+
+
+/* file URIs */
+
+export function is_file(uri: Uri): boolean
+{
+ return uri.scheme === "file"
+}
+
+
+/* Isabelle configuration */
+
+export function get_configuration<T>(name: string): T
+{
+ return workspace.getConfiguration("isabelle").get<T>(name)
+}
+
+export function get_color(color: string, light: boolean): string
+{
+ 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 Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Tue May 30 22:39:18 2017 +0200
@@ -1,93 +1,54 @@
'use strict';
-import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position,
- ViewColumn, workspace, window, commands } from 'vscode'
+import * as timers from 'timers'
+import { TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext,
+ Event, EventEmitter, Uri, Position, workspace, window, commands } from 'vscode'
+import * as library from './library'
-const uri_scheme = 'isabelle-preview';
+/* HTML content */
+
+const preview_uri = Uri.parse("isabelle-preview:Preview")
+
+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>`
+
+let preview_content = default_preview_content
class Provider implements TextDocumentContentProvider
{
- constructor() { }
dispose() { }
private emitter = new EventEmitter<Uri>()
- private waiting: boolean = false;
-
+ public update() { this.emitter.fire(preview_uri) }
get onDidChange(): Event<Uri> { return this.emitter.event }
- public update(document_uri: Uri)
- {
- if (!this.waiting) {
- this.waiting = true
- setTimeout(() =>
- {
- this.waiting = false
- this.emitter.fire(encode_name(document_uri))
- }, 300)
- }
- }
-
- provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
- {
- const document_uri = decode_name(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 encode_name(document_uri: Uri): Uri
+export function update(content: string)
{
- return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
+ preview_content = content === "" ? default_preview_content : content
+ provider.update()
+ commands.executeCommand("vscode.previewHtml", preview_uri,
+ library.other_column(window.activeTextEditor), "Isabelle Preview")
}
-export function decode_name(preview_uri: Uri): Uri
-{
- const [name] = <[string]>JSON.parse(preview_uri.query)
- return Uri.parse(name)
-}
-function other_column(): ViewColumn
-{
- const active = window.activeTextEditor
- if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One
- else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two
- else return ViewColumn.Three
-}
+/* init */
+
+let provider: Provider
export function init(context: ExtensionContext)
{
- const provider = new Provider()
- context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
+ provider = new 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_name(editor.document.uri)
- return workspace.openTextDocument(preview_uri).then(doc =>
- commands.executeCommand("vscode.previewHtml", preview_uri, other_column(), "Isabelle Preview"))
- }))
-
- context.subscriptions.push(
- workspace.onDidChangeTextDocument(event =>
- {
- if (event.document.languageId === 'isabelle') {
- provider.update(event.document.uri)
- }
- }))
}
--- a/src/Tools/VSCode/extension/src/protocol.ts Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts Tue May 30 22:39:18 2017 +0200
@@ -39,8 +39,19 @@
export interface Dynamic_Output
{
- body: string
+ content: string
}
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")
--- a/src/Tools/VSCode/src/dynamic_output.scala Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Tue May 30 22:39:18 2017 +0200
@@ -18,9 +18,9 @@
resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =
{
val st1 =
- resources.caret_offset() match {
+ resources.get_caret() match {
case None => copy(output = Nil)
- case Some((model, caret_offset)) =>
+ case Some((_, model, caret_offset)) =>
val snapshot = model.snapshot()
if (do_update && !snapshot.is_outdated) {
snapshot.current_command(model.node_name, caret_offset) match {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/dynamic_preview.scala Tue May 30 22:39:18 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 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala Tue May 30 22:39:18 2017 +0200
@@ -461,6 +461,15 @@
object Dynamic_Output
{
def apply(body: String): JSON.T =
- Notification("PIDE/dynamic_output", Map("body" -> body))
+ Notification("PIDE/dynamic_output", Map("content" -> 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 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala Tue May 30 22:39:18 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()
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue May 30 14:04:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue May 30 22:39:18 2017 +0200
@@ -302,7 +302,7 @@
def update_caret(caret: Option[(JFile, Line.Position)])
{ state.change(_.update_caret(caret)) }
- def caret_offset(): Option[(Document_Model, Text.Offset)] =
+ def get_caret(): Option[(JFile, Document_Model, Text.Offset)] =
{
val st = state.value
for {
@@ -310,7 +310,7 @@
model <- st.models.get(file)
offset <- model.content.doc.offset(pos)
}
- yield (model, offset)
+ yield (file, model, offset)
}