provide preview content on Scala side (similar to output);
authorwenzelm
Tue May 30 22:06:39 2017 +0200 (2017-05-30)
changeset 65977c51b74be23b6
parent 65976 1448d71fbd22
child 65978 5754708a2d05
provide preview content on Scala side (similar to output);
src/Pure/build-jars
src/Tools/VSCode/etc/options
src/Tools/VSCode/extension/src/extension.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/protocol.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Pure/build-jars	Tue May 30 21:38:38 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Tue May 30 22:06:39 2017 +0200
     1.3 @@ -167,6 +167,7 @@
     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/protocol.scala
    1.10    ../Tools/VSCode/src/server.scala
     2.1 --- a/src/Tools/VSCode/etc/options	Tue May 30 21:38:38 2017 +0200
     2.2 +++ b/src/Tools/VSCode/etc/options	Tue May 30 22:06:39 2017 +0200
     2.3 @@ -26,3 +26,6 @@
     2.4  
     2.5  option vscode_caret_perspective : int = 50
     2.6    -- "number of visible lines above and below the caret (0: unrestricted)"
     2.7 +
     2.8 +option vscode_caret_preview : bool = false
     2.9 +  -- "dynamic preview of caret document node"
     3.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 21:38:38 2017 +0200
     3.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 22:06:39 2017 +0200
     3.3 @@ -91,11 +91,11 @@
     3.4      })
     3.5  
     3.6  
     3.7 -    /* preview */
     3.8 +    /* dynamic preview */
     3.9  
    3.10      preview.init(context)
    3.11 -    context.subscriptions.push(
    3.12 -      workspace.onDidChangeTextDocument(event => preview.touch_document(event.document)))
    3.13 +    client.onReady().then(() =>
    3.14 +      client.onNotification(protocol.dynamic_preview_type, params => preview.update(params.content)))
    3.15  
    3.16  
    3.17      /* start server */
     4.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Tue May 30 21:38:38 2017 +0200
     4.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Tue May 30 22:06:39 2017 +0200
     4.3 @@ -6,49 +6,39 @@
     4.4  import * as library from './library'
     4.5  
     4.6  
     4.7 -/* generated content */
     4.8 +/* HTML content */
     4.9  
    4.10 -const uri_scheme = 'isabelle-preview';
    4.11 +const preview_uri = Uri.parse("isabelle-preview:Preview")
    4.12  
    4.13 -export function encode_preview(document_uri: Uri): Uri
    4.14 -{
    4.15 -  return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
    4.16 -}
    4.17 +const default_preview_content =
    4.18 +  `<html>
    4.19 +  <head>
    4.20 +    <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
    4.21 +  </head>
    4.22 +  <body>
    4.23 +    <h1>Isabelle Preview</h1>
    4.24 +  </body>
    4.25 +  </html>`
    4.26  
    4.27 -export function decode_preview(preview_uri: Uri): Uri
    4.28 -{
    4.29 -  const [name] = <[string]>JSON.parse(preview_uri.query)
    4.30 -  return Uri.parse(name)
    4.31 -}
    4.32 +let preview_content = default_preview_content
    4.33  
    4.34  class Provider implements TextDocumentContentProvider
    4.35  {
    4.36    dispose() { }
    4.37  
    4.38    private emitter = new EventEmitter<Uri>()
    4.39 -  public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
    4.40 +  public update() { this.emitter.fire(preview_uri) }
    4.41    get onDidChange(): Event<Uri> { return this.emitter.event }
    4.42  
    4.43 -  provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
    4.44 -  {
    4.45 -    const document_uri = decode_preview(preview_uri)
    4.46 -    const editor =
    4.47 -      window.visibleTextEditors.find(editor =>
    4.48 -        document_uri.toString() === editor.document.uri.toString())
    4.49 -    return `
    4.50 -      <html>
    4.51 -      <head>
    4.52 -        <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
    4.53 -      </head>
    4.54 -      <body>
    4.55 -        <h1>Isabelle Preview</h1>
    4.56 -        <ul>
    4.57 -        <li><b>file</b> = <code>${document_uri.fsPath}</code></li>` +
    4.58 -        (editor ? `<li><b>line count</b> = ${editor.document.lineCount}</li>` : "") +
    4.59 -        `</ul>
    4.60 -      </body>
    4.61 -      </html>`
    4.62 -  }
    4.63 +  provideTextDocumentContent(uri: Uri): string { return preview_content }
    4.64 +}
    4.65 +
    4.66 +export function update(content: string)
    4.67 +{
    4.68 +  preview_content = content === "" ? default_preview_content : content
    4.69 +  provider.update()
    4.70 +  commands.executeCommand("vscode.previewHtml", preview_uri,
    4.71 +    library.other_column(window.activeTextEditor), "Isabelle Preview")
    4.72  }
    4.73  
    4.74  
    4.75 @@ -59,39 +49,6 @@
    4.76  export function init(context: ExtensionContext)
    4.77  {
    4.78    provider = new Provider()
    4.79 -  context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
    4.80 +  context.subscriptions.push(workspace.registerTextDocumentContentProvider(preview_uri.scheme, provider))
    4.81    context.subscriptions.push(provider)
    4.82 -
    4.83 -  context.subscriptions.push(
    4.84 -    commands.registerTextEditorCommand("isabelle.preview", editor =>
    4.85 -    {
    4.86 -      const preview_uri = encode_preview(editor.document.uri)
    4.87 -      return workspace.openTextDocument(preview_uri).then(doc =>
    4.88 -        commands.executeCommand("vscode.previewHtml", preview_uri,
    4.89 -          library.other_column(window.activeTextEditor), "Isabelle Preview"))
    4.90 -    }))
    4.91  }
    4.92 -
    4.93 -
    4.94 -/* handle document changes */
    4.95 -
    4.96 -const touched_documents = new Set<TextDocument>()
    4.97 -let touched_timer: NodeJS.Timer
    4.98 -
    4.99 -function update_touched_documents()
   4.100 -{
   4.101 -  if (provider) {
   4.102 -    for (const document of touched_documents) {
   4.103 -      provider.update(encode_preview(document.uri))
   4.104 -    }
   4.105 -  }
   4.106 -}
   4.107 -
   4.108 -export function touch_document(document: TextDocument)
   4.109 -{
   4.110 -  if (library.is_file(document.uri) && document.languageId === 'isabelle') {
   4.111 -    if (touched_timer) timers.clearTimeout(touched_timer)
   4.112 -    touched_documents.add(document)
   4.113 -    touched_timer = timers.setTimeout(update_touched_documents, 300)
   4.114 -  }
   4.115 -}
     5.1 --- a/src/Tools/VSCode/extension/src/protocol.ts	Tue May 30 21:38:38 2017 +0200
     5.2 +++ b/src/Tools/VSCode/extension/src/protocol.ts	Tue May 30 22:06:39 2017 +0200
     5.3 @@ -44,3 +44,14 @@
     5.4  
     5.5  export const dynamic_output_type =
     5.6    new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
     5.7 +
     5.8 +
     5.9 +/* dynamic preview */
    5.10 +
    5.11 +export interface Dynamic_Preview
    5.12 +{
    5.13 +  content: string
    5.14 +}
    5.15 +
    5.16 +export const dynamic_preview_type =
    5.17 +  new NotificationType<Dynamic_Preview, void>("PIDE/dynamic_preview")
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/VSCode/src/dynamic_preview.scala	Tue May 30 22:06:39 2017 +0200
     6.3 @@ -0,0 +1,99 @@
     6.4 +/*  Title:      Tools/VSCode/src/dynamic_preview.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Dynamic preview, depending on caret document node.
     6.8 +*/
     6.9 +
    6.10 +package isabelle.vscode
    6.11 +
    6.12 +
    6.13 +import isabelle._
    6.14 +
    6.15 +import java.io.{File => JFile}
    6.16 +
    6.17 +
    6.18 +object Dynamic_Preview
    6.19 +{
    6.20 +  def make_preview(model: Document_Model, snapshot: Document.Snapshot): XML.Body =
    6.21 +    List(
    6.22 +      HTML.chapter("Preview " + model.node_name),
    6.23 +      HTML.itemize(
    6.24 +        snapshot.node.commands.toList.flatMap(
    6.25 +          command =>
    6.26 +            if (command.span.name == "") None
    6.27 +            else Some(HTML.text(command.span.name)))))
    6.28 +
    6.29 +  object State
    6.30 +  {
    6.31 +    val init: State = State()
    6.32 +  }
    6.33 +
    6.34 +  sealed case class State(file: Option[JFile] = None, body: XML.Body = Nil)
    6.35 +  {
    6.36 +    def handle_update(
    6.37 +      resources: VSCode_Resources,
    6.38 +      channel: Channel,
    6.39 +      changed: Option[Set[Document.Node.Name]]): State =
    6.40 +    {
    6.41 +      val st1 =
    6.42 +        if (resources.options.bool("vscode_caret_preview")) {
    6.43 +          resources.get_caret() match {
    6.44 +            case Some((caret_file, caret_model, _)) =>
    6.45 +              if (file != Some(caret_file) ||
    6.46 +                  changed.isDefined && changed.get.contains(caret_model.node_name))
    6.47 +              {
    6.48 +                val snapshot = caret_model.snapshot()
    6.49 +                if (!snapshot.is_outdated)
    6.50 +                  State(Some(caret_file), make_preview(caret_model, snapshot))
    6.51 +                else this
    6.52 +              }
    6.53 +              else this
    6.54 +            case None => State.init
    6.55 +          }
    6.56 +        }
    6.57 +        else State.init
    6.58 +
    6.59 +      if (st1.body != body) {
    6.60 +        val content =
    6.61 +          if (st1.body.isEmpty) ""
    6.62 +          else HTML.output_document(Nil, st1.body, css = "")
    6.63 +        channel.write(Protocol.Dynamic_Preview(content))
    6.64 +      }
    6.65 +
    6.66 +      st1
    6.67 +    }
    6.68 +  }
    6.69 +
    6.70 +  def apply(server: Server): Dynamic_Preview = new Dynamic_Preview(server)
    6.71 +}
    6.72 +
    6.73 +
    6.74 +class Dynamic_Preview private(server: Server)
    6.75 +{
    6.76 +  private val state = Synchronized(Dynamic_Preview.State.init)
    6.77 +
    6.78 +  private def handle_update(changed: Option[Set[Document.Node.Name]])
    6.79 +  { state.change(_.handle_update(server.resources, server.channel, changed)) }
    6.80 +
    6.81 +
    6.82 +  /* main */
    6.83 +
    6.84 +  private val main =
    6.85 +    Session.Consumer[Any](getClass.getName) {
    6.86 +      case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
    6.87 +      case Session.Caret_Focus => handle_update(None)
    6.88 +    }
    6.89 +
    6.90 +  def init()
    6.91 +  {
    6.92 +    server.session.commands_changed += main
    6.93 +    server.session.caret_focus += main
    6.94 +    handle_update(None)
    6.95 +  }
    6.96 +
    6.97 +  def exit()
    6.98 +  {
    6.99 +    server.session.commands_changed -= main
   6.100 +    server.session.caret_focus -= main
   6.101 +  }
   6.102 +}
     7.1 --- a/src/Tools/VSCode/src/protocol.scala	Tue May 30 21:38:38 2017 +0200
     7.2 +++ b/src/Tools/VSCode/src/protocol.scala	Tue May 30 22:06:39 2017 +0200
     7.3 @@ -463,4 +463,13 @@
     7.4      def apply(body: String): JSON.T =
     7.5        Notification("PIDE/dynamic_output", Map("body" -> body))
     7.6    }
     7.7 +
     7.8 +
     7.9 +  /* dynamic preview */
    7.10 +
    7.11 +  object Dynamic_Preview
    7.12 +  {
    7.13 +    def apply(content: String): JSON.T =
    7.14 +      Notification("PIDE/dynamic_preview", Map("content" -> content))
    7.15 +  }
    7.16  }
     8.1 --- a/src/Tools/VSCode/src/server.scala	Tue May 30 21:38:38 2017 +0200
     8.2 +++ b/src/Tools/VSCode/src/server.scala	Tue May 30 22:06:39 2017 +0200
     8.3 @@ -105,6 +105,7 @@
     8.4      } yield (rendering, offset)
     8.5  
     8.6    private val dynamic_output = Dynamic_Output(this)
     8.7 +  private val dynamic_preview = Dynamic_Preview(this)
     8.8  
     8.9  
    8.10    /* input from client or file-system */
    8.11 @@ -250,6 +251,7 @@
    8.12        session.all_messages += syslog
    8.13  
    8.14        dynamic_output.init()
    8.15 +      dynamic_preview.init()
    8.16  
    8.17        var session_phase: Session.Consumer[Session.Phase] = null
    8.18        session_phase =
    8.19 @@ -279,6 +281,7 @@
    8.20          session.all_messages -= syslog
    8.21  
    8.22          dynamic_output.exit()
    8.23 +        dynamic_preview.exit()
    8.24  
    8.25          delay_load.revoke()
    8.26          file_watcher.shutdown()