From 8798d70ab29b056c8f688ab2468cec695d729db2 Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Fri, 12 Jun 2015 15:27:41 +0200 Subject: [PATCH] Initial support semantic highlights Semantic source highlighting information from Idris is no longer ignored. Atom highlights are not wrapped around the text. Instead, they live at a different z-index, which means they can't apply text highlights. This is why the selection doesn't touch text colors. Thus, the semantic highlights are applied to the background only. Because they are ugly, they are currently disabled by default in the settings. But it's a start that can be built upon. --- lib/idris-controller.coffee | 34 +++++++++++++++++++++++---- lib/idris-model.coffee | 15 +++++++++--- lib/language-idris.coffee | 3 +++ lib/utils/sourceHighlight.coffee | 36 +++++++++++++++++++++++++++++ package.json | 4 ++++ styles/idris.atom-text-editor.less | 25 ++++++++++++++++++++ styles/idris.atom-text-editor.less~ | 3 +++ 7 files changed, 112 insertions(+), 8 deletions(-) create mode 100644 lib/utils/sourceHighlight.coffee create mode 100644 styles/idris.atom-text-editor.less create mode 100644 styles/idris.atom-text-editor.less~ 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; +}