Merge pull request #126 from jfdm/add-warnings-to-rtd

Improve messages in Idris2 Sphinx Docs about documentation completness so they are more visible.

.gitignore

@@ -1,3 +1,4 @@
+idris2docs_venv
 *~
 *.ibc
 *.ttc

docs/source/reference/envvars.rst

@@ -4,4 +4,6 @@
 Environment Variables
 *********************
 
-[TODO: Fill in the environment variables recognised by Idris 2]
+.. todo::
+
+   Fill in the environment variables recognised by Idris 2

docs/source/tutorial/miscellany.rst

@@ -81,9 +81,9 @@ number as 0), we could write:
 
 .. code-block:: idris
 
-	fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
-	fibonacci {lag} Z = lag
-	fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
+        fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
+        fibonacci {lag} Z = lag
+        fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
 
 After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
 and will return the 5th fibonacci number. Note that while this works, this is not the
@@ -114,7 +114,9 @@ any other character).
 Cumulativity
 ============
 
-[NOT YET IN IDRIS 2]
+.. warning::
+
+   NOT YET IN IDRIS 2
 
 Since values can appear in types and *vice versa*, it is natural that
 types themselves have types. For example:

docs/source/tutorial/theorems.rst

@@ -126,7 +126,7 @@ To see more detail on what's going on, we can replace the recursive call to
 ``plusReducesZ`` with a hole:
 
 .. code-block:: idris
-    
+
     plusReducesZ (S k) = cong S ?help
 
 Then inspecting the type of the hole at the REPL shows us:
@@ -361,7 +361,9 @@ total, a function ``f`` must:
 Directives and Compiler Flags for Totality
 ------------------------------------------
 
-[NOTE: Not all of this is implemented yet for Idris 2]
+.. warning::
+
+   Not all of this is implemented yet for Idris 2
 
 By default, Idris allows all well-typed definitions, whether total or not.
 However, it is desirable for functions to be total as far as possible, as this

docs/source/tutorial/views.rst

@@ -4,7 +4,9 @@
 Views and the “``with``” rule
 *****************************
 
-[NOT UPDATED FOR IDRIS 2 YET]
+.. warning::
+
+   NOT UPDATED FOR IDRIS 2 YET
 
 Dependent pattern matching
 ==========================

docs/source/typedd/typedd.rst

@@ -461,4 +461,6 @@ In ``ATM.idr``, add:
 Chapter 15
 ----------
 
-TODO
+.. todo::
+
+   This chapter.