# HG changeset patch
# User wenzelm
# Date 1498741960 -7200
# Node ID d4949bae0badd1839459b09a0aead62fe8dd8243
# Parent  9a8b6b86350c7618350c8deacc192daed7c3fddb
clarified editor focus;

diff -r 9a8b6b86350c -r d4949bae0bad src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 14:39:24 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 29 15:12:40 2017 +0200
@@ -9,8 +9,8 @@
 import * as state_panel from './state_panel';
 import * as symbol from './symbol';
 import * as completion from './completion';
-import { Uri, Selection, Position, ExtensionContext, workspace, window, commands, languages }
-  from 'vscode';
+import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window,
+  commands, languages } from 'vscode';
 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind,
   NotificationType } from 'vscode-languageclient';
 
@@ -82,14 +82,18 @@
 
     function goto_file(caret_update: protocol.Caret_Update)
     {
+      function move_cursor(editor: TextEditor)
+      {
+        const pos = new Position(caret_update.line || 0, caret_update.character || 0)
+        editor.selections = [new Selection(pos, pos)]
+      }
+
       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)]
-          }
+          const column = editor ? editor.viewColumn : ViewColumn.One
+          window.showTextDocument(document, column, !caret_update.focus).then(move_cursor)
         })
       }
     }
diff -r 9a8b6b86350c -r d4949bae0bad src/Tools/VSCode/extension/src/protocol.ts
--- a/src/Tools/VSCode/extension/src/protocol.ts	Thu Jun 29 14:39:24 2017 +0200
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Thu Jun 29 15:12:40 2017 +0200
@@ -30,6 +30,7 @@
   uri?: string
   line?: number
   character?: number
+  focus?: boolean
 }
 
 export const caret_update_type =
diff -r 9a8b6b86350c -r d4949bae0bad src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 14:39:24 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Thu Jun 29 15:12:40 2017 +0200
@@ -482,14 +482,12 @@
 
   object Caret_Update
   {
-    def apply(node_pos: Line.Node_Position): JSON.T =
+    def apply(node_pos: Line.Node_Position, focus: Boolean): 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))
+          "character" -> node_pos.pos.column,
+          "focus" -> focus))
 
     def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
       json match {
diff -r 9a8b6b86350c -r d4949bae0bad src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Jun 29 14:39:24 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Jun 29 15:12:40 2017 +0200
@@ -531,8 +531,11 @@
       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)) } })
+      else
+        snapshot.find_command_position(id, offset).map(node_pos =>
+          new Hyperlink {
+            def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) }
+          })
     }