diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index 04c8c7a..190d453 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -33,9 +33,9 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
           <blockquote class="alectryon-goal">
             <div class="goal-hyps">
               <span class="hyp-type">
-                <var>{tyi.name}</var>
-                <b>: </b>
-                <span>{tyi.type}</span>
+                <var>{tyi.name}<//var>
+                <b>: <//b>
+                <span>{tyi.type}<//span>
               <//span>
             <//div>
           <//blockquote>
@@ -43,6 +43,13 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
       <//small>
     <//div>
 
+def Token.processSemantic (t : Token) : Html :=
+  match t.semanticType with
+  | some "Name.Attribute" => <span class="na">{t.raw}<//span>
+  | some "Name.Variable" => <span class="nv">{t.raw}<//span>
+  | some "Keyword" => <span class="k">{t.raw}<//span>
+  | _ => Html.text t.raw
+
 def Token.toHtml (t : Token) : AlectryonM Html := do
   -- Right now t.link is always none from LeanInk, ignore it
   -- TODO: render docstring
@@ -50,10 +57,11 @@ def Token.toHtml (t : Token) : AlectryonM Html := do
   if let some tyi := t.typeinfo then
     parts := parts.push $ ←tyi.toHtml
 
-  parts := parts.push $ Html.text t.raw
+  parts := parts.push t.processSemantic
+
   pure
     -- TODO: Show rest of token
-    <span class="alectryon-token" foo={t.link.getD "none"} bar={t.docstring.getD "none"}>
+    <span class="alectryon-token">
       [parts]
     <//span>
 
@@ -173,6 +181,7 @@ def baseHtml (content : Array Html) : AlectryonM Html := do
         <meta name="viewport" content="width=device-width, initial-scale=1"/>
 
         <link rel="stylesheet" href={s!"{←getRoot}src/alectryon.css"}/>
+        <link rel="stylesheet" href={s!"{←getRoot}src/pygments.css"}/>
         <link rel="stylesheet" href={s!"{←getRoot}src/docutils_basic.css"}/>
         <link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
 
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 5c11ebc..fe24651 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -82,6 +82,7 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
   FS.writeFile (srcBasePath / "alectryon.css") alectryonCss
   FS.writeFile (srcBasePath / "alectryon.js") alectryonJs
   FS.writeFile (srcBasePath / "docutils_basic.css") docUtilsCss
+  FS.writeFile (srcBasePath / "pygments.css") pygmentsCss
 
   for (modName, module) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath modName
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 63b1af1..b23cc6f 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -115,6 +115,7 @@ are used in documentation generation, notably JS and CSS ones.
   def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
   def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
   def docUtilsCss : String  := include_str "../../static/alectryon/docutils_basic.css"
+  def pygmentsCss : String  := include_str "../../static/alectryon/pygments.css"
 end Static
 
 /--
diff --git a/static/alectryon/pygments.css b/static/alectryon/pygments.css
new file mode 100644
index 0000000..d7b9245
--- /dev/null
+++ b/static/alectryon/pygments.css
@@ -0,0 +1,82 @@
+/* Pygments stylesheet generated by Alectryon (style=None) */
+/* Most of the following are unused as of now */
+td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
+td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
+.highlight .hll, .code .hll { background-color: #ffffcc }
+.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
+.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
+.highlight .g, .code .g { color: #000000 } /* Generic */
+.highlight .k, .code .k { color: #8f5902 } /* Keyword */
+.highlight .l, .code .l { color: #2e3436 } /* Literal */
+.highlight .n, .code .n { color: #000000 } /* Name */
+.highlight .o, .code .o { color: #000000 } /* Operator */
+.highlight .x, .code .x { color: #2e3436 } /* Other */
+.highlight .p, .code .p { color: #000000 } /* Punctuation */
+.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
+.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
+.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
+.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
+.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
+.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
+.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
+.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
+.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
+.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
+.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
+.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
+.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
+.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
+.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
+.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
+.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
+.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
+.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
+.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
+.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
+.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
+.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
+.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
+.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
+.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
+.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
+.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
+.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
+.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
+.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
+.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
+.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
+.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
+.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
+.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
+.highlight .py, .code .py { color: #000000 } /* Name.Property */
+.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
+.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
+.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
+.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
+.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
+.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
+.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
+.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
+.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
+.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
+.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
+.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
+.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
+.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
+.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
+.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
+.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
+.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
+.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
+.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
+.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
+.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
+.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
+.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
+.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
+.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
+.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
+.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
+.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */