Fixed syntax for commands and some words

docs/reference/repl.rst

@@ -45,7 +45,7 @@ repl/init in Idris's application data directory. The application data
 directory is the result of the Haskell function call
 ``getAppUserDataDirectory "idris"``, which on most Unix-like systems
 will return $HOME/.idris and on various versions of Windows will return
-paths such as "C:/Documents And Settings/user/Application Data/appName".
+paths such as ``C:/Documents And Settings/user/Application Data/appName``.
 
 The file repl/init is a newline-separate list of REPL commands. Not all
 commands are supported in initialisation scripts — only the subset that

docs/reference/semantic-highlighting.rst

@@ -41,7 +41,7 @@ Idris also supports the pretty printing of code to HTML and LaTeX using the comm
 Customisation
 =============
 
-If you are not happy with the colours used. The VIM and Emacs editor support allows for customisation of the colours used. When pretty printing Idris code as LaTeX and HTML, commands and a CSS style are provided. As of writing support for customising the console colours is not knowingly supported.
+If you are not happy with the colours used. The VIM and Emacs editor support allows for customisation of the colours used. When pretty printing Idris code as LaTeX and HTML, commands and a CSS style are provided. The colours used by the REPL can be customised through the initialisation script.
 
 
 Further Information

docs/reference/syntax-guide.rst

@@ -1,5 +1,3 @@
-.. _sect-repl:
-
 **************
 Syntax Guide
 **************

docs/reference/tactics.rst

@@ -2,31 +2,35 @@
 Tactics and Theorem Proving
 ***************************
 
-To list all unproven metavariables, use the command ``:m``. This will
-display their qualified names and the expected types. To interactively
-prove a metavariable, use the command ``:p name`` where ``name`` is the
-metavariable. Once the proof is complete, the command ``:a`` will append
-it to the current module.
+Idris supports interactive theorem proving, and theh analyse of
+context through metavariables.  To list all unproven metavariables,
+use the command ``:m``. This will display their qualified names and
+the expected types. To interactively prove a metavariable, use the
+command ``:p name`` where ``name`` is the metavariable. Once the proof
+is complete, the command ``:a`` will append it to the current module.
 
 Once in the interactive prover, the following commands are available:
 
 Basic commands
 ==============
 
--  **:q** - Quits the prover (gives up on proving current lemma).
--  **abandon** - Same as :q
--  **state** - Displays the current state of the proof.
--  **term** - Displays the current proof term complete with its
+-  ``:q`` - Quits the prover (gives up on proving current lemma).
+-  ``abandon`` - Same as :q
+-  ``state`` - Displays the current state of the proof.
+-  ``term`` - Displays the current proof term complete with its
    yet-to-be-filled holes (is only really useful for debugging).
--  **undo** - Undoes the last tactic.
--  **qed** - Once the interactive theorem prover tells you "No more
+-  ``undo`` - Undoes the last tactic.
+-  ``qed`` - Once the interactive theorem prover tells you "No more
    goals," you get to type this in celebration! (Completes the proof and
    exits the prover)
 
-Most common tactics
-===================
+Commonly Used Tactics
+=====================
 
--  **compute** - Normalizes all terms in the goal (note: does not
+Compute
+-------
+
+-  ``compute`` - Normalizes all terms in the goal (note: does not
    normalize assumptions)
 
 ::
@@ -38,7 +42,10 @@ Most common tactics
      (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
     -lemma>
 
--  **exact** - Provide a term of the goal type directly.
+Exact
+-----
+
+-  ``exact`` - Provide a term of the goal type directly.
 
 ::
 
@@ -48,10 +55,16 @@ Most common tactics
     lemma: No more goals.
     -lemma>
 
--  **refine** - Use a name to refine the goal. If the name needs
+Refine
+------
+
+-  ``refine`` - Use a name to refine the goal. If the name needs
    arguments, introduce them as new goals.
 
--  **trivial** - Satisfies the goal using an assumption that matches its
+Trivial
+-------
+
+-  ``trivial`` - Satisfies the goal using an assumption that matches its
    type.
 
 ::
@@ -64,7 +77,10 @@ Most common tactics
     lemma: No more goals.
     -lemma>
 
--  **intro** - If your goal is an arrow, turns the left term into an
+Intro
+-----
+
+-  ``intro`` - If your goal is an arrow, turns the left term into an
    assumption.
 
 ::
@@ -90,7 +106,11 @@ You can also supply your own name for the assumption:
     ----------                 Goal:                  ----------
     Nat -> Nat
 
--  **intros** - Exactly like intro, but it operates on all left terms at
+
+Intros
+------
+
+-  ``intros`` - Exactly like intro, but it operates on all left terms at
    once.
 
 ::
@@ -105,7 +125,10 @@ You can also supply your own name for the assumption:
      Nat
     -lemma>
 
--  **let** - Introduces a new assumption; you may use current
+let
+---
+
+-  ``let`` - Introduces a new assumption; you may use current
    assumptions to define the new one.
 
 ::
@@ -122,7 +145,10 @@ You can also supply your own name for the assumption:
      BigInt
     -lemma>
 
--  **rewrite** - Takes an expression with an equality type (x = y), and
+rewrite
+-------
+
+-  ``rewrite`` - Takes an expression with an equality type (x = y), and
    replaces all instances of x in the goal with y. Is often useful in
    combination with 'sym'.
 
@@ -143,7 +169,10 @@ You can also supply your own name for the assumption:
      Vect Z a
     -lemma>
 
--  **induction** - (**Note that this is still experimental** and you may
+induction
+---------
+
+-  ``induction`` - (``Note that this is still experimental`` and you may
    get strange results and error messages. We are aware of these and
    will finish the implementation eventually!) Prove the goal by
    induction. Each constructor of the datatype becomes a goal.
@@ -153,7 +182,10 @@ You can also supply your own name for the assumption:
    ``%elim`` modifier.
 
 
--  **sourceLocation** - Solve the current goal with information about
+sourceLocation
+--------------
+
+-  ``sourceLocation`` - Solve the current goal with information about
    the location in the source code where the tactic was invoked. This is
    mostly for embedded DSLs and programmer tools like assertions that
    need to know where they are called. See
@@ -162,20 +194,20 @@ You can also supply your own name for the assumption:
 Less commonly-used tactics
 ==========================
 
--  **applyTactic** - Apply a user-defined tactic. This should be a
+-  ``applyTactic`` - Apply a user-defined tactic. This should be a
    function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
    the first argument represents the proof context and the second
    represents the goal. If your tactic will produce a proof term
    directly, use the ``Exact`` constructor from ``Tactic``.
--  **attack** - ?
--  **equiv** - Replaces the goal with a new one that is convertible with
+-  ``attack`` - ?
+-  ``equiv`` - Replaces the goal with a new one that is convertible with
    the old one
--  **fill** - ?
--  **focus** - ?
--  **mrefine** - Refining by matching against a type
--  **reflect** - ?
--  **solve** - Takes a guess with the correct type and fills a hole with
+-  ``fill`` - ?
+-  ``focus`` - ?
+-  ``mrefine`` - Refining by matching against a type
+-  ``reflect`` - ?
+-  ``solve`` - Takes a guess with the correct type and fills a hole with
    it, closing a proof obligation. This happens automatically in the
    interactive prover, so ``solve`` is really only relevant in tactic
    scripts used for helping implicit argument resolution.
--  **try** - ?
+-  ``try`` - ?