Skip to content

Commit

Permalink
Merge pull request #2066 from jfdm/doc/sphinx-version-fixes
Browse files Browse the repository at this point in the history
Sphinx 1.2 series compatibility fixes.
  • Loading branch information
jfdm committed Mar 27, 2015
2 parents 1dec451 + df9c178 commit d0b8bb5
Show file tree
Hide file tree
Showing 7 changed files with 21 additions and 13 deletions.
8 changes: 7 additions & 1 deletion docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,13 @@ To build the manual the following dependencies must be met. We assume that you h
### Sphinx-Doc

Python should be installed by default on most systems.
Sphinx can be installed wither through your hosts package manager or using pip/easy_install.
Sphinx can be installed either through your hosts package manager or using pip/easy_install.

*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
`v1.2.2`. If you install a more recent version of sphinx then
'incorrectly' marked up documentation may get passed the build system
of readthedocs and be ignored. In the past we had several code-blocks
disappear because of that.

### LaTeX

Expand Down
3 changes: 1 addition & 2 deletions docs/effects/simpleeff.rst
Original file line number Diff line number Diff line change
Expand Up @@ -274,8 +274,7 @@ correct:
guess : Int -> { [STDIO] } Eff ()
For reference, the code for ``guess`` is given in Listing
:ref:`eff-game`.
For reference, the code for ``guess`` is given below:

.. _eff-game:
.. code-block:: idris
Expand Down
2 changes: 1 addition & 1 deletion docs/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ Learning Effects
effects/conclusions
effects/summary

.. _proofs::
.. _proofs:

###############
Theorem Proving
Expand Down
3 changes: 2 additions & 1 deletion docs/tutorial/interp.rst
Original file line number Diff line number Diff line change
Expand Up @@ -266,8 +266,9 @@ integer, giving 0 if the input is invalid. An example run of this
program at the Idris interactive environment is:


.. _factrun:
.. literalinclude:: ../listing/idris-prompt-interp.txt
:name: factrun


Aside: ``cast``
~~~~~~~~~~~~~~~
Expand Down
6 changes: 4 additions & 2 deletions docs/tutorial/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ module, a list of ``import`` statements giving the other modules which
are to be imported, and a collection of declarations and definitions of
types, classes and functions. For example, the listing below gives a
module which defines a binary tree type ``BTree`` (in a file
``btree.idr``):;
``btree.idr``):

.. code-block:: idris
Expand All @@ -32,8 +32,9 @@ module which defines a binary tree type ``BTree`` (in a file
toTree [] = Leaf
toTree (x :: xs) = insert x (toTree xs)
Then, this gives a main program (in a file
``bmain.idr``) which uses the ``bst`` module to sort a list::
``bmain.idr``) which uses the ``bst`` module to sort a list:

.. code-block:: idris
Expand All @@ -45,6 +46,7 @@ Then, this gives a main program (in a file
main = do let t = toTree [1,8,2,7,9,3]
print (btree.toList t)
The same names can be defined in multiple modules. This is possible
because in practice names are *qualified* with the name of the module.
The names defined in the ``btree`` module are, in full:
Expand Down
2 changes: 1 addition & 1 deletion docs/tutorial/starting.rst
Original file line number Diff line number Diff line change
Expand Up @@ -86,5 +86,5 @@ checking a file, if successful, creates a bytecode version of the file
(in this case ``hello.ibc``) to speed up loading in future. The
bytecode is regenerated if the source file changes.

.. _run1:
.. literalinclude:: ../listing/idris-prompt-helloworld.txt
:name: run1
10 changes: 5 additions & 5 deletions docs/tutorial/typesfuns.rst
Original file line number Diff line number Diff line change
Expand Up @@ -221,8 +221,8 @@ declaration for a function ``f`` *can* be omitted if:

- ``f`` appears in the right hand side of the top level definition

- The type of ``f`` can be completely determined from its first
application
- The type of ``f`` can be completely determined from its first application


So, for example, the following definitions are legal:

Expand Down Expand Up @@ -948,10 +948,10 @@ analysis of intermediate expressions to avoid the need to write
auxiliary functions, and is also used internally to implement pattern
matching ``let`` and lambda bindings. It will *only* work if:

- Each branch *matches* a value of the same type, and *returns* a value
of the same type.
- Each branch *matches* a value of the same type, and *returns* a
value of the same type.

- The type of the result is known. i.e. the type of the expression
- The type of the result is "known". i.e. the type of the expression
can be determined *without* type checking the ``case``-expression
itself.

Expand Down

0 comments on commit d0b8bb5

Please sign in to comment.