From a20bb113b484cffcb5a0e2e40a9d0bea6ee4b754 Mon Sep 17 00:00:00 2001 From: Michael Raymond Date: Sat, 3 Oct 2020 10:16:54 +0100 Subject: [PATCH 1/3] naive state tracking --- src/providers/hover.ts | 217 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 217 insertions(+) diff --git a/src/providers/hover.ts b/src/providers/hover.ts index 3d98d54..b09ee8e 100644 --- a/src/providers/hover.ts +++ b/src/providers/hover.ts @@ -1,7 +1,219 @@ import * as vscode from "vscode" import { IdrisClient } from "idris-ide-client" +import { deflate } from "zlib" export const selector = { language: "idris" } +type DocState = + | "code" // abc + | "line-comment" // -- abc + | "block-comment" // {- abc -} + | "doc-comment" // ||| abc + | "string" // "abc" + | "multi-line-string" // """abc""" + +type Delimiter = + | "string-delim" + | "multi-line-string-delim" + | "new-line" + | "start-line-comment" + | "start-block-comment" + | "end-block-comment" + | "start-doc-comment" + +class DocStateParser { + private text: string + private endPos: vscode.Position + private state: DocState + private line: number // current line number in document + private col: number // current column number on current line + private pos: number // position in text-string + + constructor(text: string, endPos: vscode.Position) { + this.text = text + this.endPos = endPos + this.state = "code" + this.line = 0 + this.col = 0 + this.pos = 0 + } + + static nextState(currentState: DocState, delim: Delimiter): DocState { + switch (currentState) { + case "code": + switch (delim) { + case "string-delim": + return "string" + case "multi-line-string-delim": + return "multi-line-string" + case "start-line-comment": + return "line-comment" + case "start-block-comment": + return "block-comment" + case "start-doc-comment": + return "doc-comment" + default: + return "code" + } + case "line-comment": + switch (delim) { + case "new-line": + return "code" + default: + return "line-comment" + } + case "block-comment": + switch (delim) { + case "end-block-comment": + return "code" + default: + return "block-comment" + } + case "doc-comment": + switch (delim) { + case "new-line": + return "code" + default: + return "doc-comment" + } + case "string": + switch (delim) { + case "string-delim": + return "code" + default: + return "string" + } + case "multi-line-string": + switch (delim) { + case "multi-line-string-delim": + return "code" + default: + return "multi-line-string" + } + } + } + + incLine(): void { + this.line += 1 + this.col = 0 + } + + consumeNextDelim(): Delimiter | null { + switch (this.state) { + case "code": { + if ( + this.text[this.pos] === '"' && + this.text[this.pos + 1] === '"' && + this.text[this.pos + 2] === '"' + ) { + this.pos += 3 + return "multi-line-string-delim" + } else if (this.text[this.pos] === '"') { + this.pos += 1 + return "string-delim" + } else if ( + this.text[this.pos] === "-" && + this.text[this.pos + 1] === "-" + ) { + this.pos += 2 + return "start-line-comment" + } else if ( + this.text[this.pos] === "{" && + this.text[this.pos + 1] === "-" + ) { + this.pos += 2 + return "start-block-comment" + } else if ( + this.text[this.pos] === "|" && + this.text[this.pos + 1] === "|" && + this.text[this.pos + 2] === "|" + ) { + this.pos += 3 + return "start-doc-comment" + } else return null + } + case "line-comment": { + if (this.text[this.pos] === "\n") { + this.incLine() + this.pos += 1 + return "new-line" + } else { + return null + } + } + case "block-comment": { + if (this.text[this.pos] === "-" && this.text[this.pos + 1] === "}") { + this.pos += 2 + return "end-block-comment" + } else { + return null + } + } + case "doc-comment": { + if (this.text[this.pos] === "\n") { + this.incLine() + this.pos += 1 + return "new-line" + } else { + return null + } + } + case "string": { + if (this.text[this.pos] === '"') { + let escapes = 0 + while (this.text[this.pos - (1 + escapes)] === "\\") { + escapes += 1 + } + const quotesAreEscaped = escapes % 2 !== 0 + if (quotesAreEscaped) return null + else { + this.pos += 1 + return "string-delim" + } + } else { + return null + } + } + case "multi-line-string": { + if ( + this.text[this.pos] === '"' && + this.text[this.pos + 1] === '"' && + this.text[this.pos + 2] === '"' + ) { + let escapes = 0 + while (this.text[this.pos - (1 + escapes)] === "\\") { + escapes += 1 + } + const quotesAreEscaped = escapes % 2 !== 0 + if (quotesAreEscaped) return null + else { + this.pos += 3 + return "multi-line-string-delim" + } + } else { + return null + } + } + } + } + + atEndPos(): boolean { + return this.line <= this.endPos.line && this.col <= this.endPos.character + } + + parseToEndPos(): DocState { + while (this.atEndPos()) { + const delim = this.consumeNextDelim() + if (delim) { + this.state = DocStateParser.nextState(this.state, delim) + } else { + if (this.text[this.pos] === "\n") this.incLine() + this.pos += 1 + } + } + return this.state + } +} + export class Provider implements vscode.HoverProvider { private client: IdrisClient @@ -17,6 +229,11 @@ export class Provider implements vscode.HoverProvider { return new Promise(async (res) => { const range = document.getWordRangeAtPosition(position) if (!range) res(null) + + const parser = new DocStateParser(document.getText(), position) + const docStateAtPos = parser.parseToEndPos() + if (docStateAtPos !== "code") res(null) + const name = document.getText(range) const reply = await this.client.typeOf(name) if (reply.ok) { From b2dfceaa506c50cd4fc964cbd5fe4f7208db208e Mon Sep 17 00:00:00 2001 From: Michael Raymond Date: Sat, 3 Oct 2020 12:00:29 +0100 Subject: [PATCH 2/3] Fix method binding --- src/extension.ts | 8 +++++--- src/providers/hover.ts | 27 ++++++++++++++++++++++----- 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/src/extension.ts b/src/extension.ts index d30aa8d..ca67498 100644 --- a/src/extension.ts +++ b/src/extension.ts @@ -45,9 +45,11 @@ export const activate = (context: vscode.ExtensionContext) => { idrisProc = spawn(config.idrisPath, ["--ide-mode"]) - idrisProc.on("error", (_ => { - vscode.window.showErrorMessage("Could not start Idris process with: " + config.idrisPath) - })) + idrisProc.on("error", (_) => { + vscode.window.showErrorMessage( + "Could not start Idris process with: " + config.idrisPath + ) + }) if (!(idrisProc.stdin && idrisProc.stdout)) { throw "Failed to start Idris process." // unreachable diff --git a/src/providers/hover.ts b/src/providers/hover.ts index b09ee8e..5c7de40 100644 --- a/src/providers/hover.ts +++ b/src/providers/hover.ts @@ -1,6 +1,5 @@ import * as vscode from "vscode" import { IdrisClient } from "idris-ide-client" -import { deflate } from "zlib" export const selector = { language: "idris" } type DocState = @@ -35,6 +34,11 @@ class DocStateParser { this.line = 0 this.col = 0 this.pos = 0 + + this.consumeNextDelim = this.consumeNextDelim.bind(this) + this.atEndPos = this.atEndPos.bind(this) + this.incLine = this.incLine.bind(this) + this.parseToEndPos = this.parseToEndPos.bind(this) } static nextState(currentState: DocState, delim: Delimiter): DocState { @@ -106,21 +110,25 @@ class DocStateParser { this.text[this.pos + 2] === '"' ) { this.pos += 3 + this.col += 3 return "multi-line-string-delim" } else if (this.text[this.pos] === '"') { this.pos += 1 + this.col += 1 return "string-delim" } else if ( this.text[this.pos] === "-" && this.text[this.pos + 1] === "-" ) { this.pos += 2 + this.col += 2 return "start-line-comment" } else if ( this.text[this.pos] === "{" && this.text[this.pos + 1] === "-" ) { this.pos += 2 + this.col += 2 return "start-block-comment" } else if ( this.text[this.pos] === "|" && @@ -128,6 +136,7 @@ class DocStateParser { this.text[this.pos + 2] === "|" ) { this.pos += 3 + this.col += 3 return "start-doc-comment" } else return null } @@ -143,6 +152,7 @@ class DocStateParser { case "block-comment": { if (this.text[this.pos] === "-" && this.text[this.pos + 1] === "}") { this.pos += 2 + this.col += 2 return "end-block-comment" } else { return null @@ -167,6 +177,7 @@ class DocStateParser { if (quotesAreEscaped) return null else { this.pos += 1 + this.col += 1 return "string-delim" } } else { @@ -187,6 +198,7 @@ class DocStateParser { if (quotesAreEscaped) return null else { this.pos += 3 + this.col += 3 return "multi-line-string-delim" } } else { @@ -197,17 +209,22 @@ class DocStateParser { } atEndPos(): boolean { - return this.line <= this.endPos.line && this.col <= this.endPos.character + return this.line >= this.endPos.line && this.col >= this.endPos.character } parseToEndPos(): DocState { - while (this.atEndPos()) { + while (!this.atEndPos()) { const delim = this.consumeNextDelim() if (delim) { this.state = DocStateParser.nextState(this.state, delim) } else { - if (this.text[this.pos] === "\n") this.incLine() - this.pos += 1 + if (this.text[this.pos] === "\n") { + this.incLine() + this.pos += 1 + } else { + this.pos += 1 + this.col += 1 + } } } return this.state From 8cbafe8406d80f537793047e9cbba48de3810a72 Mon Sep 17 00:00:00 2001 From: Michael Raymond Date: Thu, 22 Oct 2020 21:25:28 +0100 Subject: [PATCH 3/3] Update changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9de33a9..13d4f40 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ - Bump dev dependencies to appease our dependabot overlords ### Fixed +- Fix hover text in inappropriate contexts (https://github.com/meraymond2/idris-vscode/issues/1) # 0.0.4 ### Added