@@ -10,13 +10,16 @@ module:
1010
1111 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
1212
13−This function takes a String and returns a list of tokens. With the tokens we
14−have indexes back to the original string which can be used in error messages:
13+.. list-table::
14+
15+ * - This function takes a String and returns a list of tokens. With the
16+ tokens we have indexes back to the original string which can be used
17+ in error messages:
1518
16−.. image:: ../image/tokenise.png
17− :width: 330px
18− :height: 73px
19− :alt: diagram illustrating these stages of lexer
19+ - .. image:: ../image/tokenise.png
20+ :width: 330px
21+ :height: 73px
22+ :alt: diagram illustrating these stages of lexer
2023
2124TokenMap
2225--------
@@ -34,21 +37,24 @@ this information:
3437 (Lexer, String -> tokenType)
3538
3639So for each Lexer in the list, if a substring in the input matches, run
37−the associated function to produce a token of type `tokenType`
40+the associated function to produce a token of type ``tokenType``
3841
39−from Text.Lexer.Core:
42+.. list-table::
4043
41−.. code-block:: idris
44+ * - from Text.Lexer.Core
45+ : https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer/Core.idr
4246
43− TokenMap : (tokenType : Type) -> Type
44− TokenMap tokenType = List (Lexer, String -> tokenType)
47+ - .. code-block:: idris
4548
46−We can create a tokenMap by using a function like this:
49+ TokenMap : (tokenType : Type) -> Type
50+ TokenMap tokenType = List (Lexer, String -> tokenType)
4751
48−.. code-block:: idris
52+ * - We can create a tokenMap by using a function like this:
53+
54+ - .. code-block:: idris
4955
50− myTokenMap : TokenMap Token
51− myTokenMap = [(is 'a',CharLit)]
56+ myTokenMap : TokenMap Token
57+ myTokenMap = [(is 'a',CharLit)]
5258
5359Once we have a TokenMap we can use it to lex many strings.
5460
@@ -74,7 +80,7 @@ combined, for example,
7480
7581.. list-table::
7682
77− * - <+> means sequence two recognisers. If either consumes a character,
83+ * - ``<+>`` means sequence two recognisers. If either consumes a character,
7884 the sequence is guaranteed to consume a character.
7985
8086 - .. code-block:: idris
@@ -83,7 +89,7 @@ combined, for example,
8389 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
8490 (Delay (is 'b')) : Recognise True
8591
86− * - <|> means if both consume, the combination is guaranteed
92+ * - ``<|>`` means if both consume, the combination is guaranteed
8793 to consumer a character:
8894
8995 - .. code-block:: idris
@@ -161,7 +167,7 @@ able to parse simple arithmetic expressions, like this:
161167so we need:
162168
163169- Numbers (for now integer literals are good enough).
164−- Some operators (for now '+', '-' and '*' will do.
170+- Some operators (for now ``+``, ``-`` and ``*`` will do.
165171- Opening and closing Parentheses.
166172
167173We can define these, as tokens, like this:
@@ -178,7 +184,7 @@ We can define these, as tokens, like this:
178184 | EndInput
179185
180186It may help with debugging and to implement error messages to
181−implement 'show' for these tokens:
187+implement ``show`` for these tokens:
182188
183189.. code-block:: idris
184190