Skip to content

Commit

Permalink
Various improvements and fixes
Browse files Browse the repository at this point in the history 
Fixes idris-hackers#154: Display the general idris compiler error message

Use syntax highlighting in the error panel when idris reports source code snippets.

Relates idris-hackers#171: Improve literate idris support: When in literate mode prefix source code inserted by atom with `>` characters where appropriate

Fixes idris-hackers#131: Use syntax highlighting when using the doc command or `:doc` in the REPL.

Update message panel version
  • Loading branch information
Markus Klink committed Jul 18, 2017
1 parent 011cd6c commit f95e49f
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 14 deletions.
78 changes: 65 additions & 13 deletions lib/idris-controller.coffee
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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: []
Expand All @@ -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,
Expand Down Expand Up @@ -65,6 +85,7 @@ class IdrisController
@messages.hide()
@model.setCompilerOptions compilerOptions

# get the currently active text editor
getEditor: () ->
atom.workspace.getActiveTextEditor()

Expand Down Expand Up @@ -198,15 +219,16 @@ class IdrisController
.flatMap => @model.caseSplit line + 1, word
.subscribe successHandler, @displayErrors

# add a new clause to a function
doAddClause: ({ target }) =>
editor = @getEditor()
@saveFile editor
uri = editor.getURI()
line = editor.getLastCursor().getBufferRow()
word = @getWordUnderCursor editor

successHandler = ({ responseType, msg }) ->
[clause] = msg
successHandler = ({ responseType, msg }) =>
[clause] = @prefixLiterateClause msg
editor.transact ->
editorHelper.moveToNextEmptyLine editor

Expand All @@ -225,15 +247,16 @@ class IdrisController
.flatMap => @model.addClause line + 1, word
.subscribe successHandler, @displayErrors

# use special syntax for proof obligation clauses
doAddProofClause: ({ target }) =>
editor = @getEditor()
@saveFile editor
uri = editor.getURI()
line = editor.getLastCursor().getBufferRow()
word = @getWordUnderCursor editor

successHandler = ({ responseType, msg }) ->
[clause] = msg
successHandler = ({ responseType, msg }) =>
[clause] = @prefixLiterateClause msg
editor.transact ->
editorHelper.moveToNextEmptyLine editor

Expand All @@ -252,15 +275,16 @@ class IdrisController
.flatMap => @model.addProofClause line + 1, word
.subscribe successHandler, @displayErrors

# add a with view
doMakeWith: ({ target }) =>
editor = @getEditor()
@saveFile editor
uri = editor.getURI()
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()
Expand All @@ -277,15 +301,20 @@ class IdrisController
.flatMap => @model.makeWith line + 1, word
.subscribe successHandler, @displayErrors

# construct a lemma from a hole
doMakeLemma: ({ target }) =>
editor = @getEditor()
@saveFile editor
uri = editor.getURI()
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
Expand Down Expand Up @@ -325,15 +354,17 @@ class IdrisController
.flatMap => @model.makeLemma line + 1, word
.subscribe successHandler, @displayErrors

# create a case statement
doMakeCase: ({ target }) =>
editor = @getEditor()
@saveFile editor
uri = editor.getURI()
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()
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -422,6 +456,7 @@ class IdrisController
.catch (e) => @model.printDefinition word
.subscribe successHandler, @displayErrors

# open the repl window
openREPL: ({ target }) =>
uri = @getEditor().getURI()

Expand All @@ -437,6 +472,7 @@ class IdrisController
.filter ({ responseType }) -> responseType == 'return'
.subscribe successHandler, @displayErrors

# open the apropos window
apropos: ({ target }) =>
uri = @getEditor().getURI()

Expand All @@ -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 '<i class="icon-bug"></i> 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: "<pre>" + err.message + "</pre>"
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: "<pre>" + info + "</pre>"
className: "preview"

editor = atom.workspace.getActiveTextEditor()
if line > 0 && uri == editor.getURI()
startPoint = warning[1]
Expand Down
2 changes: 1 addition & 1 deletion package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down

0 comments on commit f95e49f

Please sign in to comment.