# HG changeset patch # User wenzelm # Date 1496176758 -7200 # Node ID 3bec939bd808c4f99970b461deaf82a0e8dbb510 # Parent 088c79b4015689a886cb170f1b9216d3d772075f# Parent c208fcf369b7a270c48c3080fd4936fa3ea6de80 merged diff -r 088c79b40156 -r 3bec939bd808 src/Pure/build-jars --- 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 diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/etc/options --- 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" diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/extension/src/decorations.ts --- 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() +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) diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/extension/src/extension.ts --- 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(name: string): T -{ - return vscode.workspace.getConfiguration("isabelle").get(name) -} - -export function get_color(color: string, light: boolean): string -{ - const config = color + (light ? "_light" : "_dark") + "_color" - return get_configuration(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("home") - const isabelle_args = get_configuration>("args") - const cygwin_root = get_configuration("cygwin_root") + const isabelle_home = library.get_configuration("home") + const isabelle_args = library.get_configuration>("args") + const cygwin_root = library.get_configuration("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 */ diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/extension/src/library.ts --- /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(name: string): T +{ + return workspace.getConfiguration("isabelle").get(name) +} + +export function get_color(color: string, light: boolean): string +{ + 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 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/extension/src/preview.ts --- 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 = + ` + + + + +

Isabelle Preview

+ + ` + +let preview_content = default_preview_content class Provider implements TextDocumentContentProvider { - constructor() { } dispose() { } private emitter = new EventEmitter() - private waiting: boolean = false; - + public update() { this.emitter.fire(preview_uri) } get onDidChange(): Event { 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 - { - const document_uri = decode_name(preview_uri) - const editor = - window.visibleTextEditors.find(editor => - document_uri.toString() === editor.document.uri.toString()) - return ` - - - - - -

Isabelle Preview

-
    -
  • file = ${document_uri.fsPath}
    • ` + - (editor ? `
  • line count = ${editor.document.lineCount}
    • ` : "") + - `
- - ` - } + 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) - } - })) } diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/extension/src/protocol.ts --- 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("PIDE/dynamic_output") + + +/* dynamic preview */ + +export interface Dynamic_Preview +{ + content: string +} + +export const dynamic_preview_type = + new NotificationType("PIDE/dynamic_preview") diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/src/dynamic_output.scala --- 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 { diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/src/dynamic_preview.scala --- /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 + } +} diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/src/protocol.scala --- 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)) } } diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/src/server.scala --- 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() diff -r 088c79b40156 -r 3bec939bd808 src/Tools/VSCode/src/vscode_resources.scala --- 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) }