From f95e49f75855ab8b164b3dddb78a7000b122de44 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Tue, 18 Jul 2017 10:41:53 +0200 Subject: [PATCH] Various improvements and fixes Fixes #154: Display the general idris compiler error message Use syntax highlighting in the error panel when idris reports source code snippets. Relates #171: Improve literate idris support: When in literate mode prefix source code inserted by atom with `>` characters where appropriate Fixes #131: Use syntax highlighting when using the doc command or `:doc` in the REPL. Update message panel version --- lib/idris-controller.coffee | 78 ++++++++++++++++++++++++++++++------- package.json | 2 +- 2 files changed, 66 insertions(+), 14 deletions(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index eb78e87..9d93b8b 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -7,6 +7,7 @@ IdrisModel = require './idris-model' Ipkg = require './utils/ipkg' Symbol = require './utils/symbol' editorHelper = require './utils/editor' +highlighter = require './utils/highlighter' class IdrisController errorMarkers: [] @@ -31,6 +32,25 @@ class IdrisController isIdrisFile: (uri) -> uri?.match? /\.idr$/ + # check if this is a literate idris file + isLiterateGrammar: () -> + @getEditor().getGrammar().scopeName == "source.idris.literate" + + # prefix code lines with "> " if we are in the literate grammar + prefixLiterateClause: (clause) => + birdPattern = ///^ # beginning of line + > # the bird + (\s)+ # some whitespace + /// + + if (@isLiterateGrammar()) + for line in clause + if line.match birdPattern + line + else "> " + line + else + clause + createMarker: (editor, range, type) -> marker = editor.markBufferRange(range, invalidate: 'never') editor.decorateMarker marker, @@ -65,6 +85,7 @@ class IdrisController @messages.hide() @model.setCompilerOptions compilerOptions + # get the currently active text editor getEditor: () -> atom.workspace.getActiveTextEditor() @@ -198,6 +219,7 @@ class IdrisController .flatMap => @model.caseSplit line + 1, word .subscribe successHandler, @displayErrors + # add a new clause to a function doAddClause: ({ target }) => editor = @getEditor() @saveFile editor @@ -205,8 +227,8 @@ class IdrisController line = editor.getLastCursor().getBufferRow() word = @getWordUnderCursor editor - successHandler = ({ responseType, msg }) -> - [clause] = msg + successHandler = ({ responseType, msg }) => + [clause] = @prefixLiterateClause msg editor.transact -> editorHelper.moveToNextEmptyLine editor @@ -225,6 +247,7 @@ class IdrisController .flatMap => @model.addClause line + 1, word .subscribe successHandler, @displayErrors + # use special syntax for proof obligation clauses doAddProofClause: ({ target }) => editor = @getEditor() @saveFile editor @@ -232,8 +255,8 @@ class IdrisController line = editor.getLastCursor().getBufferRow() word = @getWordUnderCursor editor - successHandler = ({ responseType, msg }) -> - [clause] = msg + successHandler = ({ responseType, msg }) => + [clause] = @prefixLiterateClause msg editor.transact -> editorHelper.moveToNextEmptyLine editor @@ -252,6 +275,7 @@ class IdrisController .flatMap => @model.addProofClause line + 1, word .subscribe successHandler, @displayErrors + # add a with view doMakeWith: ({ target }) => editor = @getEditor() @saveFile editor @@ -259,8 +283,8 @@ class IdrisController line = editor.getLastCursor().getBufferRow() word = @getWordUnderCursor editor - successHandler = ({ responseType, msg }) -> - [clause] = msg + successHandler = ({ responseType, msg }) => + [clause] = @prefixLiterateClause msg editor.transact -> # Delete old line, insert the new with block editor.deleteLine() @@ -277,6 +301,7 @@ class IdrisController .flatMap => @model.makeWith line + 1, word .subscribe successHandler, @displayErrors + # construct a lemma from a hole doMakeLemma: ({ target }) => editor = @getEditor() @saveFile editor @@ -284,8 +309,12 @@ class IdrisController line = editor.getLastCursor().getBufferRow() word = @getWordUnderCursor editor - successHandler = ({ responseType, msg }) -> + successHandler = ({ responseType, msg }) => + # param1 contains the code which replaces the hole + # param2 contains the code for the lemma function [lemty, param1, param2] = msg + param2 = @prefixLiterateClause param2 + editor.transact -> if lemty == ':metavariable-lemma' # Move the cursor to the beginning of the word @@ -325,6 +354,7 @@ class IdrisController .flatMap => @model.makeLemma line + 1, word .subscribe successHandler, @displayErrors + # create a case statement doMakeCase: ({ target }) => editor = @getEditor() @saveFile editor @@ -332,8 +362,9 @@ class IdrisController line = editor.getLastCursor().getBufferRow() word = @getWordUnderCursor editor - successHandler = ({ responseType, msg }) -> - [clause] = msg + successHandler = ({ responseType, msg }) => + [clause] = @prefixLiterateClause msg + editor.transact -> # Delete old line, insert the new case block editor.deleteLine() @@ -349,6 +380,7 @@ class IdrisController .flatMap => @model.makeCase line + 1, word .subscribe successHandler, @displayErrors + # show all holes in the current file showHoles: ({ target }) => editor = @getEditor() @saveFile editor @@ -370,6 +402,7 @@ class IdrisController .flatMap => @model.holes 80 .subscribe successHandler, @displayErrors + # replace a hole with a proof doProofSearch: ({ target }) => editor = @getEditor() @saveFile editor @@ -397,6 +430,7 @@ class IdrisController .flatMap => @model.proofSearch line + 1, word .subscribe successHandler, @displayErrors + # get the definition of a function or type printDefinition: ({ target }) => editor = @getEditor() @saveFile editor @@ -422,6 +456,7 @@ class IdrisController .catch (e) => @model.printDefinition word .subscribe successHandler, @displayErrors + # open the repl window openREPL: ({ target }) => uri = @getEditor().getURI() @@ -437,6 +472,7 @@ class IdrisController .filter ({ responseType }) -> responseType == 'return' .subscribe successHandler, @displayErrors + # open the apropos window apropos: ({ target }) => uri = @getEditor().getURI() @@ -452,27 +488,43 @@ class IdrisController .filter ({ responseType }) -> responseType == 'return' .subscribe successHandler, @displayErrors + # generic function to display errors in the status bar displayErrors: (err) => @messages.attach() @messages.show() @messages.clear() @messages.setTitle ' Idris Errors', true - @messages.add new PlainMessageView - message: "Errors (#{err.warnings.length})" - className: 'idris-error' + # display the general error message + if err.message? + @messages.add new PlainMessageView + raw: true + message: "
" + err.message + "
" + className: "preview" for warning in err.warnings + type = warning[3] + highlightingInfo = warning[4] + highlighting = highlighter.highlight type, highlightingInfo + info = highlighter.highlightToString highlighting + line = warning[1][0] character = warning[1][1] uri = warning[0].replace("./", err.cwd + "/") + # this provides information about the line and column of the error @messages.add new LineMessageView line: line character: character - preview: warning[3] file: uri + # this provides a highlighted version of the error message + # returned by idris + @messages.add new PlainMessageView + raw: true + message: "
" + info + "
" + className: "preview" + editor = atom.workspace.getActiveTextEditor() if line > 0 && uri == editor.getURI() startPoint = warning[1] diff --git a/package.json b/package.json index 821eac5..9662ace 100644 --- a/package.json +++ b/package.json @@ -40,7 +40,7 @@ }, "consumedServices": {}, "dependencies": { - "atom-message-panel": "^1.2.7", + "atom-message-panel": "^1.3.0", "bennu": "17.3.0", "nu-stream": "3.3.1", "rx-lite": "4.0.0",