basic support for VSCode Language Server protocol;
authorwenzelm
Mon Dec 19 20:27:49 2016 +0100 (2016-12-19)
changeset 646059c1173a7e4cb
parent 64604 2bf8cfc98c4d
child 64606 a871fa7c24fc
basic support for VSCode Language Server protocol;
minimal extension for VSCode editor;
.hgignore
src/Pure/System/isabelle_tool.scala
src/Pure/build-jars
src/Tools/VSCode/README.md
src/Tools/VSCode/extension/.vscode/launch.json
src/Tools/VSCode/extension/.vscode/settings.json
src/Tools/VSCode/extension/.vscode/tasks.json
src/Tools/VSCode/extension/.vscodeignore
src/Tools/VSCode/extension/README.md
src/Tools/VSCode/extension/isabelle.png
src/Tools/VSCode/extension/language-configuration.json
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/test/extension.test.ts
src/Tools/VSCode/extension/test/index.ts
src/Tools/VSCode/extension/tsconfig.json
src/Tools/VSCode/extension/vsc-extension-quickstart.md
src/Tools/VSCode/src/channel.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/line.scala
src/Tools/VSCode/src/logger.scala
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/uri_resources.scala
     1.1 --- a/.hgignore	Sun Dec 18 23:43:50 2016 +0100
     1.2 +++ b/.hgignore	Mon Dec 19 20:27:49 2016 +0100
     1.3 @@ -20,5 +20,8 @@
     1.4  ^doc/.*\.pdf
     1.5  ^doc/.*\.ps
     1.6  ^src/Tools/jEdit/dist/
     1.7 +^src/Tools/VSCode/out/
     1.8 +^src/Tools/VSCode/extension/node_modules/
     1.9 +^src/Tools/VSCode/extension/protocol.log
    1.10  ^Admin/jenkins/ci-extras/target/
    1.11  ^stats/
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Dec 18 23:43:50 2016 +0100
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Mon Dec 19 20:27:49 2016 +0100
     2.3 @@ -113,7 +113,8 @@
     2.4        Update_Cartouches.isabelle_tool,
     2.5        Update_Header.isabelle_tool,
     2.6        Update_Then.isabelle_tool,
     2.7 -      Update_Theorems.isabelle_tool)
     2.8 +      Update_Theorems.isabelle_tool,
     2.9 +      isabelle.vscode.Server.isabelle_tool)
    2.10  
    2.11    private def list_internal(): List[(String, String)] =
    2.12      for (tool <- internal_tools.toList if tool.accessible)
     3.1 --- a/src/Pure/build-jars	Sun Dec 18 23:43:50 2016 +0100
     3.2 +++ b/src/Pure/build-jars	Mon Dec 19 20:27:49 2016 +0100
     3.3 @@ -153,6 +153,13 @@
     3.4    "../Tools/Graphview/popups.scala"
     3.5    "../Tools/Graphview/shapes.scala"
     3.6    "../Tools/Graphview/tree_panel.scala"
     3.7 +  "../Tools/VSCode/src/channel.scala"
     3.8 +  "../Tools/VSCode/src/document_model.scala"
     3.9 +  "../Tools/VSCode/src/line.scala"
    3.10 +  "../Tools/VSCode/src/logger.scala"
    3.11 +  "../Tools/VSCode/src/protocol.scala"
    3.12 +  "../Tools/VSCode/src/server.scala"
    3.13 +  "../Tools/VSCode/src/uri_resources.scala"
    3.14  )
    3.15  
    3.16  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/README.md	Mon Dec 19 20:27:49 2016 +0100
     4.3 @@ -0,0 +1,58 @@
     4.4 +# Isabelle/PIDE for Visual Studio Code editor #
     4.5 +
     4.6 +* Extension for the editor ([TypeScript](extension/src/extension.ts))
     4.7 +* Language Server protocol implementation ([Isabelle/Scala](src/server.scala))
     4.8 +
     4.9 +
    4.10 +## Build and run ##
    4.11 +
    4.12 +* shell> `isabelle build -b HOL`
    4.13 +
    4.14 +* shell> `cd src/Tools/VSCode/extension; vsce package`
    4.15 +
    4.16 +* Preferences / User settings / edit settings.json: e.g.
    4.17 +    `"isabelle.home": "/home/makarius/isabelle/repos"`
    4.18 +
    4.19 +* Extensions / ... / Install from VSIX: `src/Tools/VSCode/extension/isabelle-0.0.1.vsix`
    4.20 +
    4.21 +* File / Open Folder: e.g. `src/HOL/Isar_Examples/` then open .thy files
    4.22 +
    4.23 +
    4.24 +## Debug
    4.25 +
    4.26 +* shell> `code src/Tools/VSCode/extension`
    4.27 +
    4.28 +* View / Debug / Launch Extension
    4.29 +
    4.30 +* File / Open Folder: e.g. `src/HOL/Isar_Examples/` then open .thy files
    4.31 +
    4.32 +
    4.33 +## Relevant links ##
    4.34 +
    4.35 +### VSCode editor ###
    4.36 +
    4.37 +* https://code.visualstudio.com
    4.38 +* https://code.visualstudio.com/docs/extensionAPI/extension-points
    4.39 +* https://code.visualstudio.com/docs/extensions/example-language-server
    4.40 +* https://github.com/Microsoft/vscode-languageserver-node-example
    4.41 +
    4.42 +
    4.43 +### Protocol ###
    4.44 +
    4.45 +* https://code.visualstudio.com/blogs/2016/06/27/common-language-protocol
    4.46 +* https://github.com/Microsoft/vscode-languageserver-node
    4.47 +* https://github.com/Microsoft/language-server-protocol
    4.48 +* https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
    4.49 +* http://www.jsonrpc.org/specification
    4.50 +* http://www.json.org
    4.51 +
    4.52 +
    4.53 +### Similar projects ###
    4.54 +
    4.55 +* Coq: https://github.com/siegebell/vscoq
    4.56 +* OCaml: https://github.com/freebroccolo/vscode-reasonml
    4.57 +* Scala: https://github.com/dragos/dragos-vscode-scala
    4.58 +* Rust:
    4.59 +    * https://github.com/jonathandturner/rls
    4.60 +    * https://github.com/jonathandturner/rls_vscode
    4.61 +    * https://github.com/RustDT/RustLSP
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/VSCode/extension/.vscode/launch.json	Mon Dec 19 20:27:49 2016 +0100
     5.3 @@ -0,0 +1,28 @@
     5.4 +// A launch configuration that compiles the extension and then opens it inside a new window
     5.5 +{
     5.6 +    "version": "0.1.0",
     5.7 +    "configurations": [
     5.8 +        {
     5.9 +            "name": "Launch Extension",
    5.10 +            "type": "extensionHost",
    5.11 +            "request": "launch",
    5.12 +            "runtimeExecutable": "${execPath}",
    5.13 +            "args": ["--extensionDevelopmentPath=${workspaceRoot}" ],
    5.14 +            "stopOnEntry": false,
    5.15 +            "sourceMaps": true,
    5.16 +            "outDir": "${workspaceRoot}/out/src",
    5.17 +            "preLaunchTask": "npm"
    5.18 +        },
    5.19 +        {
    5.20 +            "name": "Launch Tests",
    5.21 +            "type": "extensionHost",
    5.22 +            "request": "launch",
    5.23 +            "runtimeExecutable": "${execPath}",
    5.24 +            "args": ["--extensionDevelopmentPath=${workspaceRoot}", "--extensionTestsPath=${workspaceRoot}/out/test" ],
    5.25 +            "stopOnEntry": false,
    5.26 +            "sourceMaps": true,
    5.27 +            "outDir": "${workspaceRoot}/out/test",
    5.28 +            "preLaunchTask": "npm"
    5.29 +        }
    5.30 +    ]
    5.31 +}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/VSCode/extension/.vscode/settings.json	Mon Dec 19 20:27:49 2016 +0100
     6.3 @@ -0,0 +1,10 @@
     6.4 +// Place your settings in this file to overwrite default and user settings.
     6.5 +{
     6.6 +    "files.exclude": {
     6.7 +        "out": false // set this to true to hide the "out" folder with the compiled JS files
     6.8 +    },
     6.9 +    "search.exclude": {
    6.10 +        "out": true // set this to false to include "out" folder in search results
    6.11 +    },
    6.12 +    "typescript.tsdk": "./node_modules/typescript/lib" // we want to use the TS server from our node_modules folder to control its version
    6.13 +}
    6.14 \ 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/.vscode/tasks.json	Mon Dec 19 20:27:49 2016 +0100
     7.3 @@ -0,0 +1,30 @@
     7.4 +// Available variables which can be used inside of strings.
     7.5 +// ${workspaceRoot}: the root folder of the team
     7.6 +// ${file}: the current opened file
     7.7 +// ${fileBasename}: the current opened file's basename
     7.8 +// ${fileDirname}: the current opened file's dirname
     7.9 +// ${fileExtname}: the current opened file's extension
    7.10 +// ${cwd}: the current working directory of the spawned process
    7.11 +
    7.12 +// A task runner that calls a custom npm script that compiles the extension.
    7.13 +{
    7.14 +    "version": "0.1.0",
    7.15 +
    7.16 +    // we want to run npm
    7.17 +    "command": "npm",
    7.18 +
    7.19 +    // the command is a shell script
    7.20 +    "isShellCommand": true,
    7.21 +
    7.22 +    // show the output window only if unrecognized errors occur.
    7.23 +    "showOutput": "silent",
    7.24 +
    7.25 +    // we run the custom script "compile" as defined in package.json
    7.26 +    "args": ["run", "compile", "--loglevel", "silent"],
    7.27 +
    7.28 +    // The tsc compiler is started in watching mode
    7.29 +    "isWatching": true,
    7.30 +
    7.31 +    // use the standard tsc in watch mode problem matcher to find compile problems in the output.
    7.32 +    "problemMatcher": "$tsc-watch"
    7.33 +}
    7.34 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/VSCode/extension/.vscodeignore	Mon Dec 19 20:27:49 2016 +0100
     8.3 @@ -0,0 +1,9 @@
     8.4 +.vscode/**
     8.5 +.vscode-test/**
     8.6 +out/test/**
     8.7 +test/**
     8.8 +src/**
     8.9 +**/*.map
    8.10 +.gitignore
    8.11 +tsconfig.json
    8.12 +vsc-extension-quickstart.md
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/VSCode/extension/README.md	Mon Dec 19 20:27:49 2016 +0100
     9.3 @@ -0,0 +1,6 @@
     9.4 +# Isabelle language support
     9.5 +
     9.6 +This extension provides language support for Isabelle.
     9.7 +
     9.8 +Make sure that User Settings `isabelle.home` points to the ISABELLE_HOME
     9.9 +directory.
    10.1 Binary file src/Tools/VSCode/extension/isabelle.png has changed
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/VSCode/extension/language-configuration.json	Mon Dec 19 20:27:49 2016 +0100
    11.3 @@ -0,0 +1,16 @@
    11.4 +{
    11.5 +    "brackets": [
    11.6 +        ["(", ")"],
    11.7 +        ["[", "]"],
    11.8 +        ["{", "}"],
    11.9 +        ["<", ">"],
   11.10 +        ["«", "»"],
   11.11 +        ["‹", "›"],
   11.12 +        ["⟨", "⟩"],
   11.13 +        ["⌈", "⌉"],
   11.14 +        ["⌊", "⌋"],
   11.15 +        ["⦇", "⦈"],
   11.16 +        ["⟦", "⟧"],
   11.17 +        ["⦃", "⦄"]
   11.18 +    ]
   11.19 +}
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Tools/VSCode/extension/package.json	Mon Dec 19 20:27:49 2016 +0100
    12.3 @@ -0,0 +1,58 @@
    12.4 +{
    12.5 +    "name": "isabelle",
    12.6 +    "displayName": "Isabelle",
    12.7 +    "description": "Isabelle Theorem Prover",
    12.8 +    "keywords": [
    12.9 +        "theorem prover",
   12.10 +        "formalized mathematics",
   12.11 +        "mathematical logic",
   12.12 +        "functional programming",
   12.13 +        "document preparation"
   12.14 +        ],
   12.15 +    "icon": "isabelle.png",
   12.16 +    "version": "0.0.1",
   12.17 +    "publisher": "Makarius",
   12.18 +    "license": "BSD-3-Clause",
   12.19 +    "repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" },
   12.20 +    "engines": { "vscode": "^1.5.0" },
   12.21 +    "categories": ["Languages"],
   12.22 +    "activationEvents": [
   12.23 +        "onLanguage:isabelle"
   12.24 +    ],
   12.25 +    "main": "./out/src/extension",
   12.26 +    "contributes": {
   12.27 +        "languages": [
   12.28 +            {
   12.29 +                "id": "isabelle",
   12.30 +                "aliases": ["Isabelle"],
   12.31 +                "extensions": [".thy"],
   12.32 +                "configuration": "./language-configuration.json"
   12.33 +            }
   12.34 +        ],
   12.35 +        "configuration": {
   12.36 +            "title": "Isabelle",
   12.37 +            "properties": {
   12.38 +                "isabelle.home": {
   12.39 +                    "type": "string",
   12.40 +                    "default": "",
   12.41 +                    "description": "ISABELLE_HOME directory"
   12.42 +                }
   12.43 +            }
   12.44 +        }
   12.45 +    },
   12.46 +    "scripts": {
   12.47 +        "vscode:prepublish": "tsc -p ./",
   12.48 +        "compile": "tsc -watch -p ./",
   12.49 +        "postinstall": "node ./node_modules/vscode/bin/install"
   12.50 +    },
   12.51 +    "devDependencies": {
   12.52 +        "typescript": "^2.0.3",
   12.53 +        "vscode": "^1.0.0",
   12.54 +        "mocha": "^2.3.3",
   12.55 +        "@types/node": "^6.0.40",
   12.56 +        "@types/mocha": "^2.2.32"
   12.57 +    },
   12.58 +    "dependencies": {
   12.59 +        "vscode-languageclient": "^2.6.3"
   12.60 +    }
   12.61 +}
   12.62 \ No newline at end of file
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Mon Dec 19 20:27:49 2016 +0100
    13.3 @@ -0,0 +1,32 @@
    13.4 +'use strict';
    13.5 +
    13.6 +import * as vscode from 'vscode';
    13.7 +import * as path from 'path';
    13.8 +
    13.9 +import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind }
   13.10 +  from 'vscode-languageclient';
   13.11 +
   13.12 +
   13.13 +export function activate(context: vscode.ExtensionContext)
   13.14 +{
   13.15 +  let isabelle_home = vscode.workspace.getConfiguration("isabelle").get("home");
   13.16 +
   13.17 +  let run = {
   13.18 +    command: path.join(isabelle_home, "bin", "isabelle"),
   13.19 +    args: ["vscode_server"]
   13.20 +  };
   13.21 +  let server_options: ServerOptions =
   13.22 +  {
   13.23 +    run: run,
   13.24 +    debug: {
   13.25 +      command: run.command,
   13.26 +      args: run.args.concat(["-L", path.join(context.extensionPath, "protocol.log")]) }
   13.27 +  };
   13.28 +  let client_options: LanguageClientOptions = { documentSelector: "isabelle" };
   13.29 +
   13.30 +  let disposable =
   13.31 +    new LanguageClient("Isabelle Language Service", server_options, client_options, false).start();
   13.32 +  context.subscriptions.push(disposable);
   13.33 +}
   13.34 +
   13.35 +export function deactivate() { }
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/VSCode/extension/test/extension.test.ts	Mon Dec 19 20:27:49 2016 +0100
    14.3 @@ -0,0 +1,22 @@
    14.4 +//
    14.5 +// Note: This example test is leveraging the Mocha test framework.
    14.6 +// Please refer to their documentation on https://mochajs.org/ for help.
    14.7 +//
    14.8 +
    14.9 +// The module 'assert' provides assertion methods from node
   14.10 +import * as assert from 'assert';
   14.11 +
   14.12 +// You can import and use all API from the 'vscode' module
   14.13 +// as well as import your extension to test it
   14.14 +import * as vscode from 'vscode';
   14.15 +import * as myExtension from '../src/extension';
   14.16 +
   14.17 +// Defines a Mocha test suite to group tests of similar kind together
   14.18 +suite("Extension Tests", () => {
   14.19 +
   14.20 +    // Defines a Mocha unit test
   14.21 +    test("Something 1", () => {
   14.22 +        assert.equal(-1, [1, 2, 3].indexOf(5));
   14.23 +        assert.equal(-1, [1, 2, 3].indexOf(0));
   14.24 +    });
   14.25 +});
   14.26 \ No newline at end of file
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Tools/VSCode/extension/test/index.ts	Mon Dec 19 20:27:49 2016 +0100
    15.3 @@ -0,0 +1,22 @@
    15.4 +//
    15.5 +// PLEASE DO NOT MODIFY / DELETE UNLESS YOU KNOW WHAT YOU ARE DOING
    15.6 +//
    15.7 +// This file is providing the test runner to use when running extension tests.
    15.8 +// By default the test runner in use is Mocha based.
    15.9 +//
   15.10 +// You can provide your own test runner if you want to override it by exporting
   15.11 +// a function run(testRoot: string, clb: (error:Error) => void) that the extension
   15.12 +// host can call to run the tests. The test runner is expected to use console.log
   15.13 +// to report the results back to the caller. When the tests are finished, return
   15.14 +// a possible error to the callback or null if none.
   15.15 +
   15.16 +var testRunner = require('vscode/lib/testrunner');
   15.17 +
   15.18 +// You can directly control Mocha options by uncommenting the following lines
   15.19 +// See https://github.com/mochajs/mocha/wiki/Using-mocha-programmatically#set-options for more info
   15.20 +testRunner.configure({
   15.21 +    ui: 'tdd', 		// the TDD UI is being used in extension.test.ts (suite, test, etc.)
   15.22 +    useColors: true // colored output from test results
   15.23 +});
   15.24 +
   15.25 +module.exports = testRunner;
   15.26 \ No newline at end of file
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/VSCode/extension/tsconfig.json	Mon Dec 19 20:27:49 2016 +0100
    16.3 @@ -0,0 +1,16 @@
    16.4 +{
    16.5 +    "compilerOptions": {
    16.6 +        "module": "commonjs",
    16.7 +        "target": "es6",
    16.8 +        "outDir": "out",
    16.9 +        "lib": [
   16.10 +            "es6"
   16.11 +        ],
   16.12 +        "sourceMap": true,
   16.13 +        "rootDir": "."
   16.14 +    },
   16.15 +    "exclude": [
   16.16 +        "node_modules",
   16.17 +        ".vscode-test"
   16.18 +    ]
   16.19 +}
   16.20 \ No newline at end of file
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/VSCode/extension/vsc-extension-quickstart.md	Mon Dec 19 20:27:49 2016 +0100
    17.3 @@ -0,0 +1,33 @@
    17.4 +# Welcome to your first VS Code Extension
    17.5 +
    17.6 +## What's in the folder
    17.7 +* This folder contains all of the files necessary for your extension
    17.8 +* `package.json` - this is the manifest file in which you declare your extension and command.
    17.9 +The sample plugin registers a command and defines its title and command name. With this information
   17.10 +VS Code can show the command in the command palette. It doesn’t yet need to load the plugin.
   17.11 +* `src/extension.ts` - this is the main file where you will provide the implementation of your command.
   17.12 +The file exports one function, `activate`, which is called the very first time your extension is
   17.13 +activated (in this case by executing the command). Inside the `activate` function we call `registerCommand`.
   17.14 +We pass the function containing the implementation of the command as the second parameter to
   17.15 +`registerCommand`.
   17.16 +
   17.17 +## Get up and running straight away
   17.18 +* press `F5` to open a new window with your extension loaded
   17.19 +* run your command from the command palette by pressing (`Ctrl+Shift+P` or `Cmd+Shift+P` on Mac) and typing `Hello World`
   17.20 +* set breakpoints in your code inside `src/extension.ts` to debug your extension
   17.21 +* find output from your extension in the debug console
   17.22 +
   17.23 +## Make changes
   17.24 +* you can relaunch the extension from the debug toolbar after changing code in `src/extension.ts`
   17.25 +* you can also reload (`Ctrl+R` or `Cmd+R` on Mac) the VS Code window with your extension to load your changes
   17.26 +
   17.27 +## Explore the API
   17.28 +* you can open the full set of our API when you open the file `node_modules/vscode/vscode.d.ts`
   17.29 +
   17.30 +## Run tests
   17.31 +* open the debug viewlet (`Ctrl+Shift+D` or `Cmd+Shift+D` on Mac) and from the launch configuration dropdown pick `Launch Tests`
   17.32 +* press `F5` to run the tests in a new window with your extension loaded
   17.33 +* see the output of the test result in the debug console
   17.34 +* make changes to `test/extension.test.ts` or create new test files inside the `test` folder
   17.35 +    * by convention, the test runner will only consider files matching the name pattern `**.test.ts`
   17.36 +    * you can create folders inside the `test` folder to structure your tests any way you want
   17.37 \ No newline at end of file
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/VSCode/src/channel.scala	Mon Dec 19 20:27:49 2016 +0100
    18.3 @@ -0,0 +1,89 @@
    18.4 +/*  Title:      Tools/VSCode/src/channel.scala
    18.5 +    Author:     Makarius
    18.6 +
    18.7 +Channel with JSON RPC protocol.
    18.8 +*/
    18.9 +
   18.10 +package isabelle.vscode
   18.11 +
   18.12 +
   18.13 +import isabelle._
   18.14 +
   18.15 +import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
   18.16 +
   18.17 +import scala.collection.mutable
   18.18 +
   18.19 +
   18.20 +class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None)
   18.21 +{
   18.22 +  val log: Logger = Logger.make(log_file)
   18.23 +
   18.24 +
   18.25 +  /* read message */
   18.26 +
   18.27 +  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
   18.28 +
   18.29 +  private def read_line(): String =
   18.30 +  {
   18.31 +    val buffer = new ByteArrayOutputStream(100)
   18.32 +    var c = 0
   18.33 +    while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
   18.34 +    Library.trim_line(buffer.toString(UTF8.charset_name))
   18.35 +  }
   18.36 +
   18.37 +  private def read_header(): List[String] =
   18.38 +  {
   18.39 +    val header = new mutable.ListBuffer[String]
   18.40 +    var line = ""
   18.41 +    while ({ line = read_line(); line != "" }) header += line
   18.42 +    header.toList
   18.43 +  }
   18.44 +
   18.45 +  private def read_content(n: Int): String =
   18.46 +  {
   18.47 +    val buffer = new Array[Byte](n)
   18.48 +    var i = 0
   18.49 +    var m = 0
   18.50 +    do {
   18.51 +      m = in.read(buffer, i, n - i)
   18.52 +      if (m != -1) i += m
   18.53 +    }
   18.54 +    while (m != -1 && n > i)
   18.55 +
   18.56 +    if (i == n) new String(buffer, UTF8.charset)
   18.57 +    else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
   18.58 +  }
   18.59 +
   18.60 +  def read(): Option[JSON.T] =
   18.61 +  {
   18.62 +    read_header() match {
   18.63 +      case Nil => None
   18.64 +      case Content_Length(s) :: _ =>
   18.65 +        s match {
   18.66 +          case Value.Int(n) if n >= 0 =>
   18.67 +            val msg = read_content(n)
   18.68 +            log("IN:\n" + msg)
   18.69 +            Some(JSON.parse(msg))
   18.70 +          case _ => error("Bad Content-Length: " + s)
   18.71 +        }
   18.72 +      case header => error(cat_lines("Malformed header:" :: header))
   18.73 +    }
   18.74 +  }
   18.75 +
   18.76 +
   18.77 +  /* write message */
   18.78 +
   18.79 +  def write(json: JSON.T)
   18.80 +  {
   18.81 +    val msg = JSON.Format(json)
   18.82 +    log("OUT:\n" + msg)
   18.83 +
   18.84 +    val content = UTF8.bytes(msg)
   18.85 +    val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
   18.86 +    out.synchronized {
   18.87 +      out.write(header)
   18.88 +      out.write(content)
   18.89 +      out.flush
   18.90 +    }
   18.91 +  }
   18.92 +}
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Dec 19 20:27:49 2016 +0100
    19.3 @@ -0,0 +1,58 @@
    19.4 +/*  Title:      Tools/VSCode/src/document_model.scala
    19.5 +    Author:     Makarius
    19.6 +
    19.7 +Document model for line-oriented text.
    19.8 +*/
    19.9 +
   19.10 +package isabelle.vscode
   19.11 +
   19.12 +
   19.13 +import isabelle._
   19.14 +
   19.15 +import scala.util.parsing.input.CharSequenceReader
   19.16 +
   19.17 +
   19.18 +case class Document_Model(
   19.19 +  session: Session, doc: Line.Document, node_name: Document.Node.Name,
   19.20 +  changed: Boolean = true)
   19.21 +{
   19.22 +  /* header */
   19.23 +
   19.24 +  def is_theory: Boolean = node_name.is_theory
   19.25 +
   19.26 +  lazy val node_header: Document.Node.Header =
   19.27 +    if (is_theory) {
   19.28 +      val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text)
   19.29 +      val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
   19.30 +      toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match {
   19.31 +        case Some(i) =>
   19.32 +          session.resources.check_thy_reader("", node_name,
   19.33 +            new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command)
   19.34 +        case None => Document.Node.no_header
   19.35 +      }
   19.36 +    }
   19.37 +    else Document.Node.no_header
   19.38 +
   19.39 +
   19.40 +  /* edits */
   19.41 +
   19.42 +  def text_edits: List[Text.Edit] =
   19.43 +    if (changed) List(Text.Edit.insert(0, doc.text)) else Nil
   19.44 +
   19.45 +  def node_edits: List[Document.Edit_Text] =
   19.46 +    if (changed) {
   19.47 +      List(session.header_edit(node_name, node_header),
   19.48 +        node_name -> Document.Node.Clear(),
   19.49 +        node_name -> Document.Node.Edits(text_edits),
   19.50 +        node_name ->
   19.51 +          Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
   19.52 +    }
   19.53 +    else Nil
   19.54 +
   19.55 +  def unchanged: Document_Model = if (changed) copy(changed = false) else this
   19.56 +
   19.57 +
   19.58 +  /* snapshot */
   19.59 +
   19.60 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
   19.61 +}
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Tools/VSCode/src/line.scala	Mon Dec 19 20:27:49 2016 +0100
    20.3 @@ -0,0 +1,151 @@
    20.4 +/*  Title:      Tools/VSCode/src/line.scala
    20.5 +    Author:     Makarius
    20.6 +
    20.7 +Line-oriented text.
    20.8 +*/
    20.9 +
   20.10 +package isabelle.vscode
   20.11 +
   20.12 +
   20.13 +import isabelle._
   20.14 +
   20.15 +import scala.annotation.tailrec
   20.16 +
   20.17 +
   20.18 +object Line
   20.19 +{
   20.20 +  /* position */
   20.21 +
   20.22 +  object Position
   20.23 +  {
   20.24 +    val zero: Position = Position(0, 0)
   20.25 +  }
   20.26 +
   20.27 +  sealed case class Position(line: Int, column: Int)
   20.28 +  {
   20.29 +    def line1: Int = line + 1
   20.30 +    def column1: Int = column + 1
   20.31 +    def print: String = line1.toString + ":" + column1.toString
   20.32 +
   20.33 +    def compare(that: Position): Int =
   20.34 +      line compare that.line match {
   20.35 +        case 0 => column compare that.column
   20.36 +        case i => i
   20.37 +      }
   20.38 +
   20.39 +    private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
   20.40 +    {
   20.41 +      var l = line
   20.42 +      var c = column
   20.43 +      for (x <- iterator) {
   20.44 +        if (is_newline(x)) { l += 1; c = 0 } else c += 1
   20.45 +      }
   20.46 +      Position(l, c)
   20.47 +    }
   20.48 +
   20.49 +    def advance(text: String): Position =
   20.50 +      if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
   20.51 +
   20.52 +    def advance_symbols(text: String): Position =
   20.53 +      if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
   20.54 +
   20.55 +    def advance_codepoints(text: String): Position =
   20.56 +      if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10)
   20.57 +  }
   20.58 +
   20.59 +
   20.60 +  /* range (right-open interval) */
   20.61 +
   20.62 +  sealed case class Range(start: Position, stop: Position)
   20.63 +  {
   20.64 +    if (start.compare(stop) > 0)
   20.65 +      error("Bad line range: " + start.print + ".." + stop.print)
   20.66 +
   20.67 +    def print: String = start.print + ".." + stop.print
   20.68 +  }
   20.69 +
   20.70 +
   20.71 +  /* document with newline as separator (not terminator) */
   20.72 +
   20.73 +  object Document
   20.74 +  {
   20.75 +    val empty: Document = new Document("", Nil)
   20.76 +
   20.77 +    def apply(lines: List[Line]): Document =
   20.78 +      if (lines.isEmpty) empty
   20.79 +      else new Document(lines.mkString("", "\n", ""), lines)
   20.80 +
   20.81 +    def apply(text: String): Document =
   20.82 +      if (text.contains('\r'))
   20.83 +        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
   20.84 +      else if (text == "") Document.empty
   20.85 +      else new Document(text, Library.split_lines(text).map(Line(_)))
   20.86 +  }
   20.87 +
   20.88 +  final class Document private(val text: String, val lines: List[Line])
   20.89 +  {
   20.90 +    override def toString: String = text
   20.91 +
   20.92 +    override def equals(that: Any): Boolean =
   20.93 +      that match {
   20.94 +        case other: Document => lines == other.lines
   20.95 +        case _ => false
   20.96 +      }
   20.97 +    override def hashCode(): Int = lines.hashCode
   20.98 +
   20.99 +    private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
  20.100 +    {
  20.101 +      @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
  20.102 +      {
  20.103 +        lines_rest match {
  20.104 +          case Nil => require(i == 0); Position(lines_count, 0)
  20.105 +          case line :: ls =>
  20.106 +            val n = line.text.length
  20.107 +            if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
  20.108 +            else move(i - (n + 1), lines_count + 1, ls)
  20.109 +        }
  20.110 +      }
  20.111 +      move(offset, 0, lines)
  20.112 +    }
  20.113 +
  20.114 +    def position(i: Text.Offset): Position = position(_.advance(_), i)
  20.115 +    def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
  20.116 +    def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
  20.117 +
  20.118 +    // FIXME symbols, codepoints
  20.119 +    def offset(pos: Position): Option[Text.Offset] =
  20.120 +    {
  20.121 +      val l = pos.line
  20.122 +      val c = pos.column
  20.123 +      if (0 <= l && l < lines.length) {
  20.124 +        val line_offset =
  20.125 +          if (l == 0) 0
  20.126 +          else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
  20.127 +        if (c <= lines(l).text.length) Some(line_offset + c) else None
  20.128 +      }
  20.129 +      else None
  20.130 +    }
  20.131 +  }
  20.132 +
  20.133 +
  20.134 +  /* line text */
  20.135 +
  20.136 +  val empty: Line = new Line("")
  20.137 +  def apply(text: String): Line = if (text == "") empty else new Line(text)
  20.138 +}
  20.139 +
  20.140 +final class Line private(val text: String)
  20.141 +{
  20.142 +  require(text.forall(c => c != '\r' && c != '\n'))
  20.143 +
  20.144 +  lazy val length_symbols: Int = Symbol.iterator(text).length
  20.145 +  lazy val length_codepoints: Int = Word.codepoint_iterator(text).length
  20.146 +
  20.147 +  override def equals(that: Any): Boolean =
  20.148 +    that match {
  20.149 +      case other: Line => text == other.text
  20.150 +      case _ => false
  20.151 +    }
  20.152 +  override def hashCode(): Int = text.hashCode
  20.153 +  override def toString: String = text
  20.154 +}
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Tools/VSCode/src/logger.scala	Mon Dec 19 20:27:49 2016 +0100
    21.3 @@ -0,0 +1,34 @@
    21.4 +/*  Title:      Tools/VSCode/src/logger.scala
    21.5 +    Author:     Makarius
    21.6 +
    21.7 +Minimal logging support.
    21.8 +*/
    21.9 +
   21.10 +package isabelle.vscode
   21.11 +
   21.12 +
   21.13 +import isabelle._
   21.14 +
   21.15 +
   21.16 +object Logger
   21.17 +{
   21.18 +  def make(log_file: Option[Path]): Logger =
   21.19 +    log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
   21.20 +}
   21.21 +
   21.22 +trait Logger
   21.23 +{
   21.24 +  def apply(msg: => String): Unit
   21.25 +}
   21.26 +
   21.27 +object No_Logger extends Logger
   21.28 +{
   21.29 +  def apply(msg: => String) { }
   21.30 +}
   21.31 +
   21.32 +class File_Logger(path: Path) extends Logger
   21.33 +{
   21.34 +  def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
   21.35 +
   21.36 +  override def toString: String = path.toString
   21.37 +}
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Tools/VSCode/src/protocol.scala	Mon Dec 19 20:27:49 2016 +0100
    22.3 @@ -0,0 +1,299 @@
    22.4 +/*  Title:      Tools/VSCode/src/protocol.scala
    22.5 +    Author:     Makarius
    22.6 +
    22.7 +Message formats for Language Server Protocol 2.0, see
    22.8 +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
    22.9 +*/
   22.10 +
   22.11 +package isabelle.vscode
   22.12 +
   22.13 +
   22.14 +import isabelle._
   22.15 +
   22.16 +
   22.17 +object Protocol
   22.18 +{
   22.19 +  /* abstract message */
   22.20 +
   22.21 +  object Message
   22.22 +  {
   22.23 +    val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0")
   22.24 +  }
   22.25 +
   22.26 +
   22.27 +  /* notification */
   22.28 +
   22.29 +  object Notification
   22.30 +  {
   22.31 +    def apply(method: String, params: JSON.T): JSON.T =
   22.32 +      Message.empty + ("method" -> method) + ("params" -> params)
   22.33 +
   22.34 +    def unapply(json: JSON.T): Option[(String, Option[JSON.T])] =
   22.35 +      for {
   22.36 +        method <- JSON.string(json, "method")
   22.37 +        params = JSON.value(json, "params")
   22.38 +      } yield (method, params)
   22.39 +  }
   22.40 +
   22.41 +  class Notification0(name: String)
   22.42 +  {
   22.43 +    def unapply(json: JSON.T): Option[Unit] =
   22.44 +      json match {
   22.45 +        case Notification(method, _) if method == name => Some(())
   22.46 +        case _ => None
   22.47 +      }
   22.48 +  }
   22.49 +
   22.50 +
   22.51 +  /* request message */
   22.52 +
   22.53 +  sealed case class Id(id: Any)
   22.54 +  {
   22.55 +    require(
   22.56 +      id.isInstanceOf[Int] ||
   22.57 +      id.isInstanceOf[Long] ||
   22.58 +      id.isInstanceOf[Double] ||
   22.59 +      id.isInstanceOf[String])
   22.60 +
   22.61 +    override def toString: String = id.toString
   22.62 +  }
   22.63 +
   22.64 +  object RequestMessage
   22.65 +  {
   22.66 +    def apply(id: Id, method: String, params: JSON.T): JSON.T =
   22.67 +      Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params)
   22.68 +
   22.69 +    def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] =
   22.70 +      for {
   22.71 +        id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id")
   22.72 +        method <- JSON.string(json, "method")
   22.73 +        params = JSON.value(json, "params")
   22.74 +      } yield (Id(id), method, params)
   22.75 +  }
   22.76 +
   22.77 +  class Request0(name: String)
   22.78 +  {
   22.79 +    def unapply(json: JSON.T): Option[Id] =
   22.80 +      json match {
   22.81 +        case RequestMessage(id, method, _) if method == name => Some(id)
   22.82 +        case _ => None
   22.83 +      }
   22.84 +  }
   22.85 +
   22.86 +
   22.87 +  /* response message */
   22.88 +
   22.89 +  object ResponseMessage
   22.90 +  {
   22.91 +    def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
   22.92 +      Message.empty + ("id" -> id.id) ++
   22.93 +      (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
   22.94 +      (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
   22.95 +
   22.96 +    def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
   22.97 +      if (error == "") apply(id, result = result)
   22.98 +      else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
   22.99 +  }
  22.100 +
  22.101 +  sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
  22.102 +  {
  22.103 +    def json: JSON.T =
  22.104 +      Map("code" -> code, "message" -> message) ++
  22.105 +      (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
  22.106 +  }
  22.107 +
  22.108 +  object ErrorCodes
  22.109 +  {
  22.110 +    val ParseError = -32700
  22.111 +    val InvalidRequest = -32600
  22.112 +    val MethodNotFound = -32601
  22.113 +    val InvalidParams = -32602
  22.114 +    val InternalError = -32603
  22.115 +    val serverErrorStart = -32099
  22.116 +    val serverErrorEnd = -32000
  22.117 +  }
  22.118 +
  22.119 +
  22.120 +  /* init and exit */
  22.121 +
  22.122 +  object Initialize extends Request0("initialize")
  22.123 +  {
  22.124 +    def reply(id: Id, error: String): JSON.T =
  22.125 +      ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error)
  22.126 +  }
  22.127 +
  22.128 +  object ServerCapabilities
  22.129 +  {
  22.130 +    val json: JSON.T =
  22.131 +      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
  22.132 +  }
  22.133 +
  22.134 +  object Shutdown extends Request0("shutdown")
  22.135 +  {
  22.136 +    def reply(id: Id, error: String): JSON.T =
  22.137 +      ResponseMessage.strict(id, Some("OK"), error)
  22.138 +  }
  22.139 +
  22.140 +  object Exit extends Notification0("exit")
  22.141 +
  22.142 +
  22.143 +  /* document positions */
  22.144 +
  22.145 +  object Position
  22.146 +  {
  22.147 +    def apply(pos: Line.Position): JSON.T =
  22.148 +      Map("line" -> pos.line, "character" -> pos.column)
  22.149 +
  22.150 +    def unapply(json: JSON.T): Option[Line.Position] =
  22.151 +      for {
  22.152 +        line <- JSON.int(json, "line")
  22.153 +        column <- JSON.int(json, "character")
  22.154 +      } yield Line.Position(line, column)
  22.155 +  }
  22.156 +
  22.157 +  object Range
  22.158 +  {
  22.159 +    def apply(range: Line.Range): JSON.T =
  22.160 +      Map("start" -> Position(range.start), "end" -> Position(range.stop))
  22.161 +
  22.162 +    def unapply(json: JSON.T): Option[Line.Range] =
  22.163 +      (JSON.value(json, "start"), JSON.value(json, "end")) match {
  22.164 +        case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop))
  22.165 +        case _ => None
  22.166 +      }
  22.167 +  }
  22.168 +
  22.169 +  object Location
  22.170 +  {
  22.171 +    def apply(uri: String, range: Line.Range): JSON.T =
  22.172 +      Map("uri" -> uri, "range" -> Range(range))
  22.173 +
  22.174 +    def unapply(json: JSON.T): Option[(String, Line.Range)] =
  22.175 +      for {
  22.176 +        uri <- JSON.string(json, "uri")
  22.177 +        range_json <- JSON.value(json, "range")
  22.178 +        range <- Range.unapply(range_json)
  22.179 +      } yield (uri, range)
  22.180 +  }
  22.181 +
  22.182 +  object TextDocumentPosition
  22.183 +  {
  22.184 +    def unapply(json: JSON.T): Option[(String, Line.Position)] =
  22.185 +      for {
  22.186 +        doc <- JSON.value(json, "textDocument")
  22.187 +        uri <- JSON.string(doc, "uri")
  22.188 +        pos_json <- JSON.value(json, "position")
  22.189 +        pos <- Position.unapply(pos_json)
  22.190 +      } yield (uri, pos)
  22.191 +  }
  22.192 +
  22.193 +
  22.194 +  /* diagnostic messages */
  22.195 +
  22.196 +  object MessageType
  22.197 +  {
  22.198 +    val Error = 1
  22.199 +    val Warning = 2
  22.200 +    val Info = 3
  22.201 +    val Log = 4
  22.202 +  }
  22.203 +
  22.204 +  object DisplayMessage
  22.205 +  {
  22.206 +    def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
  22.207 +      Notification(if (show) "window/showMessage" else "window/logMessage",
  22.208 +        Map("type" -> message_type, "message" -> message))
  22.209 +  }
  22.210 +
  22.211 +
  22.212 +  /* document edits */
  22.213 +
  22.214 +  object DidOpenTextDocument
  22.215 +  {
  22.216 +    def unapply(json: JSON.T): Option[(String, String, Long, String)] =
  22.217 +      json match {
  22.218 +        case Notification("textDocument/didOpen", Some(params)) =>
  22.219 +          for {
  22.220 +            doc <- JSON.value(params, "textDocument")
  22.221 +            uri <- JSON.string(doc, "uri")
  22.222 +            lang <- JSON.string(doc, "languageId")
  22.223 +            version <- JSON.long(doc, "version")
  22.224 +            text <- JSON.string(doc, "text")
  22.225 +          } yield (uri, lang, version, text)
  22.226 +        case _ => None
  22.227 +      }
  22.228 +  }
  22.229 +
  22.230 +
  22.231 +  sealed abstract class TextDocumentContentChange
  22.232 +  case class TextDocumentContent(text: String) extends TextDocumentContentChange
  22.233 +  case class TextDocumentChange(range: Line.Range, range_length: Int, text: String)
  22.234 +    extends TextDocumentContentChange
  22.235 +
  22.236 +  object TextDocumentContentChange
  22.237 +  {
  22.238 +    def unapply(json: JSON.T): Option[TextDocumentContentChange] =
  22.239 +      for { text <- JSON.string(json, "text") }
  22.240 +      yield {
  22.241 +        (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match {
  22.242 +          case (Some(Range(range)), Some(range_length)) =>
  22.243 +            TextDocumentChange(range, range_length, text)
  22.244 +          case _ => TextDocumentContent(text)
  22.245 +        }
  22.246 +      }
  22.247 +  }
  22.248 +
  22.249 +  object DidChangeTextDocument
  22.250 +  {
  22.251 +    def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
  22.252 +      json match {
  22.253 +        case Notification("textDocument/didChange", Some(params)) =>
  22.254 +          for {
  22.255 +            doc <- JSON.value(params, "textDocument")
  22.256 +            uri <- JSON.string(doc, "uri")
  22.257 +            version <- JSON.long(doc, "version")
  22.258 +            changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
  22.259 +          } yield (uri, version, changes)
  22.260 +        case _ => None
  22.261 +      }
  22.262 +  }
  22.263 +
  22.264 +  class TextDocumentNotification(name: String)
  22.265 +  {
  22.266 +    def unapply(json: JSON.T): Option[String] =
  22.267 +      json match {
  22.268 +        case Notification(method, Some(params)) if method == name =>
  22.269 +          for {
  22.270 +            doc <- JSON.value(params, "textDocument")
  22.271 +            uri <- JSON.string(doc, "uri")
  22.272 +          } yield uri
  22.273 +        case _ => None
  22.274 +      }
  22.275 +  }
  22.276 +
  22.277 +  object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
  22.278 +  object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
  22.279 +
  22.280 +
  22.281 +  /* hover request */
  22.282 +
  22.283 +  object Hover
  22.284 +  {
  22.285 +    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
  22.286 +      json match {
  22.287 +        case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
  22.288 +          Some((id, uri, pos))
  22.289 +        case _ => None
  22.290 +      }
  22.291 +
  22.292 +    def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
  22.293 +    {
  22.294 +      val res =
  22.295 +        result match {
  22.296 +          case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
  22.297 +          case None => Map("contents" -> Nil)
  22.298 +        }
  22.299 +      ResponseMessage(id, Some(res))
  22.300 +    }
  22.301 +  }
  22.302 +}
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Dec 19 20:27:49 2016 +0100
    23.3 @@ -0,0 +1,354 @@
    23.4 +/*  Title:      Tools/VSCode/src/server.scala
    23.5 +    Author:     Makarius
    23.6 +
    23.7 +Server for VS Code Language Server Protocol 2.0, see also
    23.8 +https://github.com/Microsoft/language-server-protocol
    23.9 +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
   23.10 +*/
   23.11 +
   23.12 +package isabelle.vscode
   23.13 +
   23.14 +
   23.15 +import isabelle._
   23.16 +
   23.17 +import java.io.{PrintStream, OutputStream}
   23.18 +
   23.19 +import scala.annotation.tailrec
   23.20 +
   23.21 +
   23.22 +object Server
   23.23 +{
   23.24 +  /* Isabelle tool wrapper */
   23.25 +
   23.26 +  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   23.27 +
   23.28 +  val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args =>
   23.29 +  {
   23.30 +    var log_file: Option[Path] = None
   23.31 +    var dirs: List[Path] = Nil
   23.32 +    var logic = default_logic
   23.33 +    var modes: List[String] = Nil
   23.34 +    var options = Options.init()
   23.35 +
   23.36 +    val getopts = Getopts("""
   23.37 +Usage: isabelle vscode_server [OPTIONS]
   23.38 +
   23.39 +  Options are:
   23.40 +    -L FILE      enable logging on FILE
   23.41 +    -d DIR       include session directory
   23.42 +    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   23.43 +    -m MODE      add print mode for output
   23.44 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   23.45 +
   23.46 +  Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
   23.47 +""",
   23.48 +      "L:" -> (arg => log_file = Some(Path.explode(arg))),
   23.49 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   23.50 +      "l:" -> (arg => logic = arg),
   23.51 +      "m:" -> (arg => modes = arg :: modes),
   23.52 +      "o:" -> (arg => options = options + arg))
   23.53 +
   23.54 +    val more_args = getopts(args)
   23.55 +    if (more_args.nonEmpty) getopts.usage()
   23.56 +
   23.57 +    if (!Build.build(options = options, build_heap = true, no_build = true,
   23.58 +          dirs = dirs, sessions = List(logic)).ok)
   23.59 +      error("Missing logic image " + quote(logic))
   23.60 +
   23.61 +    val channel = new Channel(System.in, System.out, log_file)
   23.62 +    val server = new Server(channel, options, logic, dirs, modes)
   23.63 +
   23.64 +    // prevent spurious garbage on the main protocol channel
   23.65 +    val orig_out = System.out
   23.66 +    try {
   23.67 +      System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
   23.68 +      server.start()
   23.69 +    }
   23.70 +    finally { System.setOut(orig_out) }
   23.71 +  })
   23.72 +
   23.73 +
   23.74 +  /* server state */
   23.75 +
   23.76 +  sealed case class State(
   23.77 +    session: Option[Session] = None,
   23.78 +    models: Map[String, Document_Model] = Map.empty)
   23.79 +}
   23.80 +
   23.81 +class Server(
   23.82 +  channel: Channel,
   23.83 +  options: Options,
   23.84 +  session_name: String = Server.default_logic,
   23.85 +  session_dirs: List[Path] = Nil,
   23.86 +  modes: List[String] = Nil)
   23.87 +{
   23.88 +  /* server state */
   23.89 +
   23.90 +  private val state = Synchronized(Server.State())
   23.91 +
   23.92 +  def session: Session = state.value.session getOrElse error("Session inactive")
   23.93 +  def resources: URI_Resources = session.resources.asInstanceOf[URI_Resources]
   23.94 +
   23.95 +
   23.96 +  /* init and exit */
   23.97 +
   23.98 +  def initialize(reply: String => Unit)
   23.99 +  {
  23.100 +    val content = Build.session_content(options, false, session_dirs, session_name)
  23.101 +    val resources =
  23.102 +      new URI_Resources(content.loaded_theories, content.known_theories, content.syntax)
  23.103 +
  23.104 +    val session =
  23.105 +      new Session(resources) {
  23.106 +        override def output_delay = options.seconds("editor_output_delay")
  23.107 +        override def prune_delay = options.seconds("editor_prune_delay")
  23.108 +        override def syslog_limit = options.int("editor_syslog_limit")
  23.109 +        override def reparse_limit = options.int("editor_reparse_limit")
  23.110 +      }
  23.111 +
  23.112 +    var session_phase: Session.Consumer[Session.Phase] = null
  23.113 +    session_phase =
  23.114 +      Session.Consumer(getClass.getName) {
  23.115 +        case Session.Ready =>
  23.116 +          session.phase_changed -= session_phase
  23.117 +          session.update_options(options)
  23.118 +          reply("")
  23.119 +        case Session.Failed =>
  23.120 +          session.phase_changed -= session_phase
  23.121 +          reply("Prover startup failed")
  23.122 +        case _ =>
  23.123 +      }
  23.124 +    session.phase_changed += session_phase
  23.125 +
  23.126 +    session.start(receiver =>
  23.127 +      Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
  23.128 +        modes = modes, receiver = receiver))
  23.129 +
  23.130 +    state.change(_.copy(session = Some(session)))
  23.131 +  }
  23.132 +
  23.133 +  def shutdown(reply: String => Unit)
  23.134 +  {
  23.135 +    state.change(st =>
  23.136 +      st.session match {
  23.137 +        case None => reply("Prover inactive"); st
  23.138 +        case Some(session) =>
  23.139 +          var session_phase: Session.Consumer[Session.Phase] = null
  23.140 +          session_phase =
  23.141 +            Session.Consumer(getClass.getName) {
  23.142 +              case Session.Inactive =>
  23.143 +                session.phase_changed -= session_phase
  23.144 +                reply("")
  23.145 +              case _ =>
  23.146 +            }
  23.147 +          session.phase_changed += session_phase
  23.148 +          session.stop()
  23.149 +          st.copy(session = None)
  23.150 +      })
  23.151 +  }
  23.152 +
  23.153 +  def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) }
  23.154 +
  23.155 +
  23.156 +  /* document management */
  23.157 +
  23.158 +  private val delay_flush =
  23.159 +    Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
  23.160 +      state.change(st =>
  23.161 +        {
  23.162 +          val models = st.models
  23.163 +          val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
  23.164 +          val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit
  23.165 +          val models1 =
  23.166 +            (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
  23.167 +
  23.168 +          session.update(Document.Blobs.empty, edits)
  23.169 +          st.copy(models = models1)
  23.170 +        })
  23.171 +    }
  23.172 +
  23.173 +  def update_document(uri: String, text: String)
  23.174 +  {
  23.175 +    state.change(st =>
  23.176 +      {
  23.177 +        val node_name = resources.node_name(uri)
  23.178 +        val model = Document_Model(session, Line.Document(text), node_name)
  23.179 +        st.copy(models = st.models + (uri -> model))
  23.180 +      })
  23.181 +    delay_flush.invoke()
  23.182 +  }
  23.183 +
  23.184 +
  23.185 +  /* tooltips -- see $ISABELLE_HOME/src/Tools/jEdit/rendering.scala */
  23.186 +
  23.187 +  def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] =
  23.188 +    for {
  23.189 +      model <- state.value.models.get(uri)
  23.190 +      snapshot = model.snapshot()
  23.191 +      offset <- model.doc.offset(pos)
  23.192 +      info <- tooltip(snapshot, Text.Range(offset, offset + 1))
  23.193 +    } yield {
  23.194 +      val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop))
  23.195 +      val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble)
  23.196 +      (r, List("```\n" + s + "\n```"))
  23.197 +    }
  23.198 +
  23.199 +  private val tooltip_descriptions =
  23.200 +    Map(
  23.201 +      Markup.CITATION -> "citation",
  23.202 +      Markup.TOKEN_RANGE -> "inner syntax token",
  23.203 +      Markup.FREE -> "free variable",
  23.204 +      Markup.SKOLEM -> "skolem variable",
  23.205 +      Markup.BOUND -> "bound variable",
  23.206 +      Markup.VAR -> "schematic variable",
  23.207 +      Markup.TFREE -> "free type variable",
  23.208 +      Markup.TVAR -> "schematic type variable")
  23.209 +
  23.210 +  private val tooltip_elements =
  23.211 +    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
  23.212 +      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
  23.213 +      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
  23.214 +      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
  23.215 +
  23.216 +  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
  23.217 +    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
  23.218 +
  23.219 +  private def timing_threshold: Double = options.real("jedit_timing_threshold")
  23.220 +
  23.221 +  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[XML.Body]] =
  23.222 +  {
  23.223 +    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
  23.224 +      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
  23.225 +    {
  23.226 +      val r = snapshot.convert(r0)
  23.227 +      val (t, info) = prev.info
  23.228 +      if (prev.range == r)
  23.229 +        Text.Info(r, (t, info :+ p))
  23.230 +      else Text.Info(r, (t, Vector(p)))
  23.231 +    }
  23.232 +
  23.233 +    val results =
  23.234 +      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
  23.235 +        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
  23.236 +        {
  23.237 +          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
  23.238 +            Some(Text.Info(r, (t1 + t2, info)))
  23.239 +
  23.240 +          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
  23.241 +          if kind != "" &&
  23.242 +            kind != Markup.ML_DEF &&
  23.243 +            kind != Markup.ML_OPEN &&
  23.244 +            kind != Markup.ML_STRUCTURE =>
  23.245 +            val kind1 = Word.implode(Word.explode('_', kind))
  23.246 +            val txt1 =
  23.247 +              if (name == "") kind1
  23.248 +              else if (kind1 == "") quote(name)
  23.249 +              else kind1 + " " + quote(name)
  23.250 +            val t = prev.info._1
  23.251 +            val txt2 =
  23.252 +              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
  23.253 +                "\n" + t.message
  23.254 +              else ""
  23.255 +            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
  23.256 +
  23.257 +          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
  23.258 +            val text = "doc " + quote(name)
  23.259 +            Some(add(prev, r, (true, XML.Text(text))))
  23.260 +
  23.261 +          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
  23.262 +            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
  23.263 +
  23.264 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
  23.265 +          if name == Markup.SORTING || name == Markup.TYPING =>
  23.266 +            Some(add(prev, r, (true, pretty_typing("::", body))))
  23.267 +
  23.268 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
  23.269 +            Some(add(prev, r, (true, Pretty.block(0, body))))
  23.270 +
  23.271 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
  23.272 +            Some(add(prev, r, (false, pretty_typing("ML:", body))))
  23.273 +
  23.274 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
  23.275 +            val lang = Word.implode(Word.explode('_', language))
  23.276 +            Some(add(prev, r, (true, XML.Text("language: " + lang))))
  23.277 +
  23.278 +          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
  23.279 +            val descr = if (kind == "") "expression" else "expression: " + kind
  23.280 +            Some(add(prev, r, (true, XML.Text(descr))))
  23.281 +
  23.282 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
  23.283 +            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
  23.284 +          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
  23.285 +            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
  23.286 +
  23.287 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
  23.288 +            tooltip_descriptions.get(name).
  23.289 +              map(descr => add(prev, r, (true, XML.Text(descr))))
  23.290 +        }).map(_.info)
  23.291 +
  23.292 +    results.map(_.info).flatMap(res => res._2.toList) match {
  23.293 +      case Nil => None
  23.294 +      case tips =>
  23.295 +        val r = Text.Range(results.head.range.start, results.last.range.stop)
  23.296 +        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
  23.297 +        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
  23.298 +    }
  23.299 +  }
  23.300 +
  23.301 +  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
  23.302 +
  23.303 +
  23.304 +  /* main loop */
  23.305 +
  23.306 +  def start()
  23.307 +  {
  23.308 +    channel.log("\nServer started " + Date.now())
  23.309 +
  23.310 +    def handle(json: JSON.T)
  23.311 +    {
  23.312 +      try {
  23.313 +        json match {
  23.314 +          case Protocol.Initialize(id) =>
  23.315 +            def initialize_reply(err: String)
  23.316 +            {
  23.317 +              channel.write(Protocol.Initialize.reply(id, err))
  23.318 +              if (err == "") {
  23.319 +                channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info,
  23.320 +                  "Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")"))
  23.321 +              }
  23.322 +              else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err))
  23.323 +            }
  23.324 +            initialize(initialize_reply _)
  23.325 +          case Protocol.Shutdown(id) =>
  23.326 +            shutdown((error: String) => channel.write(Protocol.Shutdown.reply(id, error)))
  23.327 +          case Protocol.Exit =>
  23.328 +            exit()
  23.329 +          case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
  23.330 +            update_document(uri, text)
  23.331 +          case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
  23.332 +            update_document(uri, text)
  23.333 +          case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
  23.334 +          case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
  23.335 +          case Protocol.Hover(id, uri, pos) =>
  23.336 +            channel.write(Protocol.Hover.reply(id, hover(uri, pos)))
  23.337 +          case _ => channel.log("### IGNORED")
  23.338 +        }
  23.339 +      }
  23.340 +      catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
  23.341 +    }
  23.342 +
  23.343 +    @tailrec def loop()
  23.344 +    {
  23.345 +      channel.read() match {
  23.346 +        case Some(json) =>
  23.347 +          json match {
  23.348 +            case bulk: List[_] => bulk.foreach(handle(_))
  23.349 +            case _ => handle(json)
  23.350 +          }
  23.351 +          loop()
  23.352 +        case None => channel.log("### TERMINATE")
  23.353 +      }
  23.354 +    }
  23.355 +    loop()
  23.356 +  }
  23.357 +}
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/Tools/VSCode/src/uri_resources.scala	Mon Dec 19 20:27:49 2016 +0100
    24.3 @@ -0,0 +1,43 @@
    24.4 +/*  Title:      Tools/VSCode/src/uri_resources.scala
    24.5 +    Author:     Makarius
    24.6 +
    24.7 +Resources based on file-system URIs.
    24.8 +*/
    24.9 +
   24.10 +package isabelle.vscode
   24.11 +
   24.12 +
   24.13 +import isabelle._
   24.14 +
   24.15 +import java.net.{URI, URISyntaxException}
   24.16 +import java.io.{File => JFile}
   24.17 +
   24.18 +
   24.19 +object URI_Resources
   24.20 +{
   24.21 +  def is_wellformed(uri: String): Boolean =
   24.22 +    try { new JFile(new URI(uri)); true }
   24.23 +    catch { case _: URISyntaxException | _: IllegalArgumentException => false }
   24.24 +
   24.25 +  def canonical_file(uri: String): JFile =
   24.26 +    new JFile(new URI(uri)).getCanonicalFile
   24.27 +
   24.28 +  val empty: URI_Resources =
   24.29 +    new URI_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
   24.30 +}
   24.31 +
   24.32 +class URI_Resources(
   24.33 +    loaded_theories: Set[String],
   24.34 +    known_theories: Map[String, Document.Node.Name],
   24.35 +    base_syntax: Outer_Syntax)
   24.36 +  extends Resources(loaded_theories, known_theories, base_syntax)
   24.37 +{
   24.38 +  def node_name(uri: String): Document.Node.Name =
   24.39 +  {
   24.40 +    val file = URI_Resources.canonical_file(uri)  // FIXME wellformed!?
   24.41 +    val node = file.getPath
   24.42 +    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
   24.43 +    val master_dir = if (theory == "") "" else file.getParent
   24.44 +    Document.Node.Name(node, master_dir, theory)
   24.45 +  }
   24.46 +}