Merge branch 'master' into issue-51

CHANGELOG.md

@@ -5,9 +5,12 @@
 ### Added
 
 - Restart the idris compiler after every commmand if it was killed [#54](https://github.com/idris-hackers/atom-language-idris/pull/54)
+- added the ability to style all the idris-panels
 
 ### Fixed
 
+- Status message should appear only in idris projects [#52](https://github.com/idris-hackers/atom-language-idris/issues/52) many thanks to @jeremy-w
+
 ## v0.2.4
 
 ### Added

documentation/tutorial.md

@@ -4,8 +4,7 @@
 
 ## Learning Idris
 
-This is an overview over the atom package for Idris.
-If you are interested in learning Idris you can find the official documentation here http://docs.idris-lang.org/en/latest/ and the official Idris tutorial here http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf.
+This is an overview of the atom package for Idris. If you are interested in learning Idris you can find the [official documentation](http://docs.idris-lang.org/en/latest/), and the [official Idris tutorial](http://docs.idris-lang.org/en/latest/tutorial/).
 
 ### Installation
 
@@ -32,12 +31,11 @@ mul (S k) y = add y (mul k y)
 
 ### Typecheck
 
-Open the command palette (`ctrl-shift-p` on Win/Linux) and select `Language Idris: Typecheck`.
+Open the command palette (`ctrl-shift-p` on Win/Linux) and select `Language Idris: Typecheck`. (or use `ctrl-alt-r`)
 
 ### Type info
 
-Select an instance of the `add` function in your code and press `ctrl-alt-t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of".
-A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`.
+Select an instance of the `add` function in your code and press `ctrl-alt-t` or use the command palette (`ctrl-shift-p` on Win/Linux) and search for "Language Idris: Type Of". A panel should open at the bottom of your window showing you the type of the `add` function, `Ops.add : Nat -> Nat -> Nat`.
 Now try the same thing with the `mul` function.
 
 ### Show documentation
@@ -59,7 +57,7 @@ module Main
 plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r
 ```
 
-Load the file into idris by typecheckiing it by pressing  `ctrl-shift-p` and typing "Language Idris: Typecheck" into the command palette then press `ctrl-shift-p` again and type "Language Idris: Holes".
+Load the file into Idris by typechecking it by pressing `ctrl-alt-r`. Then press `ctrl-shift-p` and type "Language Idris: Holes".
 
 At the bottom of your window should open a small panel with all holes you'll have to prove.
 Here it should just show:
@@ -74,7 +72,7 @@ Main.plusAssoc : plus l (plus c r) = plus (plus l c) r
 where `l : Nat, c : Nat, r : Nat` are variables you can use to prove
 `Main.plusAssoc : plus l (plus c r) = plus (plus l c) r`.
 
-If you put your cursor over `plusAssoc` in the `proving.idr` file and execute the command "Language Idris: Add Clause" a line wil be inserted by atom at the bottom of your file.
+If you put your cursor over `plusAssoc` in the `proving.idr` file and execute the command "Language Idris: Add Clause" (`ctrl-alt-a`) a line wil be inserted by atom at the bottom of your file.
 
 Your file should now look like this:
 ```idris
@@ -125,7 +123,7 @@ plusAssoc Z c r = Refl
 plusAssoc (S l) c r = ?plusAssoc_rhs_2
 ```
 
-Only ne hole is left now:
+Only one hole is left now:
 
 ```
 Main.plusAssoc_rhs_2
@@ -145,7 +143,7 @@ plusAssoc (S l) c r = ?plusAssoc_rhs_2
 with
 
 ```idris
-plusAssoc (S l) c r = ?plusAssoc_rhs_2
+plusAssoc (S l) c r = rewrite plusAssoc l c r in ?plusAssoc_rhs_2
 ```
 
 and after type checking the holes view now shows us:
@@ -160,7 +158,7 @@ Main.plusAssoc_rhs_2
 Main.plusAssoc_rhs_2 : S (plus (plus l c) r) = S (plus (plus l c) r)
 ```
 
-Now you need to prove that `S (plus (plus l c) r) = S (plus (plus l c) r)` and Idrs can again do this for us.
+Now you need to prove that `S (plus (plus l c) r) = S (plus (plus l c) r)` and Idris can again do this for us.
 
 And you end with the file
 
@@ -174,5 +172,5 @@ plusAssoc (S l) c r = rewrite plusAssoc l c r in Refl
 
 and a proof that the addition of natural numbers is associative.
 
-This tutorial is a written version of [David Christiansens](https://twitter.com/d_christiansen) emacs video for Atom.
+This tutorial is a written version of [David Christiansen's](https://twitter.com/d_christiansen) emacs video for Atom.
 https://www.youtube.com/watch?v=0eOY1NxbZHo&list=PLiHLLF-foEexGJu1a0WH_llkQ2gOKqipg

lib/idris-controller.coffee

@@ -85,7 +85,7 @@ class IdrisController
       [type, highlightingInfo] = msg
       @messages.show()
       @messages.clear()
-      @messages.setTitle 'Idris: Type of <tt>' + word + '</tt>', true
+      @messages.setTitle 'Idris: Docs for <tt>' + word + '</tt>', true
       informationView = new InformationView
       informationView.initialize
         obligation: type
@@ -340,10 +340,15 @@ class IdrisController
         message: warning[3]
 
   attachStatusIndicator: (statusBar) ->
-    @statusIndicator = new StatusIndicator
-    @statusIndicator.initialize()
-    statusBar.addLeftTile
-      item: @statusIndicator
+    if not @statusIndicator
+      @statusIndicator = new StatusIndicator
+      @statusIndicator.initialize()
+      statusBar.addLeftTile
+        item: @statusIndicator
+
+  detachStatusIndicator: ->
+    @statusIndicator?.remove()
+    @statusIndicator = null
 
 
 module.exports = IdrisController

lib/language-idris.coffee

@@ -7,6 +7,18 @@ module.exports =
       type: 'string'
       default: 'idris'
       description: 'Path to the idris executable'
+    panelFontFamily:
+      type: 'string'
+      default: ''
+      description: 'The font family to use in the various idris panels'
+    panelFontSize:
+      type: 'number'
+      default: 13
+      description: 'The font size to use in the various idris panels'
+    panelFontLigatures:
+      type: 'boolean'
+      default: false
+      description: 'Enable ligatures in the various idris panels'
 
   activate: ->
     @controller = new IdrisController
@@ -20,4 +32,11 @@ module.exports =
     this.controller.destroy()
 
   consumeStatusBar: (statusBar) ->
-    @controller.attachStatusIndicator statusBar
+    subscription = atom.workspace.observeActivePaneItem (paneItem) =>
+      if paneItem && paneItem.getGrammar?
+        grammar = paneItem.getGrammar().name
+        if grammar == 'Idris'
+          @controller?.attachStatusIndicator statusBar
+        else
+          @controller?.detachStatusIndicator statusBar
+    @subscriptions?.add? subscription

lib/utils/dom.coffee

@@ -4,5 +4,18 @@ joinHtmlElements = (containerElem, elems) ->
     div.appendChild elem
   div
 
+createCodeElement = ->
+  pre = document.createElement 'pre'
+  fontFamily = atom.config.get 'language-idris.panelFontFamily'
+  if fontFamily != ''
+    pre.style.fontFamily = fontFamily
+  fontSize = atom.config.get 'language-idris.panelFontSize'
+  pre.style.fontSize = "#{fontSize}px"
+  enableLigatures = atom.config.get 'language-idris.panelFontLigatures'
+  if enableLigatures
+    pre.style.webkitFontFeatureSettings = '"liga"'
+  pre
+
 module.exports =
   joinHtmlElements: joinHtmlElements
+  createCodeElement: createCodeElement

lib/views/holes-view.coffee

@@ -6,7 +6,8 @@ textNode = (text) ->
 
 class HolesView extends HTMLElement
   initialize: (holes) ->
-    @holesContainer = document.createElement 'pre'
+    @classList.add 'idris-panel'
+    @holesContainer = dom.createCodeElement()
     @holesContainer.classList.add 'idris-mode'
     @holesContainer.classList.add 'block'
     @holesContainer.classList.add 'idris-holes-view'

lib/views/information-view.coffee

@@ -1,20 +1,20 @@
 highlighter = require '../utils/highlighter'
+dom = require '../utils/dom'
 
 class InformationView extends HTMLElement
   initialize: (params) ->
+    @classList.add 'idris-panel'
     @obligation = params.obligation
     @highlightingInfo = params.highlightingInfo
     if @highlightingInfo?
       highlighting = highlighter.highlight @obligation, @highlightingInfo
       info = highlighter.highlightToHtml highlighting
-      pre = document.createElement 'pre'
+      pre = dom.createCodeElement()
       pre.appendChild info
       @appendChild pre
     else
       @text @obligation
 
-  @content: ->
-    @pre class: 'idris-mode block'
-
 module.exports = InformationView =
-  document.registerElement('idris-informations-view', {prototype: InformationView.prototype})
+  document.registerElement 'idris-informations-view',
+    prototype: InformationView.prototype

styles/idris-panel.less

@@ -0,0 +1,7 @@
+.idris-panel
+{
+  pre
+  {
+    font-size: 13px;
+  }
+}