clarified modules;
authorwenzelm
Tue Jun 13 15:11:01 2017 +0200 (2017-06-13)
changeset 66081441f95b05944
parent 66080 066f4ba9c965
child 66082 2d12a730a380
clarified modules;
src/Tools/VSCode/extension/src/library.ts
src/Tools/VSCode/extension/src/preview.ts
     1.1 --- a/src/Tools/VSCode/extension/src/library.ts	Tue Jun 13 11:53:24 2017 +0200
     1.2 +++ b/src/Tools/VSCode/extension/src/library.ts	Tue Jun 13 15:11:01 2017 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  'use strict';
     1.5  
     1.6  import * as os from 'os';
     1.7 -import { TextEditor, Uri, workspace } from 'vscode'
     1.8 +import { TextEditor, Uri, ViewColumn, workspace } from 'vscode'
     1.9  
    1.10  
    1.11  /* regular expressions */
    1.12 @@ -40,3 +40,15 @@
    1.13    const config = color + (light ? "_light" : "_dark") + "_color"
    1.14    return get_configuration<string>(config)
    1.15  }
    1.16 +
    1.17 +
    1.18 +/* GUI */
    1.19 +
    1.20 +export function adjacent_editor_column(editor: TextEditor, split: boolean): ViewColumn
    1.21 +{
    1.22 +  if (!editor) return ViewColumn.One
    1.23 +  else if (!split) return editor.viewColumn
    1.24 +  else if (editor.viewColumn === ViewColumn.One || editor.viewColumn === ViewColumn.Three)
    1.25 +    return ViewColumn.Two
    1.26 +  else return ViewColumn.Three
    1.27 +}
     2.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 11:53:24 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Tue Jun 13 15:11:01 2017 +0200
     2.3 @@ -85,24 +85,14 @@
     2.4  
     2.5  /* commands */
     2.6  
     2.7 -function preview_column(split: boolean): ViewColumn
     2.8 -{
     2.9 -  const active_editor = window.activeTextEditor
    2.10 -
    2.11 -  if (!active_editor) return ViewColumn.One
    2.12 -  else if (!split) return active_editor.viewColumn
    2.13 -  else if (active_editor.viewColumn === ViewColumn.One ||
    2.14 -    active_editor.viewColumn === ViewColumn.Three) return ViewColumn.Two
    2.15 -  else return ViewColumn.Three
    2.16 -}
    2.17 -
    2.18  export function request(uri?: Uri, split: boolean = false)
    2.19  {
    2.20    const document_uri = uri || window.activeTextEditor.document.uri
    2.21    const preview_uri = encode_preview(document_uri)
    2.22    if (preview_uri && language_client) {
    2.23      language_client.sendNotification(protocol.preview_request_type,
    2.24 -      { uri: document_uri.toString(), column: preview_column(split) })
    2.25 +      { uri: document_uri.toString(),
    2.26 +        column: library.adjacent_editor_column(window.activeTextEditor, split) })
    2.27    }
    2.28  }
    2.29