# HG changeset patch # User wenzelm # Date 1482175669 -3600 # Node ID 9c1173a7e4cbbd976193f676d9f24dd0f84d0098 # Parent 2bf8cfc98c4d10a1b8ff1a29783ba4a8330ec24b basic support for VSCode Language Server protocol; minimal extension for VSCode editor; diff -r 2bf8cfc98c4d -r 9c1173a7e4cb .hgignore --- a/.hgignore Sun Dec 18 23:43:50 2016 +0100 +++ b/.hgignore Mon Dec 19 20:27:49 2016 +0100 @@ -20,5 +20,8 @@ ^doc/.*\.pdf ^doc/.*\.ps ^src/Tools/jEdit/dist/ +^src/Tools/VSCode/out/ +^src/Tools/VSCode/extension/node_modules/ +^src/Tools/VSCode/extension/protocol.log ^Admin/jenkins/ci-extras/target/ ^stats/ diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sun Dec 18 23:43:50 2016 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Dec 19 20:27:49 2016 +0100 @@ -113,7 +113,8 @@ Update_Cartouches.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, - Update_Theorems.isabelle_tool) + Update_Theorems.isabelle_tool, + isabelle.vscode.Server.isabelle_tool) private def list_internal(): List[(String, String)] = for (tool <- internal_tools.toList if tool.accessible) diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Pure/build-jars --- a/src/Pure/build-jars Sun Dec 18 23:43:50 2016 +0100 +++ b/src/Pure/build-jars Mon Dec 19 20:27:49 2016 +0100 @@ -153,6 +153,13 @@ "../Tools/Graphview/popups.scala" "../Tools/Graphview/shapes.scala" "../Tools/Graphview/tree_panel.scala" + "../Tools/VSCode/src/channel.scala" + "../Tools/VSCode/src/document_model.scala" + "../Tools/VSCode/src/line.scala" + "../Tools/VSCode/src/logger.scala" + "../Tools/VSCode/src/protocol.scala" + "../Tools/VSCode/src/server.scala" + "../Tools/VSCode/src/uri_resources.scala" ) diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/README.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/README.md Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,58 @@ +# Isabelle/PIDE for Visual Studio Code editor # + +* Extension for the editor ([TypeScript](extension/src/extension.ts)) +* Language Server protocol implementation ([Isabelle/Scala](src/server.scala)) + + +## Build and run ## + +* shell> `isabelle build -b HOL` + +* shell> `cd src/Tools/VSCode/extension; vsce package` + +* Preferences / User settings / edit settings.json: e.g. + `"isabelle.home": "/home/makarius/isabelle/repos"` + +* Extensions / ... / Install from VSIX: `src/Tools/VSCode/extension/isabelle-0.0.1.vsix` + +* File / Open Folder: e.g. `src/HOL/Isar_Examples/` then open .thy files + + +## Debug + +* shell> `code src/Tools/VSCode/extension` + +* View / Debug / Launch Extension + +* File / Open Folder: e.g. `src/HOL/Isar_Examples/` then open .thy files + + +## Relevant links ## + +### VSCode editor ### + +* https://code.visualstudio.com +* https://code.visualstudio.com/docs/extensionAPI/extension-points +* https://code.visualstudio.com/docs/extensions/example-language-server +* https://github.com/Microsoft/vscode-languageserver-node-example + + +### Protocol ### + +* https://code.visualstudio.com/blogs/2016/06/27/common-language-protocol +* https://github.com/Microsoft/vscode-languageserver-node +* https://github.com/Microsoft/language-server-protocol +* https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md +* http://www.jsonrpc.org/specification +* http://www.json.org + + +### Similar projects ### + +* Coq: https://github.com/siegebell/vscoq +* OCaml: https://github.com/freebroccolo/vscode-reasonml +* Scala: https://github.com/dragos/dragos-vscode-scala +* Rust: + * https://github.com/jonathandturner/rls + * https://github.com/jonathandturner/rls_vscode + * https://github.com/RustDT/RustLSP diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/.vscode/launch.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/.vscode/launch.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,28 @@ +// A launch configuration that compiles the extension and then opens it inside a new window +{ + "version": "0.1.0", + "configurations": [ + { + "name": "Launch Extension", + "type": "extensionHost", + "request": "launch", + "runtimeExecutable": "${execPath}", + "args": ["--extensionDevelopmentPath=${workspaceRoot}" ], + "stopOnEntry": false, + "sourceMaps": true, + "outDir": "${workspaceRoot}/out/src", + "preLaunchTask": "npm" + }, + { + "name": "Launch Tests", + "type": "extensionHost", + "request": "launch", + "runtimeExecutable": "${execPath}", + "args": ["--extensionDevelopmentPath=${workspaceRoot}", "--extensionTestsPath=${workspaceRoot}/out/test" ], + "stopOnEntry": false, + "sourceMaps": true, + "outDir": "${workspaceRoot}/out/test", + "preLaunchTask": "npm" + } + ] +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/.vscode/settings.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/.vscode/settings.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,10 @@ +// Place your settings in this file to overwrite default and user settings. +{ + "files.exclude": { + "out": false // set this to true to hide the "out" folder with the compiled JS files + }, + "search.exclude": { + "out": true // set this to false to include "out" folder in search results + }, + "typescript.tsdk": "./node_modules/typescript/lib" // we want to use the TS server from our node_modules folder to control its version +} \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/.vscode/tasks.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/.vscode/tasks.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,30 @@ +// Available variables which can be used inside of strings. +// ${workspaceRoot}: the root folder of the team +// ${file}: the current opened file +// ${fileBasename}: the current opened file's basename +// ${fileDirname}: the current opened file's dirname +// ${fileExtname}: the current opened file's extension +// ${cwd}: the current working directory of the spawned process + +// A task runner that calls a custom npm script that compiles the extension. +{ + "version": "0.1.0", + + // we want to run npm + "command": "npm", + + // the command is a shell script + "isShellCommand": true, + + // show the output window only if unrecognized errors occur. + "showOutput": "silent", + + // we run the custom script "compile" as defined in package.json + "args": ["run", "compile", "--loglevel", "silent"], + + // The tsc compiler is started in watching mode + "isWatching": true, + + // use the standard tsc in watch mode problem matcher to find compile problems in the output. + "problemMatcher": "$tsc-watch" +} \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/.vscodeignore --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/.vscodeignore Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,9 @@ +.vscode/** +.vscode-test/** +out/test/** +test/** +src/** +**/*.map +.gitignore +tsconfig.json +vsc-extension-quickstart.md diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/README.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/README.md Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,6 @@ +# Isabelle language support + +This extension provides language support for Isabelle. + +Make sure that User Settings `isabelle.home` points to the ISABELLE_HOME +directory. diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/isabelle.png Binary file src/Tools/VSCode/extension/isabelle.png has changed diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/language-configuration.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/language-configuration.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,16 @@ +{ + "brackets": [ + ["(", ")"], + ["[", "]"], + ["{", "}"], + ["<", ">"], + ["«", "»"], + ["‹", "›"], + ["⟨", "⟩"], + ["⌈", "⌉"], + ["⌊", "⌋"], + ["⦇", "⦈"], + ["⟦", "⟧"], + ["⦃", "⦄"] + ] +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/package.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/package.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,58 @@ +{ + "name": "isabelle", + "displayName": "Isabelle", + "description": "Isabelle Theorem Prover", + "keywords": [ + "theorem prover", + "formalized mathematics", + "mathematical logic", + "functional programming", + "document preparation" + ], + "icon": "isabelle.png", + "version": "0.0.1", + "publisher": "Makarius", + "license": "BSD-3-Clause", + "repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" }, + "engines": { "vscode": "^1.5.0" }, + "categories": ["Languages"], + "activationEvents": [ + "onLanguage:isabelle" + ], + "main": "./out/src/extension", + "contributes": { + "languages": [ + { + "id": "isabelle", + "aliases": ["Isabelle"], + "extensions": [".thy"], + "configuration": "./language-configuration.json" + } + ], + "configuration": { + "title": "Isabelle", + "properties": { + "isabelle.home": { + "type": "string", + "default": "", + "description": "ISABELLE_HOME directory" + } + } + } + }, + "scripts": { + "vscode:prepublish": "tsc -p ./", + "compile": "tsc -watch -p ./", + "postinstall": "node ./node_modules/vscode/bin/install" + }, + "devDependencies": { + "typescript": "^2.0.3", + "vscode": "^1.0.0", + "mocha": "^2.3.3", + "@types/node": "^6.0.40", + "@types/mocha": "^2.2.32" + }, + "dependencies": { + "vscode-languageclient": "^2.6.3" + } +} \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/src/extension.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/extension.ts Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,32 @@ +'use strict'; + +import * as vscode from 'vscode'; +import * as path from 'path'; + +import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind } + from 'vscode-languageclient'; + + +export function activate(context: vscode.ExtensionContext) +{ + let isabelle_home = vscode.workspace.getConfiguration("isabelle").get("home"); + + let run = { + command: path.join(isabelle_home, "bin", "isabelle"), + args: ["vscode_server"] + }; + let server_options: ServerOptions = + { + run: run, + debug: { + command: run.command, + args: run.args.concat(["-L", path.join(context.extensionPath, "protocol.log")]) } + }; + let client_options: LanguageClientOptions = { documentSelector: "isabelle" }; + + let disposable = + new LanguageClient("Isabelle Language Service", server_options, client_options, false).start(); + context.subscriptions.push(disposable); +} + +export function deactivate() { } diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/test/extension.test.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/test/extension.test.ts Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,22 @@ +// +// Note: This example test is leveraging the Mocha test framework. +// Please refer to their documentation on https://mochajs.org/ for help. +// + +// The module 'assert' provides assertion methods from node +import * as assert from 'assert'; + +// You can import and use all API from the 'vscode' module +// as well as import your extension to test it +import * as vscode from 'vscode'; +import * as myExtension from '../src/extension'; + +// Defines a Mocha test suite to group tests of similar kind together +suite("Extension Tests", () => { + + // Defines a Mocha unit test + test("Something 1", () => { + assert.equal(-1, [1, 2, 3].indexOf(5)); + assert.equal(-1, [1, 2, 3].indexOf(0)); + }); +}); \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/test/index.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/test/index.ts Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,22 @@ +// +// PLEASE DO NOT MODIFY / DELETE UNLESS YOU KNOW WHAT YOU ARE DOING +// +// This file is providing the test runner to use when running extension tests. +// By default the test runner in use is Mocha based. +// +// You can provide your own test runner if you want to override it by exporting +// a function run(testRoot: string, clb: (error:Error) => void) that the extension +// host can call to run the tests. The test runner is expected to use console.log +// to report the results back to the caller. When the tests are finished, return +// a possible error to the callback or null if none. + +var testRunner = require('vscode/lib/testrunner'); + +// You can directly control Mocha options by uncommenting the following lines +// See https://github.com/mochajs/mocha/wiki/Using-mocha-programmatically#set-options for more info +testRunner.configure({ + ui: 'tdd', // the TDD UI is being used in extension.test.ts (suite, test, etc.) + useColors: true // colored output from test results +}); + +module.exports = testRunner; \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/tsconfig.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/tsconfig.json Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,16 @@ +{ + "compilerOptions": { + "module": "commonjs", + "target": "es6", + "outDir": "out", + "lib": [ + "es6" + ], + "sourceMap": true, + "rootDir": "." + }, + "exclude": [ + "node_modules", + ".vscode-test" + ] +} \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/extension/vsc-extension-quickstart.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/vsc-extension-quickstart.md Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,33 @@ +# Welcome to your first VS Code Extension + +## What's in the folder +* This folder contains all of the files necessary for your extension +* `package.json` - this is the manifest file in which you declare your extension and command. +The sample plugin registers a command and defines its title and command name. With this information +VS Code can show the command in the command palette. It doesn’t yet need to load the plugin. +* `src/extension.ts` - this is the main file where you will provide the implementation of your command. +The file exports one function, `activate`, which is called the very first time your extension is +activated (in this case by executing the command). Inside the `activate` function we call `registerCommand`. +We pass the function containing the implementation of the command as the second parameter to +`registerCommand`. + +## Get up and running straight away +* press `F5` to open a new window with your extension loaded +* run your command from the command palette by pressing (`Ctrl+Shift+P` or `Cmd+Shift+P` on Mac) and typing `Hello World` +* set breakpoints in your code inside `src/extension.ts` to debug your extension +* find output from your extension in the debug console + +## Make changes +* you can relaunch the extension from the debug toolbar after changing code in `src/extension.ts` +* you can also reload (`Ctrl+R` or `Cmd+R` on Mac) the VS Code window with your extension to load your changes + +## Explore the API +* you can open the full set of our API when you open the file `node_modules/vscode/vscode.d.ts` + +## Run tests +* open the debug viewlet (`Ctrl+Shift+D` or `Cmd+Shift+D` on Mac) and from the launch configuration dropdown pick `Launch Tests` +* press `F5` to run the tests in a new window with your extension loaded +* see the output of the test result in the debug console +* make changes to `test/extension.test.ts` or create new test files inside the `test` folder + * by convention, the test runner will only consider files matching the name pattern `**.test.ts` + * you can create folders inside the `test` folder to structure your tests any way you want \ No newline at end of file diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/channel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/channel.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,89 @@ +/* Title: Tools/VSCode/src/channel.scala + Author: Makarius + +Channel with JSON RPC protocol. +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream} + +import scala.collection.mutable + + +class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None) +{ + val log: Logger = Logger.make(log_file) + + + /* read message */ + + private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r + + private def read_line(): String = + { + val buffer = new ByteArrayOutputStream(100) + var c = 0 + while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c) + Library.trim_line(buffer.toString(UTF8.charset_name)) + } + + private def read_header(): List[String] = + { + val header = new mutable.ListBuffer[String] + var line = "" + while ({ line = read_line(); line != "" }) header += line + header.toList + } + + private def read_content(n: Int): String = + { + val buffer = new Array[Byte](n) + var i = 0 + var m = 0 + do { + m = in.read(buffer, i, n - i) + if (m != -1) i += m + } + while (m != -1 && n > i) + + if (i == n) new String(buffer, UTF8.charset) + else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)") + } + + def read(): Option[JSON.T] = + { + read_header() match { + case Nil => None + case Content_Length(s) :: _ => + s match { + case Value.Int(n) if n >= 0 => + val msg = read_content(n) + log("IN:\n" + msg) + Some(JSON.parse(msg)) + case _ => error("Bad Content-Length: " + s) + } + case header => error(cat_lines("Malformed header:" :: header)) + } + } + + + /* write message */ + + def write(json: JSON.T) + { + val msg = JSON.Format(json) + log("OUT:\n" + msg) + + val content = UTF8.bytes(msg) + val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n") + out.synchronized { + out.write(header) + out.write(content) + out.flush + } + } +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/document_model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/document_model.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,58 @@ +/* Title: Tools/VSCode/src/document_model.scala + Author: Makarius + +Document model for line-oriented text. +*/ + +package isabelle.vscode + + +import isabelle._ + +import scala.util.parsing.input.CharSequenceReader + + +case class Document_Model( + session: Session, doc: Line.Document, node_name: Document.Node.Name, + changed: Boolean = true) +{ + /* header */ + + def is_theory: Boolean = node_name.is_theory + + lazy val node_header: Document.Node.Header = + if (is_theory) { + val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text) + val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY)) + toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match { + case Some(i) => + session.resources.check_thy_reader("", node_name, + new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command) + case None => Document.Node.no_header + } + } + else Document.Node.no_header + + + /* edits */ + + def text_edits: List[Text.Edit] = + if (changed) List(Text.Edit.insert(0, doc.text)) else Nil + + def node_edits: List[Document.Edit_Text] = + if (changed) { + List(session.header_edit(node_name, node_header), + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(text_edits), + node_name -> + Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) + } + else Nil + + def unchanged: Document_Model = if (changed) copy(changed = false) else this + + + /* snapshot */ + + def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/line.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/line.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,151 @@ +/* Title: Tools/VSCode/src/line.scala + Author: Makarius + +Line-oriented text. +*/ + +package isabelle.vscode + + +import isabelle._ + +import scala.annotation.tailrec + + +object Line +{ + /* position */ + + object Position + { + val zero: Position = Position(0, 0) + } + + sealed case class Position(line: Int, column: Int) + { + def line1: Int = line + 1 + def column1: Int = column + 1 + def print: String = line1.toString + ":" + column1.toString + + def compare(that: Position): Int = + line compare that.line match { + case 0 => column compare that.column + case i => i + } + + private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position = + { + var l = line + var c = column + for (x <- iterator) { + if (is_newline(x)) { l += 1; c = 0 } else c += 1 + } + Position(l, c) + } + + def advance(text: String): Position = + if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n') + + def advance_symbols(text: String): Position = + if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _) + + def advance_codepoints(text: String): Position = + if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10) + } + + + /* range (right-open interval) */ + + sealed case class Range(start: Position, stop: Position) + { + if (start.compare(stop) > 0) + error("Bad line range: " + start.print + ".." + stop.print) + + def print: String = start.print + ".." + stop.print + } + + + /* document with newline as separator (not terminator) */ + + object Document + { + val empty: Document = new Document("", Nil) + + def apply(lines: List[Line]): Document = + if (lines.isEmpty) empty + else new Document(lines.mkString("", "\n", ""), lines) + + def apply(text: String): Document = + if (text.contains('\r')) + apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_)))) + else if (text == "") Document.empty + else new Document(text, Library.split_lines(text).map(Line(_))) + } + + final class Document private(val text: String, val lines: List[Line]) + { + override def toString: String = text + + override def equals(that: Any): Boolean = + that match { + case other: Document => lines == other.lines + case _ => false + } + override def hashCode(): Int = lines.hashCode + + private def position(advance: (Position, String) => Position, offset: Text.Offset): Position = + { + @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = + { + lines_rest match { + case Nil => require(i == 0); Position(lines_count, 0) + case line :: ls => + val n = line.text.length + if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i)) + else move(i - (n + 1), lines_count + 1, ls) + } + } + move(offset, 0, lines) + } + + def position(i: Text.Offset): Position = position(_.advance(_), i) + def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i) + def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i) + + // FIXME symbols, codepoints + def offset(pos: Position): Option[Text.Offset] = + { + val l = pos.line + val c = pos.column + if (0 <= l && l < lines.length) { + val line_offset = + if (l == 0) 0 + else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 }) + if (c <= lines(l).text.length) Some(line_offset + c) else None + } + else None + } + } + + + /* line text */ + + val empty: Line = new Line("") + def apply(text: String): Line = if (text == "") empty else new Line(text) +} + +final class Line private(val text: String) +{ + require(text.forall(c => c != '\r' && c != '\n')) + + lazy val length_symbols: Int = Symbol.iterator(text).length + lazy val length_codepoints: Int = Word.codepoint_iterator(text).length + + override def equals(that: Any): Boolean = + that match { + case other: Line => text == other.text + case _ => false + } + override def hashCode(): Int = text.hashCode + override def toString: String = text +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/logger.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/logger.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,34 @@ +/* Title: Tools/VSCode/src/logger.scala + Author: Makarius + +Minimal logging support. +*/ + +package isabelle.vscode + + +import isabelle._ + + +object Logger +{ + def make(log_file: Option[Path]): Logger = + log_file match { case Some(file) => new File_Logger(file) case None => No_Logger } +} + +trait Logger +{ + def apply(msg: => String): Unit +} + +object No_Logger extends Logger +{ + def apply(msg: => String) { } +} + +class File_Logger(path: Path) extends Logger +{ + def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } } + + override def toString: String = path.toString +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/protocol.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/protocol.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,299 @@ +/* Title: Tools/VSCode/src/protocol.scala + Author: Makarius + +Message formats for Language Server Protocol 2.0, see +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md +*/ + +package isabelle.vscode + + +import isabelle._ + + +object Protocol +{ + /* abstract message */ + + object Message + { + val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0") + } + + + /* notification */ + + object Notification + { + def apply(method: String, params: JSON.T): JSON.T = + Message.empty + ("method" -> method) + ("params" -> params) + + def unapply(json: JSON.T): Option[(String, Option[JSON.T])] = + for { + method <- JSON.string(json, "method") + params = JSON.value(json, "params") + } yield (method, params) + } + + class Notification0(name: String) + { + def unapply(json: JSON.T): Option[Unit] = + json match { + case Notification(method, _) if method == name => Some(()) + case _ => None + } + } + + + /* request message */ + + sealed case class Id(id: Any) + { + require( + id.isInstanceOf[Int] || + id.isInstanceOf[Long] || + id.isInstanceOf[Double] || + id.isInstanceOf[String]) + + override def toString: String = id.toString + } + + object RequestMessage + { + def apply(id: Id, method: String, params: JSON.T): JSON.T = + Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params) + + def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] = + for { + id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id") + method <- JSON.string(json, "method") + params = JSON.value(json, "params") + } yield (Id(id), method, params) + } + + class Request0(name: String) + { + def unapply(json: JSON.T): Option[Id] = + json match { + case RequestMessage(id, method, _) if method == name => Some(id) + case _ => None + } + } + + + /* response message */ + + object ResponseMessage + { + def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T = + Message.empty + ("id" -> id.id) ++ + (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++ + (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty }) + + def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T = + if (error == "") apply(id, result = result) + else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error))) + } + + sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) + { + def json: JSON.T = + Map("code" -> code, "message" -> message) ++ + (data match { case Some(x) => Map("data" -> x) case None => Map.empty }) + } + + object ErrorCodes + { + val ParseError = -32700 + val InvalidRequest = -32600 + val MethodNotFound = -32601 + val InvalidParams = -32602 + val InternalError = -32603 + val serverErrorStart = -32099 + val serverErrorEnd = -32000 + } + + + /* init and exit */ + + object Initialize extends Request0("initialize") + { + def reply(id: Id, error: String): JSON.T = + ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error) + } + + object ServerCapabilities + { + val json: JSON.T = + Map("textDocumentSync" -> 1, "hoverProvider" -> true) + } + + object Shutdown extends Request0("shutdown") + { + def reply(id: Id, error: String): JSON.T = + ResponseMessage.strict(id, Some("OK"), error) + } + + object Exit extends Notification0("exit") + + + /* document positions */ + + object Position + { + def apply(pos: Line.Position): JSON.T = + Map("line" -> pos.line, "character" -> pos.column) + + def unapply(json: JSON.T): Option[Line.Position] = + for { + line <- JSON.int(json, "line") + column <- JSON.int(json, "character") + } yield Line.Position(line, column) + } + + object Range + { + def apply(range: Line.Range): JSON.T = + Map("start" -> Position(range.start), "end" -> Position(range.stop)) + + def unapply(json: JSON.T): Option[Line.Range] = + (JSON.value(json, "start"), JSON.value(json, "end")) match { + case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop)) + case _ => None + } + } + + object Location + { + def apply(uri: String, range: Line.Range): JSON.T = + Map("uri" -> uri, "range" -> Range(range)) + + def unapply(json: JSON.T): Option[(String, Line.Range)] = + for { + uri <- JSON.string(json, "uri") + range_json <- JSON.value(json, "range") + range <- Range.unapply(range_json) + } yield (uri, range) + } + + object TextDocumentPosition + { + def unapply(json: JSON.T): Option[(String, Line.Position)] = + for { + doc <- JSON.value(json, "textDocument") + uri <- JSON.string(doc, "uri") + pos_json <- JSON.value(json, "position") + pos <- Position.unapply(pos_json) + } yield (uri, pos) + } + + + /* diagnostic messages */ + + object MessageType + { + val Error = 1 + val Warning = 2 + val Info = 3 + val Log = 4 + } + + object DisplayMessage + { + def apply(message_type: Int, message: String, show: Boolean = true): JSON.T = + Notification(if (show) "window/showMessage" else "window/logMessage", + Map("type" -> message_type, "message" -> message)) + } + + + /* document edits */ + + object DidOpenTextDocument + { + def unapply(json: JSON.T): Option[(String, String, Long, String)] = + json match { + case Notification("textDocument/didOpen", Some(params)) => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + lang <- JSON.string(doc, "languageId") + version <- JSON.long(doc, "version") + text <- JSON.string(doc, "text") + } yield (uri, lang, version, text) + case _ => None + } + } + + + sealed abstract class TextDocumentContentChange + case class TextDocumentContent(text: String) extends TextDocumentContentChange + case class TextDocumentChange(range: Line.Range, range_length: Int, text: String) + extends TextDocumentContentChange + + object TextDocumentContentChange + { + def unapply(json: JSON.T): Option[TextDocumentContentChange] = + for { text <- JSON.string(json, "text") } + yield { + (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match { + case (Some(Range(range)), Some(range_length)) => + TextDocumentChange(range, range_length, text) + case _ => TextDocumentContent(text) + } + } + } + + object DidChangeTextDocument + { + def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] = + json match { + case Notification("textDocument/didChange", Some(params)) => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + version <- JSON.long(doc, "version") + changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _) + } yield (uri, version, changes) + case _ => None + } + } + + class TextDocumentNotification(name: String) + { + def unapply(json: JSON.T): Option[String] = + json match { + case Notification(method, Some(params)) if method == name => + for { + doc <- JSON.value(params, "textDocument") + uri <- JSON.string(doc, "uri") + } yield uri + case _ => None + } + } + + object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose") + object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave") + + + /* hover request */ + + object Hover + { + def unapply(json: JSON.T): Option[(Id, String, Line.Position)] = + json match { + case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) => + Some((id, uri, pos)) + case _ => None + } + + def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T = + { + val res = + result match { + case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range)) + case None => Map("contents" -> Nil) + } + ResponseMessage(id, Some(res)) + } + } +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/server.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/server.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,354 @@ +/* Title: Tools/VSCode/src/server.scala + Author: Makarius + +Server for VS Code Language Server Protocol 2.0, see also +https://github.com/Microsoft/language-server-protocol +https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.io.{PrintStream, OutputStream} + +import scala.annotation.tailrec + + +object Server +{ + /* Isabelle tool wrapper */ + + private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") + + val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => + { + var log_file: Option[Path] = None + var dirs: List[Path] = Nil + var logic = default_logic + var modes: List[String] = Nil + var options = Options.init() + + val getopts = Getopts(""" +Usage: isabelle vscode_server [OPTIONS] + + Options are: + -L FILE enable logging on FILE + -d DIR include session directory + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) + -m MODE add print mode for output + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + + Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. +""", + "L:" -> (arg => log_file = Some(Path.explode(arg))), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "o:" -> (arg => options = options + arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + if (!Build.build(options = options, build_heap = true, no_build = true, + dirs = dirs, sessions = List(logic)).ok) + error("Missing logic image " + quote(logic)) + + val channel = new Channel(System.in, System.out, log_file) + val server = new Server(channel, options, logic, dirs, modes) + + // prevent spurious garbage on the main protocol channel + val orig_out = System.out + try { + System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) + server.start() + } + finally { System.setOut(orig_out) } + }) + + + /* server state */ + + sealed case class State( + session: Option[Session] = None, + models: Map[String, Document_Model] = Map.empty) +} + +class Server( + channel: Channel, + options: Options, + session_name: String = Server.default_logic, + session_dirs: List[Path] = Nil, + modes: List[String] = Nil) +{ + /* server state */ + + private val state = Synchronized(Server.State()) + + def session: Session = state.value.session getOrElse error("Session inactive") + def resources: URI_Resources = session.resources.asInstanceOf[URI_Resources] + + + /* init and exit */ + + def initialize(reply: String => Unit) + { + val content = Build.session_content(options, false, session_dirs, session_name) + val resources = + new URI_Resources(content.loaded_theories, content.known_theories, content.syntax) + + val session = + new Session(resources) { + override def output_delay = options.seconds("editor_output_delay") + override def prune_delay = options.seconds("editor_prune_delay") + override def syslog_limit = options.int("editor_syslog_limit") + override def reparse_limit = options.int("editor_reparse_limit") + } + + var session_phase: Session.Consumer[Session.Phase] = null + session_phase = + Session.Consumer(getClass.getName) { + case Session.Ready => + session.phase_changed -= session_phase + session.update_options(options) + reply("") + case Session.Failed => + session.phase_changed -= session_phase + reply("Prover startup failed") + case _ => + } + session.phase_changed += session_phase + + session.start(receiver => + Isabelle_Process(options = options, logic = session_name, dirs = session_dirs, + modes = modes, receiver = receiver)) + + state.change(_.copy(session = Some(session))) + } + + def shutdown(reply: String => Unit) + { + state.change(st => + st.session match { + case None => reply("Prover inactive"); st + case Some(session) => + var session_phase: Session.Consumer[Session.Phase] = null + session_phase = + Session.Consumer(getClass.getName) { + case Session.Inactive => + session.phase_changed -= session_phase + reply("") + case _ => + } + session.phase_changed += session_phase + session.stop() + st.copy(session = None) + }) + } + + def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) } + + + /* document management */ + + private val delay_flush = + Standard_Thread.delay_last(options.seconds("editor_input_delay")) { + state.change(st => + { + val models = st.models + val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList + val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit + val models1 = + (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) }) + + session.update(Document.Blobs.empty, edits) + st.copy(models = models1) + }) + } + + def update_document(uri: String, text: String) + { + state.change(st => + { + val node_name = resources.node_name(uri) + val model = Document_Model(session, Line.Document(text), node_name) + st.copy(models = st.models + (uri -> model)) + }) + delay_flush.invoke() + } + + + /* tooltips -- see $ISABELLE_HOME/src/Tools/jEdit/rendering.scala */ + + def hover(uri: String, pos: Line.Position): Option[(Line.Range, List[String])] = + for { + model <- state.value.models.get(uri) + snapshot = model.snapshot() + offset <- model.doc.offset(pos) + info <- tooltip(snapshot, Text.Range(offset, offset + 1)) + } yield { + val r = Line.Range(model.doc.position(info.range.start), model.doc.position(info.range.stop)) + val s = Pretty.string_of(info.info, margin = tooltip_margin.toDouble) + (r, List("```\n" + s + "\n```")) + } + + private val tooltip_descriptions = + Map( + Markup.CITATION -> "citation", + Markup.TOKEN_RANGE -> "inner syntax token", + Markup.FREE -> "free variable", + Markup.SKOLEM -> "skolem variable", + Markup.BOUND -> "bound variable", + Markup.VAR -> "schematic variable", + Markup.TFREE -> "free type variable", + Markup.TVAR -> "schematic type variable") + + private val tooltip_elements = + Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, + Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, + Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, + Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) + + private def pretty_typing(kind: String, body: XML.Body): XML.Tree = + Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) + + private def timing_threshold: Double = options.real("jedit_timing_threshold") + + def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[XML.Body]] = + { + def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])], + r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] = + { + val r = snapshot.convert(r0) + val (t, info) = prev.info + if (prev.range == r) + Text.Info(r, (t, info :+ p)) + else Text.Info(r, (t, Vector(p))) + } + + val results = + snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( + range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ => + { + case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => + Some(Text.Info(r, (t1 + t2, info))) + + case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) + if kind != "" && + kind != Markup.ML_DEF && + kind != Markup.ML_OPEN && + kind != Markup.ML_STRUCTURE => + val kind1 = Word.implode(Word.explode('_', kind)) + val txt1 = + if (name == "") kind1 + else if (kind1 == "") quote(name) + else kind1 + " " + quote(name) + val t = prev.info._1 + val txt2 = + if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold) + "\n" + t.message + else "" + Some(add(prev, r, (true, XML.Text(txt1 + txt2)))) + + case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) => + val text = "doc " + quote(name) + Some(add(prev, r, (true, XML.Text(text)))) + + case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => + Some(add(prev, r, (true, XML.Text("URL " + quote(name))))) + + case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) + if name == Markup.SORTING || name == Markup.TYPING => + Some(add(prev, r, (true, pretty_typing("::", body)))) + + case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) => + Some(add(prev, r, (true, Pretty.block(0, body)))) + + case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => + Some(add(prev, r, (false, pretty_typing("ML:", body)))) + + case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) => + val lang = Word.implode(Word.explode('_', language)) + Some(add(prev, r, (true, XML.Text("language: " + lang)))) + + case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) => + val descr = if (kind == "") "expression" else "expression: " + kind + Some(add(prev, r, (true, XML.Text(descr)))) + + case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => + Some(add(prev, r, (true, XML.Text("Markdown: paragraph")))) + case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) => + Some(add(prev, r, (true, XML.Text("Markdown: " + kind)))) + + case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => + tooltip_descriptions.get(name). + map(descr => add(prev, r, (true, XML.Text(descr)))) + }).map(_.info) + + results.map(_.info).flatMap(res => res._2.toList) match { + case Nil => None + case tips => + val r = Text.Range(results.head.range.start, results.last.range.stop) + val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2) + Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips))) + } + } + + def tooltip_margin: Int = options.int("jedit_tooltip_margin") + + + /* main loop */ + + def start() + { + channel.log("\nServer started " + Date.now()) + + def handle(json: JSON.T) + { + try { + json match { + case Protocol.Initialize(id) => + def initialize_reply(err: String) + { + channel.write(Protocol.Initialize.reply(id, err)) + if (err == "") { + channel.write(Protocol.DisplayMessage(Protocol.MessageType.Info, + "Welcome to Isabelle/" + session_name + " (" + Distribution.version + ")")) + } + else channel.write(Protocol.DisplayMessage(Protocol.MessageType.Error, err)) + } + initialize(initialize_reply _) + case Protocol.Shutdown(id) => + shutdown((error: String) => channel.write(Protocol.Shutdown.reply(id, error))) + case Protocol.Exit => + exit() + case Protocol.DidOpenTextDocument(uri, lang, version, text) => + update_document(uri, text) + case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) => + update_document(uri, text) + case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri) + case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri) + case Protocol.Hover(id, uri, pos) => + channel.write(Protocol.Hover.reply(id, hover(uri, pos))) + case _ => channel.log("### IGNORED") + } + } + catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) } + } + + @tailrec def loop() + { + channel.read() match { + case Some(json) => + json match { + case bulk: List[_] => bulk.foreach(handle(_)) + case _ => handle(json) + } + loop() + case None => channel.log("### TERMINATE") + } + } + loop() + } +} diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/uri_resources.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/uri_resources.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,43 @@ +/* Title: Tools/VSCode/src/uri_resources.scala + Author: Makarius + +Resources based on file-system URIs. +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.net.{URI, URISyntaxException} +import java.io.{File => JFile} + + +object URI_Resources +{ + def is_wellformed(uri: String): Boolean = + try { new JFile(new URI(uri)); true } + catch { case _: URISyntaxException | _: IllegalArgumentException => false } + + def canonical_file(uri: String): JFile = + new JFile(new URI(uri)).getCanonicalFile + + val empty: URI_Resources = + new URI_Resources(Set.empty, Map.empty, Outer_Syntax.empty) +} + +class URI_Resources( + loaded_theories: Set[String], + known_theories: Map[String, Document.Node.Name], + base_syntax: Outer_Syntax) + extends Resources(loaded_theories, known_theories, base_syntax) +{ + def node_name(uri: String): Document.Node.Name = + { + val file = URI_Resources.canonical_file(uri) // FIXME wellformed!? + val node = file.getPath + val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("") + val master_dir = if (theory == "") "" else file.getParent + Document.Node.Name(node, master_dir, theory) + } +}