diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index b7348b1..3247a67 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -3,13 +3,16 @@ PlainMessageView = require('atom-message-panel').PlainMessageView LineMessageView = require('atom-message-panel').LineMessageView ProofObligationView = require('./proof-obligation-view') MetavariablesView = require './metavariables-view' +SourceHighlightHelp = require('./utils/sourceHighlight.coffee') class IdrisController idrisBuffers: 0 localChanges: undefined + constructor: (@statusbar, @model) -> @idrisBuffers = 0 + @semanticMarkers = [] atom.workspace.getTextEditors().forEach (editor) => uri = editor.getURI() @@ -58,14 +61,14 @@ class IdrisController @messages.hide() @localChanges = false if @isIdrisFile(editor.getURI()) - @loadFile editor.getURI() + @loadFile editor idrisFileChanged: (editor) -> @localChanges = editor.isModified() if @localChanges @statusbar.setStatus 'Idris: local modifications' else if @isIdrisFile(editor.getURI()) - @loadFile editor.getURI() + @loadFile editor idrisFileClosed: (editor) -> @idrisBuffers -= 1 @@ -81,7 +84,7 @@ class IdrisController uri = editor.getPath() if @isIdrisFile(uri) @statusbar.show() - @loadFile uri + @loadFile editor else @statusbar.hide() @@ -96,10 +99,18 @@ class IdrisController cursorPosition = editor.getLastCursor().getCurrentWordBufferRange() editor.getTextInBufferRange cursorPosition - loadFile: (uri) -> + loadFile: (editor) -> + console.log editor + uri = editor.getURI() console.log 'Loading ' + uri @messages.clear() - @model.load uri, (err, message, progress) => + + console.log @semanticMarkers + for marker in @semanticMarkers + marker.destroy() + @semanticMarkers = [] + + callback = (err, message, progress) => if err @statusbar.setStatus 'Idris: ' + err.message @messages.show() @@ -115,6 +126,19 @@ class IdrisController @statusbar.setStatus 'Idris: ' + progress else @statusbar.setStatus 'Idris: ' + JSON.stringify(message) + @model.load uri, callback, (highlightMsg) => + if atom.config.get('language-idris.semanticHighlighting') && highlightMsg && highlightMsg[0] == ":highlight-source" + for [where, what] in highlightMsg[1] + {file, start, end} = SourceHighlightHelp.fileLocation(where) + semanticClass = SourceHighlightHelp.decoClass(what) + if file == editor.getPath() + marker = editor.markBufferRange([start, end], + invalidate: 'never') + decoration = editor.decorateMarker(marker, + type: "highlight", + class: semanticClass) + @semanticMarkers.push(marker) + getDocsForWord: ({target}) => word = @getWordUnderCursor target diff --git a/lib/idris-model.coffee b/lib/idris-model.coffee index 608547a..36c85c5 100644 --- a/lib/idris-model.coffee +++ b/lib/idris-model.coffee @@ -10,6 +10,7 @@ class IdrisModel extends EventEmitter @buffer = '' @process = undefined @callbacks = {} + @outputCallbacks = {} @warnings = {} super this @@ -77,12 +78,18 @@ class IdrisModel extends EventEmitter message: ret[1] warnings: @warnings[id] delete @callbacks[id] + #delete @outputCallbacks[id] delete @warnings[id] when ':write-string' id = params[params.length - 1] msg = params[0] if @callbacks[id] @callbacks[id] undefined, undefined, msg + when ':output' + id = params[params.length - 1] + msg = params[0] + if @outputCallbacks[id] && msg[0] == ':ok' + @outputCallbacks[id] msg[1] when ':warning' id = params[params.length - 1] warning = params[0] @@ -105,14 +112,16 @@ class IdrisModel extends EventEmitter Logger.logOutgoingCommand cmd @process.stdin.write sexpFormatter.serialize(cmd) - prepareCommand: (cmd, callback) -> + prepareCommand: (cmd, callback, outputCallback = null) -> id = @getUID() @callbacks[id] = callback + if outputCallback + @outputCallbacks[id] = outputCallback @warnings[id] = [] @sendCommand [cmd, id] - load: (uri, callback) -> - @prepareCommand [':load-file', uri], callback + load: (uri, callback, outputCallback) -> + @prepareCommand [':load-file', uri], callback, outputCallback docsFor: (word, callback) -> @prepareCommand [':docs-for', word], callback diff --git a/lib/language-idris.coffee b/lib/language-idris.coffee index e0be3ab..0b26a68 100644 --- a/lib/language-idris.coffee +++ b/lib/language-idris.coffee @@ -10,6 +10,9 @@ module.exports = pathToIdris: type: 'string' default: 'idris' + semanticHighlighting: + type: 'boolean' + default: false activate: -> pathToIdris = atom.config.get "language-idris.pathToIdris" diff --git a/lib/utils/sourceHighlight.coffee b/lib/utils/sourceHighlight.coffee new file mode 100644 index 0000000..dd07e89 --- /dev/null +++ b/lib/utils/sourceHighlight.coffee @@ -0,0 +1,36 @@ +fileLocation = (where) -> + [[tag1, file], [tag2, startLine, startCol], [tag3, endLine, endCol]] = where + if tag1 == ':filename' && tag2 == ':start' && tag3 == ':end' + {file: file, start: [startLine - 1, startCol - 1], end: [endLine - 1 , endCol - 1]} + else + throw ("bad location " + where) + +assoc = (key, list) -> + try + [car, cdr...] = list + [k, vs...] = car + if k == key + vs + else + assoc key, cdr + catch e + null + + +decoClass = (props) -> + decor = assoc ':decor', props + console.log decor + decoClass = + switch decor[0] + when ':function' then ' function' + when ':bound' then ' bound' + when ':data' then ' data' + when ':metavar' then ' metavar' + when ':type' then ' type' + else '' + console.log decoClass + 'idris-thing' + decoClass + +module.exports = + fileLocation: fileLocation + decoClass: decoClass diff --git a/package.json b/package.json index bb6c1db..ee7216b 100644 --- a/package.json +++ b/package.json @@ -21,6 +21,10 @@ { "name": "Heather", "url": "https://github.com/Heather" + }, + { + "name": "David Christiansen", + "url": "http://www.davidchristiansen.dk" } ], "consumedServices": { diff --git a/styles/idris.atom-text-editor.less b/styles/idris.atom-text-editor.less new file mode 100644 index 0000000..1914585 --- /dev/null +++ b/styles/idris.atom-text-editor.less @@ -0,0 +1,25 @@ +.editor .idris-thing .region { + +} + +.editor .idris-thing.type .region { + background-color: #EBFAFF; +} + +.editor .idris-thing.function .region { + background-color: #B2F0B2; +} + +.editor .idris-thing.bound .region { + background-color: #D9B2D9; +} +.editor .idris-thing.metavar .region { + border: 1px solid gray !important; +} + +.editor .idris-thing.data .region { + background-color: #FF9999; +} + +.editor .idris-thing.module .region { +} diff --git a/styles/idris.atom-text-editor.less~ b/styles/idris.atom-text-editor.less~ new file mode 100644 index 0000000..0072292 --- /dev/null +++ b/styles/idris.atom-text-editor.less~ @@ -0,0 +1,3 @@ +.HERE .region { + color: red; +}