basic support for VSCode Language Server protocol;
minimal extension for VSCode editor;
--- 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/
--- 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)
--- 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"
)
--- /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
--- /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"
+ }
+ ]
+}
--- /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
--- /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
--- /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
--- /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.
Binary file src/Tools/VSCode/extension/isabelle.png has changed
--- /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": [
+ ["(", ")"],
+ ["[", "]"],
+ ["{", "}"],
+ ["<", ">"],
+ ["«", "»"],
+ ["‹", "›"],
+ ["⟨", "⟩"],
+ ["⌈", "⌉"],
+ ["⌊", "⌋"],
+ ["⦇", "⦈"],
+ ["⟦", "⟧"],
+ ["⦃", "⦄"]
+ ]
+}
--- /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
--- /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() { }
--- /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
--- /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
--- /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
--- /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
--- /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
+ }
+ }
+}
--- /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)
+}
--- /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
+}
--- /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
+}
--- /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))
+ }
+ }
+}
--- /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()
+ }
+}
--- /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)
+ }
+}
