Update documentation; write tutorial. (#687)

* Un-break the custom CSS. * Fix Pygments lexer for RedPRL. * Write tutorial, part one. * Write tutorial, part two.
RedPRL · Jun 8, 2018 · 6820113 · 6820113
1 parent 26606ed
commit 6820113
Show file tree

Hide file tree

Showing 5 changed files with 178 additions and 235 deletions.
diff --git a/doc/src/conf.py b/doc/src/conf.py
@@ -73,7 +73,7 @@
 exclude_patterns = ['build', 'Thumbs.db', '.DS_Store']
 
 # The name of the Pygments (syntax highlighting) style to use.
-pygments_style = 'sphinx'
+pygments_style = 'colorful'
 
 # If true, `todo` and `todoList` produce output, else they produce nothing.
 todo_include_todos = True

diff --git a/doc/src/redprl.py b/doc/src/redprl.py
@@ -30,6 +30,9 @@ class RedPRLLexer(RegexLexer):
              'line', 'pushout', 'coeq', 'eq', 'fcom', 'V', 'universe', 'hcom',
              'coe', 'subtype', 'universe']
 
+    def joiner(arr):
+        return '|'.join(map(lambda str: '\\b' + str + '\\b', arr))
+
     # earlier rules take precedence
     tokens = {
         'root': [
@@ -38,18 +41,20 @@ class RedPRLLexer(RegexLexer):
             (r'//.*?$', Comment.Singleline),
             (r'/\*', Comment.Multiline, 'comment'),
 
-            ('/[\w/]+|\\b'.join(types), Name.Builtin),
-            ('|\\b'.join(exprs), Name.Builtin),
+            (joiner(map(lambda str: str + '/[\w/]+', types)), Name.Builtin),
+            (joiner(exprs), Name.Builtin),
+            (joiner(types), Name.Builtin),
             (r'\$|\*|!|@|=(?!>)|\+|->|~>|<~', Name.Builtin),
 
-            ('|\\b'.join(tacs), Keyword),
+            (joiner(tacs), Keyword),
             (r';|`|=>|<=', Keyword),
 
-            ('|\\b'.join(cmds), Keyword.Declaration),
+            (joiner(cmds), Keyword.Declaration),
 
-            ('|\\b'.join(misc), Name.Builtin),
+            (joiner(misc), Name.Builtin),
 
             (r'\#[a-zA-Z0-9\'/-]*', Name.Variable),
+            (r'\%[a-zA-Z0-9\'/-]*', Name.Variable),
 
             (r'\(|\)|\[|\]|\.|:|,|\{|\}|_', Punctuation),
             (r'\b\d+', Number),
@@ -58,12 +63,16 @@ class RedPRLLexer(RegexLexer):
             (r'^\|', Generic.Traceback),
             (r'>>', Name.Keyword),
             (r'<-', Name.Keyword),
+            (r'/=', Name.Keyword),
+            (r'<', Name.Keyword),
             (r'ext', Name.Keyword),
             (r'where', Name.Keyword),
 
+            (r'\|', Punctuation),
             (r'[A-Z][a-zA-Z0-9\'/-]*', Name.Function),
             (r'[a-z][a-zA-Z0-9\'/-]*', Name.Variable),
             (r'\?[a-zA-Z0-9\'/-]*', Name.Exception),
+            (r'-+$', Punctuation),
         ],
 
         'comment': [

diff --git a/doc/src/refine.rst b/doc/src/refine.rst
@@ -10,6 +10,8 @@ Booleans
 
   H >> bool = bool in (U #l #k)
 
+.. _bool/eq/tt:
+
 :index:`bool/eq/tt`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 ::

diff --git a/doc/src/static/red.css b/doc/src/static/red.css
@@ -79,13 +79,13 @@ code {
 }
 
 div[class^='highlight'] pre {
-  font-size: 14px;
+  font-size: 14px !important;
   line-height: 1.5 !important;
   padding: 12px 20px;
 }
 
 div[class^='highlight'] {
-  border: none;
+  border: none !important;
   background: initial;
 }
 
@@ -94,7 +94,7 @@ div[class^='highlight'] {
   font-weight: 700;
 }
 
-pre .gt {
+.highlight .gt {
   background-color: #f7bcbb;
   color: #f7bcbb;
   padding: 3px 0;