# HG changeset patch
# User wenzelm
# Date 1498739964 -7200
# Node ID 9a8b6b86350c7618350c8deacc192daed7c3fddb
# Parent  eec1c99e1bdcf4ad31711ad4908670b28baf211f
proper hyperlink_command, notably for locate_query;
support bidirectional caret update;

diff -r eec1c99e1bdc -r 9a8b6b86350c src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 13:28:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 14:39:24 2017 +0200
@@ -9,9 +9,10 @@
 import * as state_panel from './state_panel';
 import * as symbol from './symbol';
 import * as completion from './completion';
-import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
-import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
-  from 'vscode-languageclient';
+import { Uri, Selection, Position, ExtensionContext, workspace, window, commands, languages }
+  from 'vscode';
+import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind,
+  NotificationType } from 'vscode-languageclient';
 
 
 let last_caret_update: protocol.Caret_Update = {}
@@ -79,12 +80,28 @@
       }
     }
 
+    function goto_file(caret_update: protocol.Caret_Update)
+    {
+      if (caret_update.uri) {
+        workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document =>
+        {
+          const editor = library.find_file_editor(document.uri)
+          if (editor) {
+            const pos = new Position(caret_update.line || 0, caret_update.character || 0)
+            editor.selections = [new Selection(pos, pos)]
+          }
+        })
+      }
+    }
+
     language_client.onReady().then(() =>
     {
       context.subscriptions.push(
         window.onDidChangeActiveTextEditor(_ => update_caret()),
         window.onDidChangeTextEditorSelection(_ => update_caret()))
       update_caret()
+
+      language_client.onNotification(protocol.caret_update_type, goto_file)
     })
 
 
diff -r eec1c99e1bdc -r 9a8b6b86350c src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 13:28:08 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Thu Jun 29 14:39:24 2017 +0200
@@ -29,15 +29,17 @@
 
 export function find_file_editor(uri: Uri): TextEditor | undefined
 {
+  function check(editor: TextEditor): boolean
+  { return editor && is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath }
+
   if (is_file(uri)) {
-    return window.visibleTextEditors.find(editor =>
-      is_file(editor.document.uri) && editor.document.uri.fsPath === uri.fsPath)
+    if (check(window.activeTextEditor)) return window.activeTextEditor
+    else return window.visibleTextEditors.find(check)
   }
   else return undefined
 }
 
 
-
 /* Isabelle configuration */
 
 export function get_configuration<T>(name: string): T
diff -r eec1c99e1bdc -r 9a8b6b86350c src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 13:28:08 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 14:39:24 2017 +0200
@@ -478,10 +478,19 @@
   }
 
 
-  /* caret handling */
+  /* caret update: bidirectional */
 
   object Caret_Update
   {
+    def apply(node_pos: Line.Node_Position): JSON.T =
+      Notification("PIDE/caret_update",
+        Map("uri" -> Url.print_file_name(node_pos.name),
+          "line" -> node_pos.pos.line,
+          "character" -> node_pos.pos.column))
+
+    def apply(file: JFile, pos: Line.Position): JSON.T =
+      apply(Line.Node_Position(file.getPath, pos))
+
     def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
       json match {
         case Notification("PIDE/caret_update", Some(params)) =>
diff -r eec1c99e1bdc -r 9a8b6b86350c src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Jun 29 13:28:08 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Jun 29 14:39:24 2017 +0200
@@ -527,8 +527,13 @@
     /* hyperlinks */
 
     override def hyperlink_command(
-      focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
-        : Option[Hyperlink] = None
+      focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic,
+      offset: Symbol.Offset = 0): Option[Hyperlink] =
+    {
+      if (snapshot.is_outdated) None
+      else snapshot.find_command_position(id, offset).map(node_pos =>
+        new Hyperlink { def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos)) } })
+    }
 
 
     /* dispatcher thread */