explicit preview request/response;
authorwenzelm
Wed May 31 17:25:26 2017 +0200 (2017-05-31)
changeset 65983d8c5603c1732
parent 65982 5b8fafde7d64
child 65984 8e6a833da7db
explicit preview request/response;
commands, icons, menus like VSCode markdown preview;
clarified Uri information (again);
tuned;
src/Pure/build-jars
src/Tools/VSCode/extension/media/Preview.svg
src/Tools/VSCode/extension/media/PreviewOnRightPane_16x.svg
src/Tools/VSCode/extension/media/PreviewOnRightPane_16x_dark.svg
src/Tools/VSCode/extension/media/Preview_inverse.svg
src/Tools/VSCode/extension/media/ViewSource.svg
src/Tools/VSCode/extension/media/ViewSource_inverse.svg
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/library.ts
src/Tools/VSCode/extension/src/preview.ts
src/Tools/VSCode/extension/src/protocol.ts
src/Tools/VSCode/src/dynamic_preview.scala
src/Tools/VSCode/src/preview.scala
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Pure/build-jars	Wed May 31 11:49:29 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Wed May 31 17:25:26 2017 +0200
     1.3 @@ -167,8 +167,8 @@
     1.4    ../Tools/VSCode/src/channel.scala
     1.5    ../Tools/VSCode/src/document_model.scala
     1.6    ../Tools/VSCode/src/dynamic_output.scala
     1.7 -  ../Tools/VSCode/src/dynamic_preview.scala
     1.8    ../Tools/VSCode/src/grammar.scala
     1.9 +  ../Tools/VSCode/src/preview.scala
    1.10    ../Tools/VSCode/src/protocol.scala
    1.11    ../Tools/VSCode/src/server.scala
    1.12    ../Tools/VSCode/src/vscode_rendering.scala
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/VSCode/extension/media/Preview.svg	Wed May 31 17:25:26 2017 +0200
     2.3 @@ -0,0 +1,1 @@
     2.4 +<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>
     2.5 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/VSCode/extension/media/PreviewOnRightPane_16x.svg	Wed May 31 17:25:26 2017 +0200
     3.3 @@ -0,0 +1,19 @@
     3.4 +<?xml version="1.0" encoding="utf-8"?>
     3.5 +<!-- Generator: Adobe Illustrator 19.2.0, SVG Export Plug-In . SVG Version: 6.00 Build 0)  -->
     3.6 +<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px"
     3.7 +	 viewBox="0 0 16 16" style="enable-background:new 0 0 16 16;" xml:space="preserve">
     3.8 +<style type="text/css">
     3.9 +	.icon_x002D_vs_x002D_bg{fill:#424242;}
    3.10 +</style>
    3.11 +<g id="canvas">
    3.12 +</g>
    3.13 +<g id="outline">
    3.14 +</g>
    3.15 +<g id="iconFg">
    3.16 +</g>
    3.17 +<g id="iconBg">
    3.18 +	<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
    3.19 +		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
    3.20 +		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"/>
    3.21 +</g>
    3.22 +</svg>
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/extension/media/PreviewOnRightPane_16x_dark.svg	Wed May 31 17:25:26 2017 +0200
     4.3 @@ -0,0 +1,19 @@
     4.4 +<?xml version="1.0" encoding="utf-8"?>
     4.5 +<!-- Generator: Adobe Illustrator 19.2.0, SVG Export Plug-In . SVG Version: 6.00 Build 0)  -->
     4.6 +<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" x="0px" y="0px"
     4.7 +	 viewBox="0 0 16 16" style="enable-background:new 0 0 16 16;" xml:space="preserve">
     4.8 +<style type="text/css">
     4.9 +	.st0{fill:#C5C5C5;}
    4.10 +</style>
    4.11 +<g id="canvas">
    4.12 +</g>
    4.13 +<g id="outline">
    4.14 +</g>
    4.15 +<g id="iconFg">
    4.16 +</g>
    4.17 +<g id="iconBg">
    4.18 +	<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
    4.19 +		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
    4.20 +		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"/>
    4.21 +</g>
    4.22 +</svg>
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/VSCode/extension/media/Preview_inverse.svg	Wed May 31 17:25:26 2017 +0200
     5.3 @@ -0,0 +1,1 @@
     5.4 +<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>
     5.5 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/VSCode/extension/media/ViewSource.svg	Wed May 31 17:25:26 2017 +0200
     6.3 @@ -0,0 +1,3 @@
     6.4 +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd" [
     6.5 +	<!ENTITY ns_flows "http://ns.adobe.com/Flows/1.0/">
     6.6 +]><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>
     6.7 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/VSCode/extension/media/ViewSource_inverse.svg	Wed May 31 17:25:26 2017 +0200
     7.3 @@ -0,0 +1,1 @@
     7.4 +<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>
     7.5 \ No newline at end of file
     8.1 --- a/src/Tools/VSCode/extension/package.json	Wed May 31 11:49:29 2017 +0200
     8.2 +++ b/src/Tools/VSCode/extension/package.json	Wed May 31 17:25:26 2017 +0200
     8.3 @@ -18,16 +18,64 @@
     8.4      "categories": ["Languages"],
     8.5      "activationEvents": [
     8.6          "onLanguage:isabelle",
     8.7 -        "onLanguage:isabelle-ml"
     8.8 +        "onLanguage:isabelle-ml",
     8.9 +        "onCommand:isabelle.preview",
    8.10 +        "onCommand:isabelle.preview-side",
    8.11 +        "onCommand:isabelle.preview-source"
    8.12      ],
    8.13      "main": "./out/src/extension",
    8.14      "contributes": {
    8.15          "commands": [
    8.16              {
    8.17 -                "command": "isabelle.preview",
    8.18 -                "title": "Isabelle Document Preview"
    8.19 +				"command": "isabelle.preview",
    8.20 +				"title": "Open Preview",
    8.21 +				"category": "Isabelle",
    8.22 +				"icon": {
    8.23 +					"light": "./media/Preview.svg",
    8.24 +					"dark": "./media/Preview_inverse.svg"
    8.25 +				}
    8.26 +			},
    8.27 +			{
    8.28 +				"command": "isabelle.preview-side",
    8.29 +				"title": "Open Preview to the Side",
    8.30 +				"category": "Isabelle",
    8.31 +				"icon": {
    8.32 +					"light": "./media/PreviewOnRightPane_16x.svg",
    8.33 +					"dark": "./media/PreviewOnRightPane_16x_dark.svg"
    8.34 +				}
    8.35 +			},
    8.36 +   			{
    8.37 +				"command": "isabelle.preview-source",
    8.38 +				"title": "Show Source",
    8.39 +				"category": "Isabelle",
    8.40 +				"icon": {
    8.41 +					"light": "./media/ViewSource.svg",
    8.42 +					"dark": "./media/ViewSource_inverse.svg"
    8.43 +			    }
    8.44              }
    8.45          ],
    8.46 +        "menus": {
    8.47 +			"editor/title": [
    8.48 +				{
    8.49 +					"when": "editorLangId == isabelle",
    8.50 +					"command": "isabelle.preview-side",
    8.51 +					"alt": "isabelle.preview",
    8.52 +					"group": "navigation"
    8.53 +				},
    8.54 +				{
    8.55 +					"when": "resourceScheme == isabelle-preview",
    8.56 +					"command": "isabelle.preview-source",
    8.57 +					"group": "navigation"
    8.58 +				}
    8.59 +			],
    8.60 +			"explorer/context": [
    8.61 +				{
    8.62 +					"when": "resourceLangId == isabelle",
    8.63 +					"command": "isabelle.preview",
    8.64 +					"group": "navigation"
    8.65 +				}
    8.66 +			]
    8.67 +		},
    8.68          "languages": [
    8.69              {
    8.70                  "id": "isabelle",
     9.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 11:49:29 2017 +0200
     9.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 17:25:26 2017 +0200
     9.3 @@ -36,11 +36,12 @@
     9.4            args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
     9.5          { command: isabelle_tool,
     9.6            args: ["vscode_server"].concat(standard_args, isabelle_args) };
     9.7 -    const client_options: LanguageClientOptions = {
     9.8 +    const language_client_options: LanguageClientOptions = {
     9.9        documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
    9.10      };
    9.11  
    9.12 -    const client = new LanguageClient("Isabelle", server_options, client_options, false)
    9.13 +    const language_client =
    9.14 +      new LanguageClient("Isabelle", server_options, language_client_options, false)
    9.15  
    9.16  
    9.17      /* decorations */
    9.18 @@ -52,8 +53,8 @@
    9.19        window.onDidChangeActiveTextEditor(decorations.update_editor),
    9.20        workspace.onDidCloseTextDocument(decorations.close_document))
    9.21  
    9.22 -    client.onReady().then(() =>
    9.23 -      client.onNotification(protocol.decoration_type, decorations.apply_decoration))
    9.24 +    language_client.onReady().then(() =>
    9.25 +      language_client.onNotification(protocol.decoration_type, decorations.apply_decoration))
    9.26  
    9.27  
    9.28      /* caret handling */
    9.29 @@ -70,12 +71,12 @@
    9.30        }
    9.31        if (last_caret_update !== caret_update) {
    9.32          if (caret_update.uri)
    9.33 -          client.sendNotification(protocol.caret_update_type, caret_update)
    9.34 +          language_client.sendNotification(protocol.caret_update_type, caret_update)
    9.35          last_caret_update = caret_update
    9.36        }
    9.37      }
    9.38  
    9.39 -    client.onReady().then(() =>
    9.40 +    language_client.onReady().then(() =>
    9.41      {
    9.42        context.subscriptions.push(
    9.43          window.onDidChangeActiveTextEditor(_ => update_caret()),
    9.44 @@ -91,23 +92,21 @@
    9.45      dynamic_output.show(true)
    9.46      dynamic_output.hide()
    9.47  
    9.48 -    client.onReady().then(() =>
    9.49 +    language_client.onReady().then(() =>
    9.50      {
    9.51 -      client.onNotification(protocol.dynamic_output_type,
    9.52 +      language_client.onNotification(protocol.dynamic_output_type,
    9.53          params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
    9.54      })
    9.55  
    9.56  
    9.57 -    /* dynamic preview */
    9.58 +    /* preview */
    9.59  
    9.60 -    preview.init(context)
    9.61 -    client.onReady().then(() =>
    9.62 -      client.onNotification(protocol.dynamic_preview_type, params => preview.update(params.content)))
    9.63 +    language_client.onReady().then(() => preview.init(context, language_client))
    9.64  
    9.65  
    9.66      /* start server */
    9.67  
    9.68 -    context.subscriptions.push(client.start());
    9.69 +    context.subscriptions.push(language_client.start());
    9.70    }
    9.71  }
    9.72  
    10.1 --- a/src/Tools/VSCode/extension/src/library.ts	Wed May 31 11:49:29 2017 +0200
    10.2 +++ b/src/Tools/VSCode/extension/src/library.ts	Wed May 31 17:25:26 2017 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4  'use strict';
    10.5  
    10.6  import * as os from 'os';
    10.7 -import { ViewColumn, TextEditor, Uri, workspace } from 'vscode'
    10.8 +import { TextEditor, Uri, workspace } from 'vscode'
    10.9  
   10.10  
   10.11  /* platform information */
   10.12 @@ -32,13 +32,3 @@
   10.13    const config = color + (light ? "_light" : "_dark") + "_color"
   10.14    return get_configuration<string>(config)
   10.15  }
   10.16 -
   10.17 -
   10.18 -/* text editor column */
   10.19 -
   10.20 -export function other_column(active_editor: TextEditor | null): ViewColumn
   10.21 -{
   10.22 -  if (!active_editor || active_editor.viewColumn === ViewColumn.Three) return ViewColumn.One
   10.23 -  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
   10.24 -  else return ViewColumn.Three
   10.25 -}
    11.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 11:49:29 2017 +0200
    11.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 17:25:26 2017 +0200
    11.3 @@ -1,14 +1,39 @@
    11.4  'use strict';
    11.5  
    11.6  import * as timers from 'timers'
    11.7 -import { TextDocument, TextEditor, TextDocumentContentProvider, ExtensionContext,
    11.8 -  Event, EventEmitter, Uri, Position, workspace, window, commands } from 'vscode'
    11.9 +import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
   11.10 +  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
   11.11 +  window, commands } from 'vscode'
   11.12 +import { LanguageClient } from 'vscode-languageclient';
   11.13  import * as library from './library'
   11.14 +import * as protocol from './protocol';
   11.15 +
   11.16 +
   11.17 +/* Uri information */
   11.18 +
   11.19 +const preview_uri_template = Uri.parse("isabelle-preview:Preview")
   11.20 +const preview_uri_scheme = preview_uri_template.scheme
   11.21 +
   11.22 +function encode_preview(document_uri: Uri | undefined): Uri | undefined
   11.23 +{
   11.24 +  if (document_uri && library.is_file(document_uri)) {
   11.25 +    return preview_uri_template.with({ query: document_uri.fsPath })
   11.26 +  }
   11.27 +  else undefined
   11.28 +}
   11.29 +
   11.30 +function decode_preview(preview_uri: Uri | undefined): Uri | undefined
   11.31 +{
   11.32 +  if (preview_uri && preview_uri.scheme === preview_uri_scheme) {
   11.33 +    return Uri.file(preview_uri.query)
   11.34 +  }
   11.35 +  else undefined
   11.36 +}
   11.37  
   11.38  
   11.39  /* HTML content */
   11.40  
   11.41 -const preview_uri = Uri.parse("isabelle-preview:Preview")
   11.42 +const preview_content = new Map<string, string>()
   11.43  
   11.44  const default_preview_content =
   11.45    `<html>
   11.46 @@ -20,35 +45,86 @@
   11.47    </body>
   11.48    </html>`
   11.49  
   11.50 -let preview_content = default_preview_content
   11.51 -
   11.52  class Provider implements TextDocumentContentProvider
   11.53  {
   11.54    dispose() { }
   11.55  
   11.56    private emitter = new EventEmitter<Uri>()
   11.57 -  public update() { this.emitter.fire(preview_uri) }
   11.58 +  public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
   11.59    get onDidChange(): Event<Uri> { return this.emitter.event }
   11.60  
   11.61 -  provideTextDocumentContent(uri: Uri): string { return preview_content }
   11.62 -}
   11.63 -
   11.64 -export function update(content: string)
   11.65 -{
   11.66 -  preview_content = content === "" ? default_preview_content : content
   11.67 -  provider.update()
   11.68 -  commands.executeCommand("vscode.previewHtml", preview_uri,
   11.69 -    library.other_column(window.activeTextEditor), "Isabelle Preview")
   11.70 +  provideTextDocumentContent(preview_uri: Uri): string
   11.71 +  {
   11.72 +    return preview_content.get(preview_uri.toString()) || default_preview_content
   11.73 +  }
   11.74  }
   11.75  
   11.76  
   11.77  /* init */
   11.78  
   11.79 +let language_client: LanguageClient
   11.80  let provider: Provider
   11.81  
   11.82 -export function init(context: ExtensionContext)
   11.83 +export function init(context: ExtensionContext, client: LanguageClient)
   11.84  {
   11.85 +  language_client = client
   11.86 +
   11.87    provider = new Provider()
   11.88 -  context.subscriptions.push(workspace.registerTextDocumentContentProvider(preview_uri.scheme, provider))
   11.89 -  context.subscriptions.push(provider)
   11.90 +  context.subscriptions.push(
   11.91 +    workspace.registerTextDocumentContentProvider(preview_uri_scheme, provider),
   11.92 +    provider)
   11.93 +
   11.94 +  context.subscriptions.push(
   11.95 +    commands.registerCommand("isabelle.preview", uri => request_preview(uri, false)),
   11.96 +    commands.registerCommand("isabelle.preview-side", uri => request_preview(uri, true)),
   11.97 +    commands.registerCommand("isabelle.preview-source", show_source))
   11.98 +
   11.99 +  language_client.onNotification(protocol.preview_response_type,
  11.100 +    params => show_preview(Uri.parse(params.uri), params.column, params.label, params.content))
  11.101 +}
  11.102 +
  11.103 +
  11.104 +/* commands */
  11.105 +
  11.106 +function preview_column(side: boolean): ViewColumn
  11.107 +{
  11.108 +  const active_editor = window.activeTextEditor
  11.109 +
  11.110 +  if (!active_editor) return ViewColumn.One
  11.111 +  else if (!side) return active_editor.viewColumn
  11.112 +  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
  11.113 +  else return ViewColumn.Three
  11.114  }
  11.115 +
  11.116 +function request_preview(uri?: Uri, side: boolean = false)
  11.117 +{
  11.118 +  const document_uri = uri || window.activeTextEditor.document.uri
  11.119 +  const preview_uri = encode_preview(document_uri)
  11.120 +  if (preview_uri) {
  11.121 +    language_client.sendNotification(protocol.preview_request_type,
  11.122 +      {uri: document_uri.toString(), column: preview_column(side) })
  11.123 +  }
  11.124 +}
  11.125 +
  11.126 +function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string)
  11.127 +{
  11.128 +  const preview_uri = encode_preview(document_uri)
  11.129 +  if (preview_uri) {
  11.130 +    preview_content.set(preview_uri.toString(), content)
  11.131 +    commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
  11.132 +  }
  11.133 +}
  11.134 +
  11.135 +function show_source(preview_uri: Uri)
  11.136 +{
  11.137 +  const document_uri = decode_preview(preview_uri)
  11.138 +  if (document_uri) {
  11.139 +    const editor =
  11.140 +      window.visibleTextEditors.find(editor =>
  11.141 +        editor.document.uri.scheme === document_uri.scheme &&
  11.142 +        editor.document.uri.fsPath === document_uri.fsPath)
  11.143 +    if (editor) window.showTextDocument(editor.document, editor.viewColumn)
  11.144 +    else workspace.openTextDocument(document_uri).then(window.showTextDocument)
  11.145 +  }
  11.146 +  else commands.executeCommand("workbench.action.navigateBack")
  11.147 +}
    12.1 --- a/src/Tools/VSCode/extension/src/protocol.ts	Wed May 31 11:49:29 2017 +0200
    12.2 +++ b/src/Tools/VSCode/extension/src/protocol.ts	Wed May 31 17:25:26 2017 +0200
    12.3 @@ -46,12 +46,24 @@
    12.4    new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
    12.5  
    12.6  
    12.7 -/* dynamic preview */
    12.8 +/* preview */
    12.9  
   12.10 -export interface Dynamic_Preview
   12.11 +export interface Preview_Request
   12.12  {
   12.13 +  uri: string
   12.14 +  column: number
   12.15 +}
   12.16 +
   12.17 +export interface Preview_Response
   12.18 +{
   12.19 +  uri: string
   12.20 +  column: number
   12.21 +  label: string
   12.22    content: string
   12.23  }
   12.24  
   12.25 -export const dynamic_preview_type =
   12.26 -  new NotificationType<Dynamic_Preview, void>("PIDE/dynamic_preview")
   12.27 +export const preview_request_type =
   12.28 +  new NotificationType<Preview_Request, void>("PIDE/preview_request")
   12.29 +
   12.30 +export const preview_response_type =
   12.31 +  new NotificationType<Preview_Response, void>("PIDE/preview_response")
    13.1 --- a/src/Tools/VSCode/src/dynamic_preview.scala	Wed May 31 11:49:29 2017 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,99 +0,0 @@
    13.4 -/*  Title:      Tools/VSCode/src/dynamic_preview.scala
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -Dynamic preview, depending on caret document node.
    13.8 -*/
    13.9 -
   13.10 -package isabelle.vscode
   13.11 -
   13.12 -
   13.13 -import isabelle._
   13.14 -
   13.15 -import java.io.{File => JFile}
   13.16 -
   13.17 -
   13.18 -object Dynamic_Preview
   13.19 -{
   13.20 -  def make_preview(model: Document_Model, snapshot: Document.Snapshot): XML.Body =
   13.21 -    List(
   13.22 -      HTML.chapter("Preview " + model.node_name),
   13.23 -      HTML.itemize(
   13.24 -        snapshot.node.commands.toList.flatMap(
   13.25 -          command =>
   13.26 -            if (command.span.name == "") None
   13.27 -            else Some(HTML.text(command.span.name)))))
   13.28 -
   13.29 -  object State
   13.30 -  {
   13.31 -    val init: State = State()
   13.32 -  }
   13.33 -
   13.34 -  sealed case class State(file: Option[JFile] = None, body: XML.Body = Nil)
   13.35 -  {
   13.36 -    def handle_update(
   13.37 -      resources: VSCode_Resources,
   13.38 -      channel: Channel,
   13.39 -      changed: Option[Set[Document.Node.Name]]): State =
   13.40 -    {
   13.41 -      val st1 =
   13.42 -        if (resources.options.bool("vscode_caret_preview")) {
   13.43 -          resources.get_caret() match {
   13.44 -            case Some((caret_file, caret_model, _)) =>
   13.45 -              if (file != Some(caret_file) ||
   13.46 -                  changed.isDefined && changed.get.contains(caret_model.node_name))
   13.47 -              {
   13.48 -                val snapshot = caret_model.snapshot()
   13.49 -                if (!snapshot.is_outdated)
   13.50 -                  State(Some(caret_file), make_preview(caret_model, snapshot))
   13.51 -                else this
   13.52 -              }
   13.53 -              else this
   13.54 -            case None => State.init
   13.55 -          }
   13.56 -        }
   13.57 -        else State.init
   13.58 -
   13.59 -      if (st1.body != body) {
   13.60 -        val content =
   13.61 -          if (st1.body.isEmpty) ""
   13.62 -          else HTML.output_document(Nil, st1.body, css = "")
   13.63 -        channel.write(Protocol.Dynamic_Preview(content))
   13.64 -      }
   13.65 -
   13.66 -      st1
   13.67 -    }
   13.68 -  }
   13.69 -
   13.70 -  def apply(server: Server): Dynamic_Preview = new Dynamic_Preview(server)
   13.71 -}
   13.72 -
   13.73 -
   13.74 -class Dynamic_Preview private(server: Server)
   13.75 -{
   13.76 -  private val state = Synchronized(Dynamic_Preview.State.init)
   13.77 -
   13.78 -  private def handle_update(changed: Option[Set[Document.Node.Name]])
   13.79 -  { state.change(_.handle_update(server.resources, server.channel, changed)) }
   13.80 -
   13.81 -
   13.82 -  /* main */
   13.83 -
   13.84 -  private val main =
   13.85 -    Session.Consumer[Any](getClass.getName) {
   13.86 -      case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
   13.87 -      case Session.Caret_Focus => handle_update(None)
   13.88 -    }
   13.89 -
   13.90 -  def init()
   13.91 -  {
   13.92 -    server.session.commands_changed += main
   13.93 -    server.session.caret_focus += main
   13.94 -    handle_update(None)
   13.95 -  }
   13.96 -
   13.97 -  def exit()
   13.98 -  {
   13.99 -    server.session.commands_changed -= main
  13.100 -    server.session.caret_focus -= main
  13.101 -  }
  13.102 -}
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/VSCode/src/preview.scala	Wed May 31 17:25:26 2017 +0200
    14.3 @@ -0,0 +1,58 @@
    14.4 +/*  Title:      Tools/VSCode/src/preview.scala
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +HTML document preview.
    14.8 +*/
    14.9 +
   14.10 +package isabelle.vscode
   14.11 +
   14.12 +
   14.13 +import isabelle._
   14.14 +
   14.15 +import java.io.{File => JFile}
   14.16 +
   14.17 +
   14.18 +class Preview(resources: VSCode_Resources)
   14.19 +{
   14.20 +  private val pending = Synchronized(Map.empty[JFile, Int])
   14.21 +
   14.22 +  def request(file: JFile, column: Int): Unit =
   14.23 +    pending.change(map => map + (file -> column))
   14.24 +
   14.25 +  def flush(channel: Channel): Boolean =
   14.26 +  {
   14.27 +    pending.change_result(map =>
   14.28 +    {
   14.29 +      val map1 =
   14.30 +        (map /: map.iterator)({ case (m, (file, column)) =>
   14.31 +          resources.get_model(file) match {
   14.32 +            case Some(model) =>
   14.33 +              val snapshot = model.snapshot()
   14.34 +              if (snapshot.is_outdated) m
   14.35 +              else {
   14.36 +                val (label, content) = make_preview(model, snapshot)
   14.37 +                channel.write(Protocol.Preview_Response(file, column, label, content))
   14.38 +                m - file
   14.39 +              }
   14.40 +            case None => m - file
   14.41 +          }
   14.42 +        })
   14.43 +      (map1.nonEmpty, map1)
   14.44 +    })
   14.45 +  }
   14.46 +
   14.47 +  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
   14.48 +  {
   14.49 +    val label = "Preview " + quote(model.node_name.toString)
   14.50 +    val content =
   14.51 +      HTML.output_document(head = Nil, css = "", body =
   14.52 +        List(
   14.53 +          HTML.chapter(label),
   14.54 +          HTML.itemize(
   14.55 +            snapshot.node.commands.toList.flatMap(
   14.56 +              command =>
   14.57 +                if (command.span.name == "") None
   14.58 +                else Some(HTML.text(command.span.name))))))
   14.59 +    (label, content)
   14.60 +  }
   14.61 +}
    15.1 --- a/src/Tools/VSCode/src/protocol.scala	Wed May 31 11:49:29 2017 +0200
    15.2 +++ b/src/Tools/VSCode/src/protocol.scala	Wed May 31 17:25:26 2017 +0200
    15.3 @@ -465,11 +465,30 @@
    15.4    }
    15.5  
    15.6  
    15.7 -  /* dynamic preview */
    15.8 +  /* preview */
    15.9  
   15.10 -  object Dynamic_Preview
   15.11 +  object Preview_Request
   15.12    {
   15.13 -    def apply(content: String): JSON.T =
   15.14 -      Notification("PIDE/dynamic_preview", Map("content" -> content))
   15.15 +    def unapply(json: JSON.T): Option[(JFile, Int)] =
   15.16 +      json match {
   15.17 +        case Notification("PIDE/preview_request", Some(params)) =>
   15.18 +          for {
   15.19 +            uri <- JSON.string(params, "uri")
   15.20 +            if Url.is_wellformed_file(uri)
   15.21 +            column <- JSON.int(params, "column")
   15.22 +          } yield (Url.canonical_file(uri), column)
   15.23 +        case _ => None
   15.24 +      }
   15.25 +  }
   15.26 +
   15.27 +  object Preview_Response
   15.28 +  {
   15.29 +    def apply(file: JFile, column: Int, label: String, content: String): JSON.T =
   15.30 +      Notification("PIDE/preview_response",
   15.31 +        Map(
   15.32 +          "uri" -> Url.print_file(file),
   15.33 +          "column" -> column,
   15.34 +          "label" -> label,
   15.35 +          "content" -> content))
   15.36    }
   15.37  }
    16.1 --- a/src/Tools/VSCode/src/server.scala	Wed May 31 11:49:29 2017 +0200
    16.2 +++ b/src/Tools/VSCode/src/server.scala	Wed May 31 17:25:26 2017 +0200
    16.3 @@ -105,7 +105,6 @@
    16.4      } yield (rendering, offset)
    16.5  
    16.6    private val dynamic_output = Dynamic_Output(this)
    16.7 -  private val dynamic_preview = Dynamic_Preview(this)
    16.8  
    16.9  
   16.10    /* input from client or file-system */
   16.11 @@ -177,6 +176,23 @@
   16.12    }
   16.13  
   16.14  
   16.15 +  /* preview */
   16.16 +
   16.17 +  private lazy val preview = new Preview(resources)
   16.18 +
   16.19 +  private lazy val delay_preview: Standard_Thread.Delay =
   16.20 +    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
   16.21 +    {
   16.22 +      if (preview.flush(channel)) delay_preview.invoke()
   16.23 +    }
   16.24 +
   16.25 +  private def request_preview(file: JFile, column: Int)
   16.26 +  {
   16.27 +    preview.request(file, column)
   16.28 +    delay_preview.invoke()
   16.29 +  }
   16.30 +
   16.31 +
   16.32    /* output to client */
   16.33  
   16.34    private val delay_output: Standard_Thread.Delay =
   16.35 @@ -251,7 +267,6 @@
   16.36        session.all_messages += syslog
   16.37  
   16.38        dynamic_output.init()
   16.39 -      dynamic_preview.init()
   16.40  
   16.41        var session_phase: Session.Consumer[Session.Phase] = null
   16.42        session_phase =
   16.43 @@ -281,13 +296,13 @@
   16.44          session.all_messages -= syslog
   16.45  
   16.46          dynamic_output.exit()
   16.47 -        dynamic_preview.exit()
   16.48  
   16.49          delay_load.revoke()
   16.50          file_watcher.shutdown()
   16.51          delay_input.revoke()
   16.52          delay_output.revoke()
   16.53          delay_caret_update.revoke()
   16.54 +        delay_preview.revoke()
   16.55  
   16.56          val rc = session.stop()
   16.57          if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc)
   16.58 @@ -382,6 +397,7 @@
   16.59            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
   16.60            case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
   16.61            case Protocol.Caret_Update(caret) => update_caret(caret)
   16.62 +          case Protocol.Preview_Request(file, column) => request_preview(file, column)
   16.63            case _ => log("### IGNORED")
   16.64          }
   16.65        }