Merge pull request #80 from idris-hackers/repl-experiments

Add a repl that opens in an atom tab

CHANGELOG.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- Added a REPL [#80](https://github.com/idris-hackers/atom-language-idris/pull/80)
+- Added a panel for the `apropos` command
+
 ### Fixed
 
 ## v0.3.4

keymaps/language-idris.json

@@ -5,6 +5,7 @@
     "ctrl-alt-a": "language-idris:add-clause",
     "ctrl-alt-s": "language-idris:proof-search",
     "ctrl-alt-d": "language-idris:docs-for",
+    "ctrl-alt-enter": "language-idris:open-repl",
     "ctrl-alt-w": "language-idris:make-with",
     "ctrl-alt-l": "language-idris:make-lemma",
     "ctrl-alt-r": "language-idris:typecheck",

lib/idris-controller.coffee

@@ -23,6 +23,8 @@ class IdrisController
     'language-idris:typecheck': @runCommand @typecheckFile
     'language-idris:print-definition': @runCommand @printDefinition
     'language-idris:stop-compiler': @stopCompiler
+    'language-idris:open-repl': @runCommand @openREPL
+    'language-idris:apropos': @runCommand @apropos
 
   isIdrisFile: (uri) ->
     uri?.match? /\.idr$/
@@ -337,6 +339,38 @@ class IdrisController
       .printDefinition word
       .subscribe successHandler, @displayErrors
 
+  openREPL: ({ target }) =>
+    editor = target.model
+    uri = editor.getURI()
+
+    successHandler = ({ responseType, msg }) ->
+      options =
+        split: 'right'
+        searchAllPanes: true
+
+      atom.workspace.open "idris://repl", options
+
+    @model
+      .load uri
+      .filter ({ responseType }) -> responseType == 'return'
+      .subscribe successHandler, @displayErrors
+
+  apropos: ({ target }) =>
+    editor = target.model
+    uri = editor.getURI()
+
+    successHandler = ({ responseType, msg }) ->
+      options =
+        split: 'right'
+        searchAllPanes: true
+
+      atom.workspace.open "idris://apropos", options
+
+    @model
+      .load uri
+      .filter ({ responseType }) -> responseType == 'return'
+      .subscribe successHandler, @displayErrors
+
   displayErrors: (err) =>
     @messages.show()
     @messages.clear()

lib/idris-model.coffee

@@ -48,6 +48,7 @@ class IdrisModel
               subject.onError
                 message: ret[1]
                 warnings: @warnings[id]
+                highlightInformation: ret[2]
             subject.onCompleted()
             delete @subjects[id]
           when ':write-string'
@@ -127,4 +128,7 @@ class IdrisModel
   printDefinition: (name) ->
     @prepareCommand [':print-definition', name]
 
+  apropos: (name) ->
+    @prepareCommand [':apropos', name]
+
 module.exports = IdrisModel

lib/language-idris.coffee

@@ -1,5 +1,7 @@
 IdrisController = require './idris-controller'
 { CompositeDisposable } = require 'atom'
+url = require 'url'
+{ IdrisPanel } = require './views/panel-view'
 
 module.exports =
   config:
@@ -28,6 +30,16 @@ module.exports =
     @subscriptions = new CompositeDisposable
     @subscriptions.add subscription
 
+    atom.workspace.addOpener (uriToOpen, options) =>
+      try
+        { protocol, host, pathname } = url.parse uriToOpen
+      catch error
+        return
+
+      return unless protocol is 'idris:'
+
+      new IdrisPanel @controller, host
+
   deactivate: ->
     @subscriptions.dispose()
     this.controller.destroy()

lib/utils/dom.coffee

@@ -16,6 +16,28 @@ createCodeElement = ->
     pre.style.webkitFontFeatureSettings = '"liga"'
   pre
 
+fontOptions = ->
+  fontSize = atom.config.get 'language-idris.panelFontSize'
+  fontSizeAttr = "#{fontSize}px"
+  enableLigatures = atom.config.get 'language-idris.panelFontLigatures'
+  webkitFontFeatureSettings =
+    if enableLigatures
+      '"liga"'
+    else
+      '"inherit"'
+
+  fontFamily = atom.config.get 'language-idris.panelFontFamily'
+  if fontFamily != ''
+    fontFamily
+  else
+    '"inherit"'
+
+  'font-size': fontSizeAttr
+  '-webkit-font-feature-settings': webkitFontFeatureSettings
+  'font-family': fontFamily
+
+
 module.exports =
   joinHtmlElements: joinHtmlElements
   createCodeElement: createCodeElement
+  fontOptions: fontOptions

lib/utils/highlighter.coffee

@@ -1,6 +1,8 @@
 # Applies the highlighting we get from the idris compiler to our source code.
 # http://docs.idris-lang.org/en/latest/reference/ide-protocol.html#output-highlighting
 
+CycleDOM = require '@cycle/dom'
+
 highlightInfoListToOb = (list) ->
   obj = { }
   for x in list
@@ -21,8 +23,18 @@ decorToClasses = (decor) ->
     else []
 
 highlightWord = (word, info) ->
+  type = info.info.type || ""
+  doc = info.info['doc-overview'] || ""
+
+  description =
+    if info.info.type?
+      "#{type}\n\n#{doc}".trim()
+    else
+      ""
+
   classes: decorToClasses(info.info.decor).concat 'idris'
   word: word
+  description: description
 
 # Build highlighting information that we can then pass to one
 # of our serializers.
@@ -80,8 +92,15 @@ highlightToHtml = (highlights) ->
     container.appendChild span
   container
 
+highlightToCycle = (highlights) ->
+  highlights.map ({ classes, word, description }) ->
+    if classes.length == 0
+      word
+    else
+      CycleDOM.h 'span', { className: classes.join(' '), title: description }, word
 
 module.exports =
   highlight: highlight
   highlightToString: highlightToString
   highlightToHtml: highlightToHtml
+  highlightToCycle: highlightToCycle

lib/utils/sexp-formatter.coffee

@@ -27,7 +27,7 @@ formatSexp = (sexp) ->
   else if isSymbol sexp
     sexp
   else if isString sexp
-    '"' + sexp + '"'
+    '"' + sexp.trim() + '"'
   else if isBoolean sexp
     if sexp
       ':True'

lib/views/apropos-view.coffee

@@ -0,0 +1,80 @@
+Cycle = require '@cycle/core'
+CycleDOM = require '@cycle/dom'
+highlighter = require '../utils/highlighter'
+Rx = require 'rx-lite'
+{ fontOptions } = require '../utils/dom'
+
+styles = fontOptions()
+
+AproposCycle =
+  # highlight : forall a.
+  #   { code : String, highlightInformation : HighlightInformation } ->
+  #   CycleDOM
+  highlight: ({ code, highlightInformation }) ->
+    highlights = highlighter.highlight code, highlightInformation
+    highlighter.highlightToCycle highlights
+
+  # view : Observable State -> Observable CycleDOM
+  view: (state$) ->
+    state$.map (apropos) ->
+      aproposAnswer =
+        if apropos.code
+          highlightedCode = AproposCycle.highlight apropos
+          CycleDOM.h 'pre', { className: 'idris-apropos-output', style: styles }, highlightedCode
+        else
+          CycleDOM.h 'span', ''
+
+      CycleDOM.h 'div',
+        {
+          className: 'idris-panel-view'
+        },
+        [
+          CycleDOM.h 'input', { type: 'text', className: 'native-key-bindings idris-repl-input-field' }, ''
+          CycleDOM.h 'div', aproposAnswer
+        ]
+
+  main: (responses) ->
+    input = responses.DOM.select('input').events('keydown')
+      .filter (ev) -> ev.keyCode == 13
+      .map (ev) -> ev.target.value
+      .startWith ''
+
+    DOM: AproposCycle.view responses.CONTENT
+    CONTENT: input
+
+  # driver : forall a.
+  #   IdrisModel -> Observable String ->
+  #   Observable (List { a | code : String, highlightInformation : highlightInformation })
+  driver:
+    (options) ->
+      DOM: CycleDOM.makeDOMDriver options.hostElement
+      CONTENT: (inp) ->
+        inp
+          .filter (line) -> line != ''
+          .flatMap (line) ->
+            escapedLine = line.replace(/"/g, '\\"')
+            options.model.apropos escapedLine
+            .map (e) ->
+              code: e.msg[0]
+              highlightInformation: e.msg[1]
+            .catch (e) ->
+              Rx.Observable.just
+                code: e.message
+                highlightInformation: e.highlightInformation
+          .startWith { }
+
+class AproposView
+  constructor: (params) ->
+    hostElement = document.createElement 'div'
+    @[0] = hostElement
+
+    model = params.controller.model
+
+    drivers =
+      AproposCycle.driver
+        hostElement: hostElement
+        model: model
+
+    Cycle.run AproposCycle.main, drivers
+
+module.exports = AproposView

lib/views/panel-view.coffee

@@ -0,0 +1,24 @@
+REPLView = require './repl-view'
+AproposView = require './apropos-view'
+
+class IdrisPanel
+  constructor: (@controller, @panel) ->
+
+  getTitle: ->
+    switch @panel
+      when "repl" then "Idris: REPL"
+      when "apropos" then "Idris: Apropos"
+      else "Idris ?"
+
+  getViewClass: ->
+    switch @panel
+      when "repl" then REPLView
+      when "apropos" then AproposView
+
+  getURI: ->
+    switch @panel
+      when "repl" then "idris://repl"
+      when "apropos" then "idris://apropos"
+
+module.exports =
+  IdrisPanel: IdrisPanel