diff --git a/app/Commands/Dev/Latex/Export.hs b/app/Commands/Dev/Latex/Export.hs
index b3ac3418d8..038a3e50f8 100644
--- a/app/Commands/Dev/Latex/Export.hs
+++ b/app/Commands/Dev/Latex/Export.hs
@@ -6,7 +6,6 @@ where
 
 import Commands.Base
 import Commands.Dev.Latex.Export.Options
-import Data.String.Interpolate (__i)
 import Data.Text qualified as Text
 import Juvix.Compiler.Backend.Latex.Translation.FromScoped.Source
 import Juvix.Compiler.Concrete.Language
diff --git a/app/Commands/Dev/Nockma.hs b/app/Commands/Dev/Nockma.hs
index 889a8af1d0..08c72c99cb 100644
--- a/app/Commands/Dev/Nockma.hs
+++ b/app/Commands/Dev/Nockma.hs
@@ -4,6 +4,7 @@ import Commands.Base
 import Commands.Dev.Nockma.Encode as Encode
 import Commands.Dev.Nockma.Eval as Eval
 import Commands.Dev.Nockma.Format as Format
+import Commands.Dev.Nockma.Ide as Ide
 import Commands.Dev.Nockma.Options
 import Commands.Dev.Nockma.Repl as Repl
 import Commands.Dev.Nockma.Run as Run
@@ -15,3 +16,4 @@ runCommand = \case
   NockmaFormat opts -> Format.runCommand opts
   NockmaRun opts -> Run.runCommand opts
   NockmaEncode opts -> Encode.runCommand opts
+  NockmaIde opts -> Ide.runCommand opts
diff --git a/app/Commands/Dev/Nockma/Format.hs b/app/Commands/Dev/Nockma/Format.hs
index d1a2c6c0a9..9878a814f7 100644
--- a/app/Commands/Dev/Nockma/Format.hs
+++ b/app/Commands/Dev/Nockma/Format.hs
@@ -8,7 +8,10 @@ import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 runCommand :: forall r. (Members AppEffects r) => NockmaFormatOptions -> Sem r ()
 runCommand opts = do
   afile <- fromAppPathFile file
-  parsedTerm <- runAppError @JuvixError (Nockma.parseTermFile afile)
+  parsedTerm <-
+    runAppError @JuvixError
+      . Nockma.ignoreHighlightBuilder
+      $ Nockma.parseTermFile afile
   putStrLn (ppPrint parsedTerm)
   where
     file :: AppPath File
diff --git a/app/Commands/Dev/Nockma/Ide.hs b/app/Commands/Dev/Nockma/Ide.hs
new file mode 100644
index 0000000000..16ee3522de
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide.hs
@@ -0,0 +1,17 @@
+module Commands.Dev.Nockma.Ide where
+
+import Commands.Base
+import Commands.Dev.Nockma.Ide.Check as Check
+import Commands.Dev.Nockma.Ide.Highlight as Highlight
+import Commands.Dev.Nockma.Ide.Options
+import Commands.Dev.Nockma.Ide.Rules as Rules
+
+runCommand ::
+  forall r.
+  (Members AppEffects r) =>
+  NockmaIdeCommand ->
+  Sem r ()
+runCommand = \case
+  NockmaIdeHighlight opts -> Highlight.runCommand opts
+  NockmaIdeCheck opts -> Check.runCommand opts
+  NockmaIdeRules {} -> Rules.runCommand
diff --git a/app/Commands/Dev/Nockma/Ide/Check.hs b/app/Commands/Dev/Nockma/Ide/Check.hs
new file mode 100644
index 0000000000..85f0cb771a
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Check.hs
@@ -0,0 +1,15 @@
+module Commands.Dev.Nockma.Ide.Check where
+
+import Commands.Base hiding (Atom)
+import Commands.Dev.Nockma.Ide.Check.Options
+import Juvix.Compiler.Nockma.Highlight
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+
+runCommand :: forall r. (Members AppEffects r) => NockmaCheckOptions -> Sem r ()
+runCommand opts = do
+  afile <- fromAppPathFile (opts ^. nockmaCheckFile)
+  void
+    . runAppError @JuvixError
+    . ignoreHighlightBuilder
+    $ Nockma.parseTermFile afile
+  renderStdOutLn ("Ok" :: Text)
diff --git a/app/Commands/Dev/Nockma/Ide/Check/Options.hs b/app/Commands/Dev/Nockma/Ide/Check/Options.hs
new file mode 100644
index 0000000000..eef30fdccb
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Check/Options.hs
@@ -0,0 +1,15 @@
+module Commands.Dev.Nockma.Ide.Check.Options where
+
+import CommonOptions
+
+newtype NockmaCheckOptions = NockmaCheckOptions
+  { _nockmaCheckFile :: AppPath File
+  }
+  deriving stock (Data)
+
+makeLenses ''NockmaCheckOptions
+
+parseNockmaCheckOptions :: Parser NockmaCheckOptions
+parseNockmaCheckOptions = do
+  _nockmaCheckFile <- parseInputFile FileExtNockma
+  pure NockmaCheckOptions {..}
diff --git a/app/Commands/Dev/Nockma/Ide/Highlight.hs b/app/Commands/Dev/Nockma/Ide/Highlight.hs
new file mode 100644
index 0000000000..8ee563fc0c
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Highlight.hs
@@ -0,0 +1,27 @@
+module Commands.Dev.Nockma.Ide.Highlight where
+
+import Commands.Base hiding (Atom)
+import Commands.Dev.Nockma.Ide.Highlight.Options
+import Juvix.Compiler.Nockma.Highlight
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
+
+runCommand :: forall r. (Members AppEffects r) => NockmaHighlightOptions -> Sem r ()
+runCommand opts = silenceProgressLog . runPipelineOptions $ do
+  afile <- fromAppPathFile (opts ^. nockmaHighlightFile)
+  hinput <-
+    fmap (filterInput afile)
+      . runJuvixErrorHighlight
+      . execHighlightBuilder
+      $ Nockma.parseTermFile afile
+  renderStdOutRaw (highlight hinput)
+  newline
+
+runJuvixErrorHighlight :: forall r. Sem (Error JuvixError ': r) HighlightInput -> Sem r HighlightInput
+runJuvixErrorHighlight m = do
+  res <- runError m
+  return $ case res of
+    Right r -> r
+    Left err ->
+      emptyHighlightInput
+        { _highlightErrors = [getLoc err]
+        }
diff --git a/app/Commands/Dev/Nockma/Ide/Highlight/Options.hs b/app/Commands/Dev/Nockma/Ide/Highlight/Options.hs
new file mode 100644
index 0000000000..de77f7bcfd
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Highlight/Options.hs
@@ -0,0 +1,15 @@
+module Commands.Dev.Nockma.Ide.Highlight.Options where
+
+import CommonOptions
+
+newtype NockmaHighlightOptions = NockmaHighlightOptions
+  { _nockmaHighlightFile :: AppPath File
+  }
+  deriving stock (Data)
+
+makeLenses ''NockmaHighlightOptions
+
+parseNockmaHighlightOptions :: Parser NockmaHighlightOptions
+parseNockmaHighlightOptions = do
+  _nockmaHighlightFile <- parseInputFile FileExtNockma
+  pure NockmaHighlightOptions {..}
diff --git a/app/Commands/Dev/Nockma/Ide/Options.hs b/app/Commands/Dev/Nockma/Ide/Options.hs
new file mode 100644
index 0000000000..8c3a4c485e
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Options.hs
@@ -0,0 +1,47 @@
+module Commands.Dev.Nockma.Ide.Options where
+
+import Commands.Dev.Nockma.Ide.Check.Options
+import Commands.Dev.Nockma.Ide.Highlight.Options
+import CommonOptions
+
+data NockmaIdeCommand
+  = NockmaIdeHighlight NockmaHighlightOptions
+  | NockmaIdeCheck NockmaCheckOptions
+  | NockmaIdeRules
+  deriving stock (Data)
+
+parseNockmaIdeCommand :: Parser NockmaIdeCommand
+parseNockmaIdeCommand =
+  hsubparser $
+    mconcat
+      [ commandHighlight,
+        commandCheck,
+        commandRules
+      ]
+  where
+    commandHighlight :: Mod CommandFields NockmaIdeCommand
+    commandHighlight = command "highlight" runInfo
+      where
+        runInfo :: ParserInfo NockmaIdeCommand
+        runInfo =
+          info
+            (NockmaIdeHighlight <$> parseNockmaHighlightOptions)
+            (progDesc "Highlight a nockma term (only for Emacs)")
+
+    commandRules :: Mod CommandFields NockmaIdeCommand
+    commandRules = command "rules" runInfo
+      where
+        runInfo :: ParserInfo NockmaIdeCommand
+        runInfo =
+          info
+            (pure NockmaIdeRules)
+            (progDesc "Print the nockma evaluation rules")
+
+    commandCheck :: Mod CommandFields NockmaIdeCommand
+    commandCheck = command "check" runInfo
+      where
+        runInfo :: ParserInfo NockmaIdeCommand
+        runInfo =
+          info
+            (NockmaIdeCheck <$> parseNockmaCheckOptions)
+            (progDesc "Parse a nockma term")
diff --git a/app/Commands/Dev/Nockma/Ide/Rules.hs b/app/Commands/Dev/Nockma/Ide/Rules.hs
new file mode 100644
index 0000000000..af8cc53f81
--- /dev/null
+++ b/app/Commands/Dev/Nockma/Ide/Rules.hs
@@ -0,0 +1,12 @@
+module Commands.Dev.Nockma.Ide.Rules where
+
+import Commands.Base
+import Juvix.Compiler.Nockma.Highlight.Doc
+import Juvix.Emacs.Render
+import Juvix.Emacs.SExp
+
+runCommand :: forall r. (Members AppEffects r) => Sem r ()
+runCommand = do
+  let (txt, format) = renderEmacs allRules
+      ret = Pair (String txt) format
+  renderStdOutLn (toPlainText ret)
diff --git a/app/Commands/Dev/Nockma/Options.hs b/app/Commands/Dev/Nockma/Options.hs
index 077714b11a..def0d10493 100644
--- a/app/Commands/Dev/Nockma/Options.hs
+++ b/app/Commands/Dev/Nockma/Options.hs
@@ -3,6 +3,7 @@ module Commands.Dev.Nockma.Options where
 import Commands.Dev.Nockma.Encode.Options
 import Commands.Dev.Nockma.Eval.Options
 import Commands.Dev.Nockma.Format.Options
+import Commands.Dev.Nockma.Ide.Options
 import Commands.Dev.Nockma.Repl.Options
 import Commands.Dev.Nockma.Run.Options
 import CommonOptions
@@ -13,6 +14,7 @@ data NockmaCommand
   | NockmaFormat NockmaFormatOptions
   | NockmaRun NockmaRunOptions
   | NockmaEncode NockmaEncodeOptions
+  | NockmaIde NockmaIdeCommand
   deriving stock (Data)
 
 parseNockmaCommand :: Parser NockmaCommand
@@ -23,9 +25,19 @@ parseNockmaCommand =
         commandFromAsm,
         commandFormat,
         commandEncode,
+        commandIde,
         commandRun
       ]
   where
+    commandIde :: Mod CommandFields NockmaCommand
+    commandIde = command "ide" runInfo
+      where
+        runInfo :: ParserInfo NockmaCommand
+        runInfo =
+          info
+            (NockmaIde <$> parseNockmaIdeCommand)
+            (progDesc "Ide related subcommands")
+
     commandEncode :: Mod CommandFields NockmaCommand
     commandEncode = command "encode" runInfo
       where
diff --git a/app/Commands/Dev/Nockma/Repl.hs b/app/Commands/Dev/Nockma/Repl.hs
index 8bac5c6cce..50e45137bc 100644
--- a/app/Commands/Dev/Nockma/Repl.hs
+++ b/app/Commands/Dev/Nockma/Repl.hs
@@ -4,7 +4,6 @@ import Commands.Base hiding (Atom)
 import Commands.Dev.Nockma.Repl.Options
 import Control.Exception (throwIO)
 import Control.Monad.State.Strict qualified as State
-import Data.String.Interpolate (__i)
 import Juvix.Compiler.Nockma.Evaluator (NockEvalError, evalRepl, fromReplTerm, programAssignments)
 import Juvix.Compiler.Nockma.Evaluator.Options
 import Juvix.Compiler.Nockma.Language
diff --git a/app/Commands/Dev/Tree/Repl.hs b/app/Commands/Dev/Tree/Repl.hs
index 81d1e0ba41..e06fff13c3 100644
--- a/app/Commands/Dev/Tree/Repl.hs
+++ b/app/Commands/Dev/Tree/Repl.hs
@@ -4,7 +4,6 @@ import Commands.Base hiding (Atom)
 import Commands.Dev.Tree.Repl.Options
 import Control.Exception (throwIO)
 import Control.Monad.State.Strict qualified as State
-import Data.String.Interpolate (__i)
 import Juvix.Compiler.Tree.Data.InfoTable
 import Juvix.Compiler.Tree.Data.InfoTableBuilder qualified as Tree
 import Juvix.Compiler.Tree.Language
diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs
index 23a732c9f5..c7a87ffa92 100644
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@@ -11,7 +11,7 @@ import Control.Monad.Reader qualified as Reader
 import Control.Monad.State.Strict qualified as State
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Trans.Reader (mapReaderT)
-import Data.String.Interpolate (i, __i)
+import Data.String.Interpolate (i)
 import HaskelineJB
 import Juvix.Compiler.Concrete.Data.Scope (scopePath)
 import Juvix.Compiler.Concrete.Data.Scope qualified as Scoped
diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs
index d59c22bdf1..e551065436 100644
--- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs
+++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs
@@ -324,6 +324,7 @@ putTag ann x = case ann of
   AnnKeyword -> return (Html.span ! juClass JuKeyword $ x)
   AnnUnkindedSym -> return (Html.span ! juClass JuVar $ x)
   AnnComment -> return (Html.span ! juClass JuComment $ x)
+  AnnPragma -> return (Html.span ! juClass JuComment $ x)
   AnnJudoc -> return (Html.span ! juClass JuJudoc $ x)
   AnnDelimiter -> return (Html.span ! juClass JuDelimiter $ x)
   AnnDef r -> boldDefine <*> tagDef r
diff --git a/src/Juvix/Compiler/Backend/Latex/Translation/FromScoped/Source.hs b/src/Juvix/Compiler/Backend/Latex/Translation/FromScoped/Source.hs
index cb8befe2b5..779b124885 100644
--- a/src/Juvix/Compiler/Backend/Latex/Translation/FromScoped/Source.hs
+++ b/src/Juvix/Compiler/Backend/Latex/Translation/FromScoped/Source.hs
@@ -108,6 +108,7 @@ putTag ann x = case ann of
   AnnComment -> juColor JuComment x
   AnnJudoc -> juColor JuJudoc x
   AnnDelimiter -> juColor JuDelimiter x
+  AnnPragma -> juColor JuComment x
   AnnDef {} -> x
   AnnRef {} -> x
   AnnCode -> x
diff --git a/src/Juvix/Compiler/Concrete/Data.hs b/src/Juvix/Compiler/Concrete/Data.hs
index dd842a64ff..af6ea9c3f4 100644
--- a/src/Juvix/Compiler/Concrete/Data.hs
+++ b/src/Juvix/Compiler/Concrete/Data.hs
@@ -8,7 +8,6 @@ module Juvix.Compiler.Concrete.Data
     module Juvix.Compiler.Store.Scoped.Data.InfoTable,
     module Juvix.Compiler.Concrete.Data.InfoTableBuilder,
     module Juvix.Data.NameKind,
-    module Juvix.Compiler.Concrete.Data.ParsedItem,
     module Juvix.Compiler.Concrete.Data.VisibilityAnn,
     module Juvix.Compiler.Concrete.Data.Literal,
     module Juvix.Compiler.Concrete.Data.NameRef,
@@ -27,7 +26,6 @@ import Juvix.Compiler.Concrete.Data.LocalModuleOrigin
 import Juvix.Compiler.Concrete.Data.ModuleIsTop
 import Juvix.Compiler.Concrete.Data.Name
 import Juvix.Compiler.Concrete.Data.NameRef
-import Juvix.Compiler.Concrete.Data.ParsedItem
 import Juvix.Compiler.Concrete.Data.PublicAnn
 import Juvix.Compiler.Concrete.Data.ScopedName qualified
 import Juvix.Compiler.Concrete.Data.VisibilityAnn
diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight.hs b/src/Juvix/Compiler/Concrete/Data/Highlight.hs
index eb9f6fe1c8..da8385b993 100644
--- a/src/Juvix/Compiler/Concrete/Data/Highlight.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Highlight.hs
@@ -1,7 +1,7 @@
 module Juvix.Compiler.Concrete.Data.Highlight
   ( module Juvix.Compiler.Concrete.Data.Highlight,
     module Juvix.Compiler.Concrete.Data.Highlight.Builder,
-    module Juvix.Compiler.Concrete.Data.Highlight.Properties,
+    module Juvix.Emacs.Properties,
   )
 where
 
@@ -10,14 +10,14 @@ import Data.ByteString.Lazy qualified as ByteString
 import Data.Text.Encoding qualified as Text
 import Juvix.Compiler.Concrete.Data.Highlight.Builder
 import Juvix.Compiler.Concrete.Data.Highlight.PrettyJudoc
-import Juvix.Compiler.Concrete.Data.Highlight.Properties
-import Juvix.Compiler.Concrete.Data.Highlight.RenderEmacs
 import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
 import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as Scoped
 import Juvix.Data.CodeAnn
-import Juvix.Data.Emacs
+import Juvix.Emacs.Properties
+import Juvix.Emacs.Render
+import Juvix.Emacs.SExp
 import Juvix.Prelude as Prelude hiding (show)
 import Prelude qualified
 
@@ -44,12 +44,31 @@ buildProperties HighlightInput {..} =
           <> mapMaybe goFaceName _highlightNames
           <> map goFaceError _highlightErrors,
       _propertiesGoto = map goGotoProperty _highlightNames,
-      _propertiesDoc = mapMaybe (goDocProperty _highlightDocTable _highlightTypes) _highlightNames
+      _propertiesInfo = mapMaybe (goDocProperty _highlightDocTable _highlightTypes) _highlightNames
     }
 
 goFaceError :: Interval -> WithLoc PropertyFace
 goFaceError i = WithLoc i (PropertyFace FaceError)
 
+goFaceSemanticItem :: SemanticItem -> Maybe (WithLoc PropertyFace)
+goFaceSemanticItem i = WithLoc (getLoc i) . PropertyFace <$> f
+  where
+    f :: Maybe Face
+    f = case i ^. withLocParam of
+      AnnKind k -> nameKindFace k
+      AnnKeyword -> Just FaceKeyword
+      AnnComment -> Just FaceComment
+      AnnPragma -> Just FacePragma
+      AnnJudoc -> Just FaceJudoc
+      AnnDelimiter -> Just FaceDelimiter
+      AnnLiteralString -> Just FaceString
+      AnnLiteralInteger -> Just FaceNumber
+      AnnCode -> Nothing
+      AnnImportant -> Nothing
+      AnnUnkindedSym -> Nothing
+      AnnDef {} -> Nothing
+      AnnRef {} -> Nothing
+
 goFaceParsedItem :: ParsedItem -> WithLoc PropertyFace
 goFaceParsedItem i = WithLoc (i ^. parsedLoc) (PropertyFace f)
   where
@@ -73,9 +92,10 @@ goGotoProperty n = WithLoc (getLoc n) PropertyGoto {..}
     _gotoPos = n ^. anameDefinedLoc . intervalStart
     _gotoFile = n ^. anameDefinedLoc . intervalFile
 
-goDocProperty :: Scoped.DocTable -> Internal.TypesTable -> AName -> Maybe (WithLoc PropertyDoc)
+goDocProperty :: Scoped.DocTable -> Internal.TypesTable -> AName -> Maybe (WithLoc PropertyInfo)
 goDocProperty doctbl tbl a = do
   let ty :: Maybe Internal.Expression = tbl ^. Internal.typesTable . at (a ^. anameDocId)
   d <- ppDocDefault a ty (doctbl ^. at (a ^. anameDocId))
-  let (_docText, _docSExp) = renderEmacs (layoutPretty defaultLayoutOptions d)
-  return (WithLoc (getLoc a) PropertyDoc {..})
+  let (txt, _infoInit) = renderEmacs d
+      _infoInfo = String txt
+  return (WithLoc (getLoc a) PropertyInfo {..})
diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/Builder.hs b/src/Juvix/Compiler/Concrete/Data/Highlight/Builder.hs
index 1fbbf4ed71..97fb216d4f 100644
--- a/src/Juvix/Compiler/Concrete/Data/Highlight/Builder.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Highlight/Builder.hs
@@ -1,13 +1,11 @@
 module Juvix.Compiler.Concrete.Data.Highlight.Builder
   ( module Juvix.Compiler.Concrete.Data.Highlight.Input,
-    module Juvix.Compiler.Concrete.Data.ParsedItem,
     module Juvix.Compiler.Concrete.Data.Highlight.Builder,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.Highlight.Input
-import Juvix.Compiler.Concrete.Data.ParsedItem
 import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Internal.Language qualified as Internal
diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/Input.hs b/src/Juvix/Compiler/Concrete/Data/Highlight/Input.hs
index f0c46ee473..9b29d50dab 100644
--- a/src/Juvix/Compiler/Concrete/Data/Highlight/Input.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Highlight/Input.hs
@@ -1,10 +1,5 @@
-module Juvix.Compiler.Concrete.Data.Highlight.Input
-  ( module Juvix.Compiler.Concrete.Data.Highlight.Input,
-    module Juvix.Compiler.Concrete.Data.ParsedItem,
-  )
-where
+module Juvix.Compiler.Concrete.Data.Highlight.Input where
 
-import Juvix.Compiler.Concrete.Data.ParsedItem
 import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index 9f4ec87e2f..e5b6a4f24b 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -119,8 +119,8 @@ literalInteger a = do
 mkList :: (Member (Reader Interval) r) => [NonEmpty (ExpressionAtom 'Parsed)] -> Sem r (ExpressionAtom 'Parsed)
 mkList as = do
   items <- mapM expressionAtoms' as
-  parenR <- Irrelevant <$> kw kwBracketR
-  parenL <- Irrelevant <$> kw kwBracketL
+  parenR <- Irrelevant <$> kw delimBracketR
+  parenL <- Irrelevant <$> kw delimBracketL
   return
     ( AtomList
         List
diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs
index a254061802..5eab9722a8 100644
--- a/src/Juvix/Compiler/Concrete/Keywords.hs
+++ b/src/Juvix/Compiler/Concrete/Keywords.hs
@@ -10,6 +10,8 @@ import Juvix.Data.Keyword.All
   ( -- delimiters
     delimBraceL,
     delimBraceR,
+    delimBracketL,
+    delimBracketR,
     delimDoubleBraceL,
     delimDoubleBraceR,
     delimJudocBlockEnd,
@@ -30,8 +32,6 @@ import Juvix.Data.Keyword.All
     kwAxiom,
     kwBelow,
     kwBinary,
-    kwBracketL,
-    kwBracketR,
     kwBuiltin,
     kwCase,
     kwCoercion,
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index e0ea1b48f9..09f2f338bf 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -894,9 +894,9 @@ instance PrettyPrint BinaryAssoc where
 
 ppSymbolList :: (SingI s) => PrettyPrinting [SymbolType s]
 ppSymbolList items = do
-  ppCode Kw.kwBracketL
+  ppCode Kw.delimBracketL
   hsepSemicolon (map ppSymbolType items)
-  ppCode Kw.kwBracketR
+  ppCode Kw.delimBracketR
 
 instance (SingI s) => PrettyPrint (ParsedFixityInfo s) where
   ppCode ParsedFixityInfo {..} = do
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index b75a497588..3620253ea2 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -716,9 +716,9 @@ parsedFixityFields = do
     belowAbove aboveOrBelow = do
       kw aboveOrBelow
       kw kwAssign
-      kw kwBracketL
+      kw delimBracketL
       r <- P.sepEndBy symbol semicolon
-      kw kwBracketR
+      kw delimBracketR
       return r
 
     assoc :: ParsecS r BinaryAssoc
@@ -1062,16 +1062,16 @@ hole = kw kwHole
 
 parseListPattern :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ListPattern 'Parsed)
 parseListPattern = do
-  _listpBracketL <- Irrelevant <$> kw kwBracketL
+  _listpBracketL <- Irrelevant <$> kw delimBracketL
   _listpItems <- P.sepEndBy parsePatternAtoms (kw delimSemicolon)
-  _listpBracketR <- Irrelevant <$> kw kwBracketR
+  _listpBracketR <- Irrelevant <$> kw delimBracketR
   return ListPattern {..}
 
 parseList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (List 'Parsed)
 parseList = do
-  _listBracketL <- Irrelevant <$> kw kwBracketL
+  _listBracketL <- Irrelevant <$> kw delimBracketL
   _listItems <- P.sepEndBy parseExpressionAtoms (kw delimSemicolon)
-  _listBracketR <- Irrelevant <$> kw kwBracketR
+  _listBracketR <- Irrelevant <$> kw delimBracketR
   return List {..}
 
 --------------------------------------------------------------------------------
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/Data/ParserState.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/Data/ParserState.hs
index 8dbda22bcf..d5d88bc1dd 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource/Data/ParserState.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/Data/ParserState.hs
@@ -1,6 +1,5 @@
 module Juvix.Compiler.Concrete.Translation.FromSource.Data.ParserState where
 
-import Juvix.Compiler.Concrete.Data.ParsedItem
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
 
diff --git a/src/Juvix/Compiler/Nockma/Highlight.hs b/src/Juvix/Compiler/Nockma/Highlight.hs
new file mode 100644
index 0000000000..acce27b9dd
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight.hs
@@ -0,0 +1,89 @@
+module Juvix.Compiler.Nockma.Highlight
+  ( module Juvix.Compiler.Nockma.Highlight.Input,
+    module Juvix.Compiler.Nockma.Highlight.Base,
+    module Juvix.Compiler.Nockma.Highlight,
+  )
+where
+
+import Juvix.Compiler.Concrete.Data.Highlight (goFaceError, goFaceSemanticItem)
+import Juvix.Compiler.Nockma.Highlight.Base
+import Juvix.Compiler.Nockma.Highlight.Doc
+import Juvix.Compiler.Nockma.Highlight.Input
+import Juvix.Compiler.Nockma.Language as Nockma
+import Juvix.Data.CodeAnn
+import Juvix.Emacs.Render
+import Juvix.Emacs.SExp
+import Juvix.Prelude
+
+highlight :: HighlightInput -> ByteString
+highlight = encodeUtf8 . renderSExp . withDocTable . toSExp . buildProperties
+
+buildProperties :: HighlightInput -> LocProperties
+buildProperties HighlightInput {..} =
+  LocProperties
+    { _propertiesFace =
+        mapMaybe goFaceSemanticItem _highlightSemanticItems
+          <> map goFaceError _highlightErrors,
+      _propertiesGoto = [],
+      _propertiesInfo = map goInfoNockOp _highlightNockOps <> map goInfoPath _highlightPaths
+    }
+
+-- | Used in nockma-mode
+nockOpKey :: NockOp -> Text
+nockOpKey = \case
+  OpAddress -> "OpAddress"
+  OpQuote -> "OpQuote"
+  OpApply -> "OpApply"
+  OpIsCell -> "OpIsCell"
+  OpInc -> "OpInc"
+  OpEq -> "OpEq"
+  OpIf -> "OpIf"
+  OpSequence -> "OpSequence"
+  OpPush -> "OpPush"
+  OpCall -> "OpCall"
+  OpReplace -> "OpReplace"
+  OpHint -> "OpHint"
+  OpScry -> "OpScry"
+
+-- | nockma-mode depends on this
+docTableVarName :: Text
+docTableVarName = "nockma-doc-table"
+
+-- | NockOp ↦ (txt, init)
+withDocTable :: SExp -> SExp
+withDocTable body =
+  progn
+    [ mkHashTable
+        docTableVarName
+        [ (Quote (Symbol (nockOpKey op)), Quote (Pair (String docTxt) initExpr)) | op <- allElements, let (docTxt, initExpr) = renderEmacs (nockOpDoc op)
+        ],
+      body
+    ]
+
+goInfoPath :: WithLoc Nockma.Path -> WithLoc PropertyInfo
+goInfoPath = fmap toProperty
+  where
+    toProperty :: Nockma.Path -> PropertyInfo
+    toProperty p =
+      PropertyInfo
+        { _infoInfo = String txt,
+          _infoInit = format
+        }
+      where
+        (txt, format) = renderEmacs msg
+
+        msg :: Doc CodeAnn
+        msg =
+          ppCodeAnn p
+            <+> kwEquals
+            <+> pretty (encodePath p ^. encodedPath)
+
+goInfoNockOp :: WithLoc NockOp -> WithLoc PropertyInfo
+goInfoNockOp = fmap toProperty
+  where
+    toProperty :: NockOp -> PropertyInfo
+    toProperty o =
+      PropertyInfo
+        { _infoInfo = Symbol (nockOpKey o),
+          _infoInit = nil
+        }
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Base.hs b/src/Juvix/Compiler/Nockma/Highlight/Base.hs
new file mode 100644
index 0000000000..841e1e7510
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Base.hs
@@ -0,0 +1,6 @@
+module Juvix.Compiler.Nockma.Highlight.Base
+  ( module Juvix.Emacs.Properties,
+  )
+where
+
+import Juvix.Emacs.Properties
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc.hs
new file mode 100644
index 0000000000..012b0f186d
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc.hs
@@ -0,0 +1,122 @@
+module Juvix.Compiler.Nockma.Highlight.Doc (nockOpDoc, allRules) where
+
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Compiler.Nockma.Highlight.Doc.Parser
+import Juvix.Compiler.Nockma.Highlight.Doc.Pretty ()
+import Juvix.Data.CodeAnn as CodeAnn
+import Juvix.Prelude
+
+allRules :: Doc CodeAnn
+allRules =
+  concatWith
+    ( \a b ->
+        a
+          <> hardline
+          <> hardline
+          <> hardline
+          <> hardline
+          <> hardline
+          <> hardline
+          <> b
+    )
+    (map ppRule allElements)
+  where
+    ppRule :: NockOp -> Doc CodeAnn
+    ppRule op =
+      ppCodeAnn op
+        <+> "("
+          <> show op
+          <> ")"
+        <+> "evaluation rules:"
+          <> hardline
+          <> nockOpDoc op
+
+nockOpDoc :: NockOp -> Doc CodeAnn
+nockOpDoc n = ppCodeAnn $ case n of
+  OpAddress ->
+    [rules|
+    ---
+    s * [@ p] => index(s; p)
+    |]
+  OpQuote ->
+    [rules|
+    ---
+    s * [quote t] => t
+    |]
+  OpApply ->
+    [rules|
+    s * t1 => t1' && s * t2 => t2'  && t1' * t2' => t'
+    ---
+    s * [apply [t1 t2]] => t'
+    |]
+  OpIsCell ->
+    [rules|
+    s * t => [t1' t2']
+    ---
+    s * [isCell t] => 0
+    and
+    s * t => a
+    ---
+    s * [isCell t] => 1
+    |]
+  OpInc ->
+    [rules|
+    s * t => n
+    ---
+    s * [suc t] => suc(t)
+    |]
+  OpEq ->
+    [rules|
+    ---
+    s * [= [t t]] => 0
+    and
+    neq(t1; t2)
+    ---
+    s * [= [t1 t2]] => 1
+    |]
+  OpIf ->
+    [rules|
+    s * t0 => 0 && s * t1 => t1'
+    ---
+    s * [if [t0 [t1 t2]]] => t1'
+    and
+    s * t0 => 1 && s * t2 => t2'
+    ---
+    s * [if [t0 [t1 t2]]] => t2'
+    |]
+  OpSequence ->
+    [rules|
+    s * t1 => t1' && t1' * t2 => t'
+    ---
+    s * [seq [t1 t2]] => t'
+    |]
+  OpPush ->
+    [rules|
+    s * t1 => t1' && [t1' s] * t2 => t'
+    ---
+    s * [push [t1 t2]] => t'
+    |]
+  OpCall ->
+    [rules|
+    s * t => t' && t' * index(t'; p) => t''
+    ---
+    s * [call [p t]] => t''
+    |]
+  OpReplace ->
+    [rules|
+    s * t1 => t1' && s * t2 => t2'
+    ---
+    s * [replace [[p t1] t2]] => replace(t2';p;t1')
+    |]
+  OpHint ->
+    [rules|
+    s * t2 => t2' && s * t3 => t3'
+    ---
+    s * [hint [[t1 t2] t3]] => t3'
+    |]
+  OpScry ->
+    [rules|
+    s * t1 => t1' && s * t2 => t2'
+    ---
+    s * [scry [t1 t2]] => index(storage; t2')
+    |]
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc/Base.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc/Base.hs
new file mode 100644
index 0000000000..1b4d2a27d6
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc/Base.hs
@@ -0,0 +1,145 @@
+module Juvix.Compiler.Nockma.Highlight.Doc.Base
+  ( module Juvix.Compiler.Nockma.Highlight.Doc.Base,
+    module Juvix.Compiler.Nockma.Language,
+    module Juvix.Data.Keyword.All,
+  )
+where
+
+import Juvix.Compiler.Nockma.Language (NockOp (..))
+import Juvix.Data.Keyword.All
+  ( delimBraceL,
+    delimBraceR,
+    delimBracketL,
+    delimBracketR,
+    delimParenL,
+    delimParenR,
+    delimRule,
+    delimSemicolon,
+    kwAnd,
+    kwDoubleArrowR,
+    kwExclamation,
+    kwIndex,
+    kwMapsTo,
+    kwNeq,
+    kwNeqSymbol,
+    kwNockmaLogicAnd,
+    kwReplace,
+    kwStar,
+    kwStorage,
+    kwSuc,
+  )
+import Juvix.Prelude
+
+data TermSymbol = TermSymbol
+  { _termSymbolLetter :: Char,
+    _termSymbolSubscript :: Maybe Natural,
+    _termSymbolPrimes :: Natural
+  }
+  deriving stock (Eq, Ord, Generic, Lift)
+
+instance Hashable TermSymbol
+
+data PathSymbol = PathP
+  deriving stock (Lift)
+
+data Symbol
+  = SymbolTerm TermSymbol
+  | SymbolPath PathSymbol
+  | SymbolStack
+  deriving stock (Lift)
+
+data Atom
+  = AtomSymbol Symbol
+  | AtomOperator NockOp
+  | AtomStorage
+  | AtomNotation Notation
+  | AtomZero
+  | AtomOne
+  deriving stock (Lift)
+
+-- | Syntax: notationName(arg1; .. ; argn), where `notationName` depends on each case
+data Notation
+  = NotationReplace Replace
+  | NotationIndex IndexAt
+  | NotationSuccessor Successor
+  deriving stock (Lift)
+
+-- | Syntax: neq(_neqLhs; _neqRhs)
+data Neq = Neq
+  { _neqLhs :: Term,
+    _neqRhs :: Term
+  }
+  deriving stock (Lift)
+
+-- | Syntax: succ(_successor)
+newtype Successor = Successor
+  { _successor :: Term
+  }
+  deriving stock (Lift)
+
+-- | Syntax: index(_indexAtBase; _indexAtIndex)
+data IndexAt = IndexAt
+  { _indexAtBase :: Term,
+    _indexAtPath :: Term
+  }
+  deriving stock (Lift)
+
+-- | Syntax: replace (_replaceBase; _replacePath;  _replaceBy)
+data Replace = Replace
+  { _replaceBase :: Term,
+    _replacePath :: PathSymbol,
+    _replaceBy :: Term
+  }
+  deriving stock (Lift)
+
+data Term
+  = TermAtom Atom
+  | TermCell Cell
+  deriving stock (Lift)
+
+-- | Syntax: [l r]
+data Cell = Cell
+  { _cellLhs :: Term,
+    _cellRhs :: Term
+  }
+  deriving stock (Lift)
+
+data Relation
+  = RelationEval EvalRelation
+  | RelationNeq Neq
+  deriving stock (Lift)
+
+-- | Syntax: _evalContext => _evalRhs
+data EvalRelation = EvalRelation
+  { _evalContext :: Context,
+    _evalRhs :: Term
+  }
+  deriving stock (Lift)
+
+-- | Syntax: _contextLhs * _contextRhs
+data Context = Context
+  { _contextLhs :: Term,
+    _contextRhs :: Term
+  }
+  deriving stock (Lift)
+
+-- | Syntax:
+-- rel_1 && .. && rel_n
+-- ---
+-- rel
+data Rule = Rule
+  { _ruleConditions :: [Relation],
+    _rulePost :: EvalRelation
+  }
+  deriving stock (Lift)
+
+-- | Syntax:
+-- rule_1
+-- and
+-- ..
+-- and
+-- rule_n
+newtype Rules = Rules
+  { _rules :: NonEmpty Rule
+  }
+  deriving stock (Lift)
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser.hs
new file mode 100644
index 0000000000..c1c1850457
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser.hs
@@ -0,0 +1,8 @@
+module Juvix.Compiler.Nockma.Highlight.Doc.Parser
+  ( module Juvix.Compiler.Nockma.Highlight.Doc.Parser.Base,
+    module Juvix.Compiler.Nockma.Highlight.Doc.Parser.QQ,
+  )
+where
+
+import Juvix.Compiler.Nockma.Highlight.Doc.Parser.Base
+import Juvix.Compiler.Nockma.Highlight.Doc.Parser.QQ
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/Base.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/Base.hs
new file mode 100644
index 0000000000..d2a9aa58e6
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/Base.hs
@@ -0,0 +1,190 @@
+module Juvix.Compiler.Nockma.Highlight.Doc.Parser.Base where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Compiler.Nockma.Language (atomOps)
+import Juvix.Parser.Error.Base
+import Juvix.Parser.Lexer
+import Juvix.Prelude
+import Juvix.Prelude.Parsing as P
+import Text.Megaparsec.Char.Lexer (decimal)
+
+type Parse a = Parsec Void Text a
+
+parseRules :: FilePath -> Text -> Either MegaparsecError Rules
+parseRules fp = mapLeft MegaparsecError . runParser (top pRules) fp
+
+lexeme :: Parse a -> Parse a
+lexeme m = m <* whiteSpace
+
+top :: Parse a -> Parse a
+top p = whiteSpace >> p <* eof
+
+pTermSymbol :: Parse TermSymbol
+pTermSymbol = lexeme $ do
+  l <- satisfy isLetter
+  subscript <- optional decimal
+  ps <- length <$> P.many (chunk "'")
+  return
+    TermSymbol
+      { _termSymbolLetter = l,
+        _termSymbolSubscript = subscript,
+        _termSymbolPrimes = fromIntegral ps
+      }
+
+isStackSymbol :: Char -> Bool
+isStackSymbol = (== 's') . toLower
+
+pPathSymbol :: Parse PathSymbol
+pPathSymbol =
+  lexeme $
+    chunk "p" $> PathP
+
+pStack :: Parse Symbol
+pStack = lexeme $ satisfy isStackSymbol $> SymbolStack
+
+pNockOp :: Parse NockOp
+pNockOp =
+  lexeme $
+    choice
+      [ chunk (opName <> " ") $> op
+        | (opName, op) <- HashMap.toList atomOps
+      ]
+
+kw :: Keyword -> Parse ()
+kw k =
+  lexeme
+    . void
+    . choice
+    . map chunk
+    $ (k ^. keywordAscii)
+      : maybeToList (k ^. keywordUnicode)
+
+delims :: Keyword -> Keyword -> Parse a -> Parse a
+delims l r p = do
+  kw l
+  p <* kw r
+
+brackets :: Parse a -> Parse a
+brackets = delims delimBracketL delimBracketR
+
+parens :: Parse a -> Parse a
+parens = delims delimParenL delimParenR
+
+pReplace :: Parse Replace
+pReplace = do
+  kw kwReplace
+  parens $ do
+    _replaceBase <- pTerm
+    kw delimSemicolon
+    _replacePath <- pPathSymbol
+    kw delimSemicolon
+    _replaceBy <- pTerm
+    optional (kw delimSemicolon)
+    return Replace {..}
+
+pIndexAt :: Parse IndexAt
+pIndexAt = do
+  kw kwIndex
+  parens $ do
+    _indexAtBase <- pTerm
+    kw delimSemicolon
+    _indexAtPath <- pTerm
+    return IndexAt {..}
+
+pSuccessor :: Parse Successor
+pSuccessor = do
+  kw kwSuc
+  t <- parens pTerm
+  return
+    Successor
+      { _successor = t
+      }
+
+pZero :: Parse ()
+pZero = lexeme . void $ chunk "0"
+
+pStorage :: Parse ()
+pStorage = kw kwStorage
+
+pOne :: Parse ()
+pOne = lexeme . void $ chunk "1"
+
+pAtom :: Parse Atom
+pAtom =
+  choice
+    [ AtomStorage <$ pStorage,
+      AtomOperator <$> pNockOp,
+      AtomNotation <$> pNotation,
+      AtomZero <$ pZero,
+      AtomOne <$ pOne,
+      AtomSymbol <$> pSymbol
+    ]
+
+pSymbol :: Parse Symbol
+pSymbol =
+  choice
+    [ SymbolStack <$ pStack,
+      SymbolPath <$> pPathSymbol,
+      SymbolTerm <$> pTermSymbol
+    ]
+
+pNotation :: Parse Notation
+pNotation =
+  choice
+    [ NotationIndex <$> pIndexAt,
+      NotationReplace <$> pReplace,
+      NotationSuccessor <$> pSuccessor
+    ]
+
+pNeq :: Parse Neq
+pNeq = do
+  kw kwNeq
+  parens $ do
+    _neqLhs <- pTerm
+    kw delimSemicolon
+    _neqRhs <- pTerm
+    optional (kw delimSemicolon)
+    return Neq {..}
+
+pCell :: Parse Cell
+pCell = brackets $ do
+  _cellLhs <- pTerm
+  _cellRhs <- pTerm
+  return Cell {..}
+
+pTerm :: Parse Term
+pTerm =
+  TermCell <$> pCell
+    <|> TermAtom <$> pAtom
+
+pContext :: Parse Context
+pContext = do
+  _contextLhs <- pTerm
+  kw kwStar
+  _contextRhs <- pTerm
+  return Context {..}
+
+pEvalRelation :: Parse EvalRelation
+pEvalRelation = do
+  _evalContext <- pContext
+  kw kwDoubleArrowR
+  _evalRhs <- pTerm
+  return EvalRelation {..}
+
+pRelation :: Parse Relation
+pRelation =
+  choice
+    [ RelationNeq <$> pNeq,
+      RelationEval <$> pEvalRelation
+    ]
+
+pRule :: Parse Rule
+pRule = do
+  _ruleConditions <- sepEndBy pRelation (kw kwNockmaLogicAnd)
+  kw delimRule
+  _rulePost <- pEvalRelation
+  return Rule {..}
+
+pRules :: Parse Rules
+pRules = Rules <$> sepEndBy1 pRule (kw kwAnd)
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/QQ.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/QQ.hs
new file mode 100644
index 0000000000..4384c509de
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc/Parser/QQ.hs
@@ -0,0 +1,24 @@
+module Juvix.Compiler.Nockma.Highlight.Doc.Parser.QQ where
+
+import Control.Monad.Fail qualified as M
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Compiler.Nockma.Highlight.Doc.Parser.Base
+import Juvix.Parser.Error (fromMegaParsecError)
+import Juvix.Prelude
+import Language.Haskell.TH.Quote
+import Language.Haskell.TH.Syntax
+
+rules :: QuasiQuoter
+rules =
+  QuasiQuoter
+    { quotePat = err,
+      quoteDec = err,
+      quoteType = err,
+      quoteExp = lift . qqRules
+    }
+  where
+    err :: String -> Q a
+    err = const (M.fail "QuasiQuote `rules` can only be used as an expression")
+
+    qqRules :: String -> Rules
+    qqRules = fromMegaParsecError . parseRules "<quasiquote>" . pack
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Doc/Pretty.hs b/src/Juvix/Compiler/Nockma/Highlight/Doc/Pretty.hs
new file mode 100644
index 0000000000..cb5f7c2f78
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Doc/Pretty.hs
@@ -0,0 +1,214 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Avoid restricted flags" #-}
+module Juvix.Compiler.Nockma.Highlight.Doc.Pretty () where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as Text
+import Juvix.Compiler.Nockma.Highlight.Doc.Base
+import Juvix.Data.CodeAnn
+import Juvix.Prelude
+
+data ColorCounter :: Effect where
+  GetSymbolColor :: Symbol -> ColorCounter m CodeAnn
+
+makeSem ''ColorCounter
+
+getTermSymbolColor :: (Members '[ColorCounter] r) => TermSymbol -> Sem r CodeAnn
+getTermSymbolColor = getSymbolColor . SymbolTerm
+
+getPathColor :: (Members '[ColorCounter] r) => PathSymbol -> Sem r CodeAnn
+getPathColor = getSymbolColor . SymbolPath
+
+getStackColor :: (Members '[ColorCounter] r) => Sem r CodeAnn
+getStackColor = getSymbolColor SymbolStack
+
+runColorCounter :: Sem (ColorCounter ': r) a -> Sem r a
+runColorCounter = reinterpret (evalState (mempty :: HashMap TermSymbol CodeAnn)) $ \case
+  GetSymbolColor s -> case s of
+    SymbolStack -> return (AnnKind KNameLocal)
+    SymbolPath p -> case p of
+      PathP -> return AnnLiteralString
+    SymbolTerm sym -> do
+      tbl <- get @(HashMap TermSymbol CodeAnn)
+      let m = length tbl
+      case tbl ^. at sym of
+        Just c -> return c
+        Nothing -> do
+          let color = colorAt m
+          modify (HashMap.insert sym color)
+          return color
+      where
+        colorAt :: Int -> CodeAnn
+        colorAt i = colors !! (i `mod` n)
+
+        n :: Int
+        n
+          | notNull colors = length colors
+          | otherwise = impossibleError "there must be at least one color"
+
+        colors :: [CodeAnn]
+        colors =
+          ( AnnKind
+              <$> [ KNameConstructor,
+                    KNameInductive,
+                    KNameAxiom,
+                    KNameTopModule
+                  ]
+          )
+            ++ [ AnnJudoc,
+                 AnnPragma,
+                 AnnComment
+               ]
+
+type PP a = a -> Sem '[ColorCounter] (Doc CodeAnn)
+
+instance PrettyCodeAnn Rules where
+  ppCodeAnn = run . runColorCounter . ppRules
+
+ppNotation :: PP Notation
+ppNotation = \case
+  NotationReplace r -> ppReplace r
+  NotationIndex i -> ppIndexAt i
+  NotationSuccessor i -> ppSuccessor i
+
+ppAtom :: PP Atom
+ppAtom = \case
+  AtomSymbol s -> ppSymbol s
+  AtomOperator n -> ppOperator n
+  AtomNotation n -> ppNotation n
+  AtomStorage -> return (ppCodeAnn kwStorage)
+  AtomZero -> return (annotate AnnKeyword "0")
+  AtomOne -> return (annotate AnnKeyword "1")
+
+ppSymbol :: PP Symbol
+ppSymbol = \case
+  SymbolStack -> ppStack
+  SymbolTerm t -> ppTermSymbol t
+  SymbolPath p -> ppPathSymbol p
+
+ppTermSymbol :: PP TermSymbol
+ppTermSymbol s@TermSymbol {..} = do
+  c <- getTermSymbolColor s
+  let primes = Text.replicate (fromIntegral _termSymbolPrimes) "'"
+      sym =
+        Text.singleton _termSymbolLetter
+          <>? (unicodeSubscript <$> _termSymbolSubscript)
+          <> primes
+  return
+    . annotate c
+    . pretty
+    $ sym
+
+ppOperator :: PP NockOp
+ppOperator = return . ppCodeAnn
+
+ppReplace :: PP Replace
+ppReplace Replace {..} = do
+  b' <- ppTerm _replaceBase
+  ix' <- ppPathSymbol _replacePath
+  by' <- ppTerm _replaceBy
+  return $
+    b'
+      <> ppCodeAnn delimBraceL
+      <> ix'
+      <+> ppCodeAnn kwMapsTo
+      <+> by'
+        <> ppCodeAnn delimBraceR
+
+ppPathSymbol :: PP PathSymbol
+ppPathSymbol = \case
+  p@PathP -> do
+    c <- getPathColor p
+    return (annotate c "p")
+
+ppNeq :: PP Neq
+ppNeq Neq {..} = do
+  l' <- ppTerm _neqLhs
+  r' <- ppTerm _neqRhs
+  return $
+    l' <+> ppCodeAnn kwNeqSymbol <+> r'
+
+ppIndexAt :: PP IndexAt
+ppIndexAt IndexAt {..} = do
+  b' <- ppTerm _indexAtBase
+  ix' <- ppTerm _indexAtPath
+  return $
+    b' <+> ppCodeAnn kwExclamation <+> ix'
+
+ppStack :: (Members '[ColorCounter] r) => Sem r (Doc CodeAnn)
+ppStack = do
+  c <- getStackColor
+  return (annotate c "S")
+
+ppSuccessor :: PP Successor
+ppSuccessor Successor {..} = do
+  t' <- ppTerm _successor
+  return $
+    t' <+> "+" <+> "1"
+
+ppCell :: PP Cell
+ppCell Cell {..} = do
+  l <- ppTerm _cellLhs
+  r <- ppTerm _cellRhs
+  return $
+    ppCodeAnn delimBracketL
+      <> l
+      <+> r
+        <> ppCodeAnn delimBracketR
+
+ppTerm :: PP Term
+ppTerm = \case
+  TermAtom a -> ppAtom a
+  TermCell a -> ppCell a
+
+ppEvalRelation :: PP EvalRelation
+ppEvalRelation EvalRelation {..} = do
+  ctx' <- ppContext _evalContext
+  r' <- ppTerm _evalRhs
+  return $
+    ctx' <+> ppCodeAnn kwDoubleArrowR <+> r'
+
+ppContext :: PP Context
+ppContext Context {..} = do
+  l <- ppTerm _contextLhs
+  r <- ppTerm _contextRhs
+  return $
+    l <+> ppCodeAnn kwStar <+> r
+
+ppRelation :: PP Relation
+ppRelation = \case
+  RelationEval r -> ppEvalRelation r
+  RelationNeq n -> ppNeq n
+
+ppRule :: PP Rule
+ppRule Rule {..} = do
+  let sep_ r1 r2 = r1 <+> (" " :: Doc CodeAnn) <+> r2
+  conds' <- concatWith sep_ <$> mapM ppRelation _ruleConditions
+  post' <- ppEvalRelation _rulePost
+  let n1 = Text.length (toPlainText conds')
+      n2 = Text.length (toPlainText post')
+      hrule = pretty (Text.replicate (max n1 (max n2 3)) "─")
+  return $
+    conds'
+      <> hardline
+      <> hrule
+      <> hardline
+      <> post'
+
+ppRules :: PP Rules
+ppRules Rules {..} = do
+  rules' <- mapM ppRule _rules
+  return $
+    concatWith
+      ( \r1 r2 ->
+          r1
+            <> hardline
+            <> hardline
+            <> ppCodeAnn kwAnd
+            <> hardline
+            <> hardline
+            <> r2
+      )
+      rules'
diff --git a/src/Juvix/Compiler/Nockma/Highlight/Input.hs b/src/Juvix/Compiler/Nockma/Highlight/Input.hs
new file mode 100644
index 0000000000..2c53d70867
--- /dev/null
+++ b/src/Juvix/Compiler/Nockma/Highlight/Input.hs
@@ -0,0 +1,55 @@
+module Juvix.Compiler.Nockma.Highlight.Input where
+
+import Juvix.Compiler.Nockma.Language hiding (Path)
+import Juvix.Compiler.Nockma.Language qualified as Nockma
+import Juvix.Data.CodeAnn
+import Juvix.Prelude
+
+data HighlightInput = HighlightInput
+  { _highlightSemanticItems :: [SemanticItem],
+    _highlightNockOps :: [WithLoc NockOp],
+    _highlightPaths :: [WithLoc Nockma.Path],
+    _highlightErrors :: [Interval]
+  }
+
+makeLenses ''HighlightInput
+
+emptyHighlightInput :: HighlightInput
+emptyHighlightInput =
+  HighlightInput
+    { _highlightSemanticItems = [],
+      _highlightNockOps = [],
+      _highlightPaths = [],
+      _highlightErrors = []
+    }
+
+filterInput :: Path Abs File -> HighlightInput -> HighlightInput
+filterInput absPth HighlightInput {..} =
+  HighlightInput
+    { _highlightSemanticItems = filterByLoc absPth _highlightSemanticItems,
+      _highlightNockOps = filterByLoc absPth _highlightNockOps,
+      _highlightPaths = filterByLoc absPth _highlightPaths,
+      _highlightErrors = _highlightErrors
+    }
+
+data HighlightBuilder :: Effect where
+  HighlightItem :: SemanticItem -> HighlightBuilder m ()
+  HighlightNockOp :: WithLoc NockOp -> HighlightBuilder m ()
+  HighlightPath :: WithLoc Nockma.Path -> HighlightBuilder m ()
+
+makeSem ''HighlightBuilder
+
+ignoreHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r a
+ignoreHighlightBuilder = interpret $ \case
+  HighlightItem {} -> return ()
+  HighlightNockOp {} -> return ()
+  HighlightPath {} -> return ()
+
+execHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput)
+execHighlightBuilder = fmap fst . runHighlightBuilder
+
+runHighlightBuilder :: Sem (HighlightBuilder ': r) a -> Sem r (HighlightInput, a)
+runHighlightBuilder = reinterpret (runState emptyHighlightInput) $ \case
+  HighlightItem i -> modify (over highlightSemanticItems (i :))
+  HighlightNockOp i -> modify (over highlightNockOps (i :))
+  HighlightPath i -> modify (over highlightPaths (i :))
diff --git a/src/Juvix/Compiler/Nockma/Language.hs b/src/Juvix/Compiler/Nockma/Language.hs
index 5da93d521e..3ef64c4eda 100644
--- a/src/Juvix/Compiler/Nockma/Language.hs
+++ b/src/Juvix/Compiler/Nockma/Language.hs
@@ -144,7 +144,7 @@ data NockOp
   | OpReplace
   | OpHint
   | OpScry
-  deriving stock (Bounded, Enum, Eq, Generic)
+  deriving stock (Show, Bounded, Enum, Eq, Generic, Lift)
 
 instance Hashable NockOp
 
@@ -164,6 +164,13 @@ instance Pretty NockOp where
     OpHint -> "hint"
     OpScry -> "scry"
 
+instance HasNameKind NockOp where
+  getNameKind = const KNameFunction
+  getNameKindPretty = const KNameFunction
+
+instance PrettyCodeAnn NockOp where
+  ppCodeAnn o = annotate (AnnKind (getNameKind o)) . pretty $ o
+
 data NockHint = NockHintPuts
   deriving stock (Show, Eq, Enum, Bounded)
 
diff --git a/src/Juvix/Compiler/Nockma/Language/Path.hs b/src/Juvix/Compiler/Nockma/Language/Path.hs
index 925e32bf23..895f4e8095 100644
--- a/src/Juvix/Compiler/Nockma/Language/Path.hs
+++ b/src/Juvix/Compiler/Nockma/Language/Path.hs
@@ -1,11 +1,18 @@
 module Juvix.Compiler.Nockma.Language.Path where
 
+import Juvix.Data.CodeAnn
 import Juvix.Prelude hiding (Atom, Path)
+import Prelude (show)
 
 data Direction
   = L
   | R
-  deriving stock (Show, Eq)
+  deriving stock (Eq, Bounded, Enum)
+
+instance Show Direction where
+  show = \case
+    L -> "L"
+    R -> "R"
 
 type Path = [Direction]
 
@@ -50,3 +57,13 @@ instance Semigroup EncodedPath where
 
 instance Monoid EncodedPath where
   mempty = encodePath []
+
+instance PrettyCodeAnn Path where
+  ppCodeAnn = \case
+    [] -> annotate (AnnKind KNameInductive) "S"
+    ds -> mconcatMap ppCodeAnn ds
+
+instance PrettyCodeAnn Direction where
+  ppCodeAnn d = annotate (AnnKind KNameInductive) $ case d of
+    L -> "L"
+    R -> "R"
diff --git a/src/Juvix/Compiler/Nockma/Pretty/Base.hs b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
index 62bc7ee1a8..c015d04a3d 100644
--- a/src/Juvix/Compiler/Nockma/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Pretty/Base.hs
@@ -67,15 +67,10 @@ instance PrettyCode Natural where
   ppCode = return . pretty
 
 instance PrettyCode Path where
-  ppCode = \case
-    [] -> return "S"
-    ds -> mconcatMapM ppCode ds
+  ppCode = return . ppCodeAnn
 
 instance PrettyCode Direction where
-  ppCode =
-    return . \case
-      L -> annotate (AnnKind KNameAxiom) "L"
-      R -> annotate AnnKeyword "R"
+  ppCode = return . ppCodeAnn
 
 instance PrettyCode NockOp where
   ppCode =
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
index c2dc3d9f12..917919fa97 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromSource/Base.hs
@@ -1,12 +1,17 @@
-module Juvix.Compiler.Nockma.Translation.FromSource.Base where
+module Juvix.Compiler.Nockma.Translation.FromSource.Base
+  ( module Juvix.Compiler.Nockma.Translation.FromSource.Base,
+    module Juvix.Compiler.Nockma.Highlight.Input,
+  )
+where
 
 import Data.HashMap.Internal.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
 import Juvix.Compiler.Nockma.Encoding.ByteString (textToNatural)
 import Juvix.Compiler.Nockma.Encoding.Cue qualified as Cue
+import Juvix.Compiler.Nockma.Highlight.Input
 import Juvix.Compiler.Nockma.Language
-import Juvix.Data.CodeAnn
+import Juvix.Data.CodeAnn hiding (delimiter, keyword)
 import Juvix.Extra.Paths
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Parser.Error
@@ -17,7 +22,9 @@ import Juvix.Prelude.Parsing hiding (runParser)
 import Text.Megaparsec qualified as P
 import Text.Megaparsec.Char.Lexer qualified as L
 
-type Parser = Parsec Void Text
+type ParserSem = '[HighlightBuilder]
+
+type Parser = ParsecT Void Text (Sem '[HighlightBuilder])
 
 parseText :: Text -> Either MegaparsecError (Term Natural)
 parseText = runParser noFile
@@ -33,7 +40,7 @@ cueJammedFileOrPretty ::
   Prelude.Path Abs File ->
   Sem r (Term Natural)
 cueJammedFileOrPretty f
-  | f `hasExtensions` nockmaDebugFileExts = parseTermFile f
+  | f `hasExtensions` nockmaDebugFileExts = ignoreHighlightBuilder (parseTermFile f)
   | otherwise = cueJammedFile f
 
 -- | If the file ends in .debug.nockma it parses an annotated unjammed program. Otherwise
@@ -77,10 +84,11 @@ cueJammedFile fp = do
         loc :: Loc
         loc = mkInitialLoc fp
 
-parseTermFile :: (Members '[Files, Error JuvixError] r) => Prelude.Path Abs File -> Sem r (Term Natural)
+parseTermFile :: (Members '[Files, Error JuvixError, HighlightBuilder] r) => Prelude.Path Abs File -> Sem r (Term Natural)
 parseTermFile fp = do
   txt <- readFile' fp
-  either (throw . JuvixError) return (runParser fp txt)
+  mapError (JuvixError @MegaparsecError) $
+    runParserForSem term fp txt
 
 parseProgramFile :: (Members '[Files, Error JuvixError] r) => Prelude.Path Abs File -> Sem r (Program Natural)
 parseProgramFile fp = do
@@ -93,10 +101,20 @@ parseReplStatement = runParserFor replStatement noFile
 runParserProgram :: Prelude.Path Abs File -> Text -> Either MegaparsecError (Program Natural)
 runParserProgram = runParserFor program
 
+runParserForSem ::
+  (Members '[Error MegaparsecError, HighlightBuilder] r) =>
+  Parser a ->
+  Prelude.Path Abs File ->
+  Text ->
+  Sem r a
+runParserForSem p f txt = do
+  x <- inject (P.runParserT (spaceConsumer >> p <* eof) (toFilePath f) txt)
+  case x of
+    Left err -> throw (MegaparsecError err)
+    Right t -> return t
+
 runParserFor :: Parser a -> Prelude.Path Abs File -> Text -> Either MegaparsecError a
-runParserFor p f input_ = case P.runParser (spaceConsumer >> p <* eof) (toFilePath f) input_ of
-  Left err -> Left (MegaparsecError err)
-  Right t -> Right t
+runParserFor p f = run . ignoreHighlightBuilder . runError . runParserForSem p f
 
 runParser :: Prelude.Path Abs File -> Text -> Either MegaparsecError (Term Natural)
 runParser = runParserFor term
@@ -112,14 +130,34 @@ lexeme = L.lexeme spaceConsumer
 symbol :: Text -> Parser Text
 symbol = L.symbol spaceConsumer
 
+semanticSymbolBare :: CodeAnn -> Text -> Parser ()
+semanticSymbolBare t = semanticParser t . void . chunk
+
+semanticSymbol :: CodeAnn -> Text -> Parser ()
+semanticSymbol t = lexeme . semanticSymbolBare t
+
+semanticParserLoc :: forall a. CodeAnn -> Parser (WithLoc a) -> Parser (WithLoc a)
+semanticParserLoc t p = do
+  s :: WithLoc a <- p
+  lift (highlightItem (s $> t))
+  return s
+
+semanticParser :: forall a. CodeAnn -> Parser a -> Parser a
+semanticParser t p = (^. withLocParam) <$> semanticParserLoc t (withLoc p)
+
+delimiter :: Text -> Parser ()
+delimiter = semanticSymbol AnnDelimiter
+
 lsbracket :: Parser ()
-lsbracket = void (lexeme "[")
+lsbracket = delimiter "["
 
 rsbracket :: Parser ()
-rsbracket = void (lexeme "]")
+rsbracket = delimiter "]"
 
 stringLiteral :: Parser Text
-stringLiteral = lexeme (pack <$> (char '"' >> manyTill L.charLiteral (char '"')))
+stringLiteral =
+  semanticParser AnnLiteralString $
+    lexeme (pack <$> (char '"' >> manyTill L.charLiteral (char '"')))
 
 dottedNatural :: Parser Natural
 dottedNatural = lexeme $ do
@@ -135,7 +173,15 @@ dottedNatural = lexeme $ do
 
 atomOp :: Maybe Tag -> Parser (Atom Natural)
 atomOp mtag = do
-  WithLoc loc op' <- withLoc (choice [symbol opName $> op | (opName, op) <- HashMap.toList atomOps])
+  lop@(WithLoc loc op') <-
+    withLoc
+      ( choice
+          [ semanticSymbolBare (AnnKind (getNameKind op)) opName $> op
+            | (opName, op) <- HashMap.toList atomOps
+          ]
+      )
+  lift (highlightNockOp lop)
+  spaceConsumer
   let info =
         AtomInfo
           { _atomInfoHint = Just AtomHintOp,
@@ -155,19 +201,32 @@ atomPath mtag = do
           }
   return (Atom (serializePath path) info)
 
+keyword :: Text -> Parser ()
+keyword = semanticSymbol AnnKeyword
+
+constructorSymbol :: Text -> Parser ()
+constructorSymbol = semanticSymbol (AnnKind KNameConstructor)
+
+directionSymbol :: Text -> Parser ()
+directionSymbol = semanticSymbol (AnnKind KNameInductive)
+
 direction :: Parser Direction
-direction =
-  symbol "L" $> L
-    <|> symbol "R" $> R
+direction = choice [directionSymbol (show lr) $> lr | lr <- allElements :: [Direction]]
 
 pPath :: Parser Path
-pPath =
-  symbol "S" $> []
-    <|> NonEmpty.toList <$> some direction
+pPath = do
+  p <-
+    withLoc $
+      choice
+        [ directionSymbol "S" $> [],
+          NonEmpty.toList <$> some direction
+        ]
+  lift (highlightPath p)
+  return (p ^. withLocParam)
 
 atomNat :: Maybe Tag -> Parser (Atom Natural)
 atomNat mtag = do
-  WithLoc loc n <- withLoc dottedNatural
+  WithLoc loc n <- semanticParserLoc AnnLiteralInteger (withLoc dottedNatural)
   let info =
         AtomInfo
           { _atomInfoHint = Nothing,
@@ -179,8 +238,8 @@ atomNat mtag = do
 atomBool :: Parser (Atom Natural)
 atomBool =
   choice
-    [ symbol Str.true $> nockTrue,
-      symbol Str.false $> nockFalse
+    [ constructorSymbol Str.true $> nockTrue,
+      constructorSymbol Str.false $> nockFalse
     ]
 
 atomWithLoc :: Parser a -> Atom Natural -> Parser (Atom Natural)
@@ -189,14 +248,14 @@ atomWithLoc p n = do
   return (set atomLoc (Just loc) n)
 
 atomNil :: Parser (Atom Natural)
-atomNil = choice (map symbol [Str.nil, Str.functionsPlaceholder, Str.stdlibPlaceholder]) $> nockNil
+atomNil = choice (map constructorSymbol [Str.nil, Str.functionsPlaceholder, Str.stdlibPlaceholder]) $> nockNil
 
 atomVoid :: Parser (Atom Natural)
-atomVoid = symbol Str.void $> nockVoid
+atomVoid = constructorSymbol Str.void $> nockVoid
 
 atomStringLiteral :: Parser (Atom Natural)
 atomStringLiteral = do
-  WithLoc loc s <- withLoc stringLiteral
+  WithLoc loc s <- semanticParserLoc AnnLiteralString (withLoc stringLiteral)
   let info =
         AtomInfo
           { _atomInfoTag = Nothing,
@@ -207,9 +266,9 @@ atomStringLiteral = do
 
 atomNockHint :: Maybe Tag -> Parser (Atom Natural)
 atomNockHint mtag = do
-  symbol Str.percent
+  keyword Str.percent
   let hints :: [NockHint] = enumerate
-  val <- choice (map (\hnt -> symbol (nockHintName hnt) >> return (nockHintValue hnt)) hints)
+  val <- choice (map (\hnt -> keyword (nockHintName hnt) $> nockHintValue hnt) hints)
   return (Atom val emptyAtomInfo {_atomInfoTag = mtag})
 
 patom :: Parser (Atom Natural)
@@ -225,11 +284,11 @@ patom = do
     <|> try atomStringLiteral
 
 iden :: Parser Text
-iden = lexeme (takeWhile1P (Just "<iden>") (isAscii .&&. not . isWhiteSpace))
+iden = semanticParser AnnJudoc (lexeme (takeWhile1P (Just "<iden>") (isAscii .&&. not . isWhiteSpace)))
 
 pTag :: Parser Tag
 pTag = do
-  void (chunk Str.tagTag)
+  keyword Str.tagTag
   Tag <$> iden
 
 cell :: Parser (Cell Natural)
@@ -251,9 +310,9 @@ cell = do
   where
     anomaLibCall :: Parser (AnomaLibCall Natural)
     anomaLibCall = do
-      chunk Str.stdlibTag
+      keyword Str.stdlibTag
       f <- stdlibFun
-      chunk Str.argsTag
+      keyword Str.argsTag
       args <- term
       return
         AnomaLibCall
@@ -280,7 +339,7 @@ term =
 assig :: Parser (Assignment Natural)
 assig = do
   n <- name
-  symbol ":="
+  keyword ":="
   t <- term
   return
     Assignment
@@ -305,7 +364,7 @@ name = lexeme $ do
 withStack :: Parser (WithStack Natural)
 withStack = do
   st <- replTerm
-  symbol "/"
+  keyword "/"
   tm <- replTerm
   return
     WithStack
diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs
index dad143f1c7..6b79609a95 100644
--- a/src/Juvix/Data.hs
+++ b/src/Juvix/Data.hs
@@ -24,6 +24,7 @@ module Juvix.Data
     module Juvix.Data.TopModulePathKey,
     module Juvix.Data.Keyword,
     module Juvix.Data.Polarity,
+    module Juvix.Data.ParsedItem,
   )
 where
 
@@ -42,6 +43,7 @@ import Juvix.Data.Loc
 import Juvix.Data.Logger
 import Juvix.Data.NameId qualified
 import Juvix.Data.NumThreads
+import Juvix.Data.ParsedItem
 import Juvix.Data.Polarity
 import Juvix.Data.Pragmas
 import Juvix.Data.Processed
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index eda39034f6..f61b6680c3 100644
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@@ -28,6 +28,7 @@ data CodeAnn
   | AnnKeyword
   | AnnCode
   | AnnComment
+  | AnnPragma
   | AnnJudoc
   | AnnImportant
   | AnnDelimiter
@@ -37,6 +38,8 @@ data CodeAnn
   | AnnDef CodeAnnReference
   | AnnRef CodeAnnReference
 
+type SemanticItem = WithLoc CodeAnn
+
 instance HasNameKind CodeAnnReference where
   getNameKind = (^. codeAnnReferenceNameKindPretty)
   getNameKindPretty = (^. codeAnnReferenceNameKindPretty)
@@ -52,6 +55,7 @@ stylize a = case a of
   AnnCode -> bold
   AnnImportant -> bold
   AnnComment -> colorDull Cyan
+  AnnPragma -> colorDull Cyan
   AnnJudoc -> colorDull Cyan
   AnnDelimiter -> colorDull White
   AnnLiteralString -> colorDull Red
@@ -66,6 +70,9 @@ instance HasAnsiBackend (Doc CodeAnn) where
   toAnsiDoc = fmap stylize
   toAnsiStream = fmap stylize . layoutPretty defaultLayoutOptions
 
+instance PrettyCodeAnn Keyword where
+  ppCodeAnn = annotate AnnKeyword . pretty
+
 simpleErrorCodeAnn :: (PrettyCodeAnn msg) => msg -> SimpleError
 simpleErrorCodeAnn = SimpleError . mkAnsiText . ppCodeAnn
 
diff --git a/src/Juvix/Data/Emacs.hs b/src/Juvix/Data/Emacs.hs
deleted file mode 100644
index 9a5d023849..0000000000
--- a/src/Juvix/Data/Emacs.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module Juvix.Data.Emacs
-  ( module Juvix.Data.Emacs.Point,
-    module Juvix.Data.Emacs.SExp,
-  )
-where
-
-import Juvix.Data.Emacs.Point
-import Juvix.Data.Emacs.SExp
diff --git a/src/Juvix/Data/Emacs/SExp.hs b/src/Juvix/Data/Emacs/SExp.hs
deleted file mode 100644
index d798849da2..0000000000
--- a/src/Juvix/Data/Emacs/SExp.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-module Juvix.Data.Emacs.SExp where
-
-import Juvix.Prelude
-import Juvix.Prelude.Pretty
-
-class ToSExp a where
-  toSExp :: a -> SExp
-
-data SExp
-  = Symbol Text
-  | App [SExp]
-  | Pair SExp SExp
-  | Quote SExp
-  | Backquote SExp
-  | Int Word64
-  | String Text
-
-progn :: [SExp] -> SExp
-progn l = App (Symbol "progn" : l)
-
-mkList :: [SExp] -> SExp
-mkList = Quote . App
-
-renderSExp :: SExp -> Text
-renderSExp =
-  renderStrict
-    . layoutPretty defaultLayoutOptions
-    . pretty
-
-instance Pretty SExp where
-  pretty = \case
-    Symbol s -> pretty s
-    Int s -> pretty s
-    App l -> parens (sep (map pretty l))
-    Pair l r -> parens (pretty l <+> dot <+> pretty r)
-    Backquote l -> pretty '`' <> pretty l
-    Quote l -> pretty '\'' <> pretty l
-    String s -> dquotes (pretty s)
diff --git a/src/Juvix/Data/Error.hs b/src/Juvix/Data/Error.hs
index 7daf3499de..c643663c7e 100644
--- a/src/Juvix/Data/Error.hs
+++ b/src/Juvix/Data/Error.hs
@@ -7,6 +7,7 @@ module Juvix.Data.Error
 where
 
 import Juvix.Data.Error.GenericError
+import Juvix.Data.Loc
 import Juvix.Prelude.Base
 
 data JuvixError
@@ -15,5 +16,8 @@ data JuvixError
 instance ToGenericError JuvixError where
   genericError (JuvixError e) = genericError e
 
+instance HasLoc JuvixError where
+  getLoc = getLoc . run . runReader defaultGenericOptions . genericError
+
 fromJuvixError :: (Typeable a) => JuvixError -> Maybe a
 fromJuvixError (JuvixError e) = cast e
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index 0171f8e7c0..fca34d037f 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -13,6 +13,36 @@ kwAs = asciiKw Str.as
 kwBuiltin :: Keyword
 kwBuiltin = asciiKw Str.builtin
 
+kwSuc :: Keyword
+kwSuc = asciiKw Str.suc
+
+delimRule :: Keyword
+delimRule = mkDelim Str.nockmaRule
+
+kwNockmaLogicAnd :: Keyword
+kwNockmaLogicAnd = asciiKw Str.nockmaLogicAnd
+
+kwAnd :: Keyword
+kwAnd = asciiKw Str.and
+
+kwStorage :: Keyword
+kwStorage = asciiKw Str.storage
+
+kwReplace :: Keyword
+kwReplace = asciiKw Str.replace
+
+kwIndex :: Keyword
+kwIndex = asciiKw Str.index
+
+kwNeq :: Keyword
+kwNeq = asciiKw Str.neq
+
+kwNeqSymbol :: Keyword
+kwNeqSymbol = unicodeKw Str.neqSymbolAscii Str.neqSymbol
+
+kwDoubleArrowR :: Keyword
+kwDoubleArrowR = unicodeKw Str.doubleArrowRAscii Str.doubleArrowR
+
 kwBottom :: Keyword
 kwBottom = unicodeKw Str.bottomAscii Str.bottom
 
@@ -404,7 +434,7 @@ kwFun :: Keyword
 kwFun = asciiKw Str.fun_
 
 kwStar :: Keyword
-kwStar = asciiKw Str.mul
+kwStar = unicodeKw Str.starAscii Str.star
 
 kwTrue :: Keyword
 kwTrue = asciiKw Str.true_
@@ -430,11 +460,11 @@ kwDollar = asciiKw Str.dollar
 kwMutual :: Keyword
 kwMutual = asciiKw Str.mutual
 
-kwBracketL :: Keyword
-kwBracketL = asciiKw Str.bracketL
+delimBracketL :: Keyword
+delimBracketL = mkDelim Str.bracketL
 
-kwBracketR :: Keyword
-kwBracketR = asciiKw Str.bracketR
+delimBracketR :: Keyword
+delimBracketR = mkDelim Str.bracketR
 
 kwAp :: Keyword
 kwAp = asciiKw Str.ap
diff --git a/src/Juvix/Compiler/Concrete/Data/ParsedItem.hs b/src/Juvix/Data/ParsedItem.hs
similarity index 85%
rename from src/Juvix/Compiler/Concrete/Data/ParsedItem.hs
rename to src/Juvix/Data/ParsedItem.hs
index 02ce836a27..4c338a7440 100644
--- a/src/Juvix/Compiler/Concrete/Data/ParsedItem.hs
+++ b/src/Juvix/Data/ParsedItem.hs
@@ -1,6 +1,7 @@
-module Juvix.Compiler.Concrete.Data.ParsedItem where
+module Juvix.Data.ParsedItem where
 
-import Juvix.Prelude
+import Juvix.Data.Loc
+import Juvix.Prelude.Base
 
 data ParsedItem = ParsedItem
   { _parsedLoc :: Interval,
diff --git a/src/Juvix/Data/Emacs/Point.hs b/src/Juvix/Emacs/Point.hs
similarity index 98%
rename from src/Juvix/Data/Emacs/Point.hs
rename to src/Juvix/Emacs/Point.hs
index 4d0c47e9ef..afe418f8e8 100644
--- a/src/Juvix/Data/Emacs/Point.hs
+++ b/src/Juvix/Emacs/Point.hs
@@ -1,4 +1,4 @@
-module Juvix.Data.Emacs.Point
+module Juvix.Emacs.Point
   ( Point,
     unPoint,
     fromZeroBasedInt,
diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/Properties.hs b/src/Juvix/Emacs/Properties.hs
similarity index 79%
rename from src/Juvix/Compiler/Concrete/Data/Highlight/Properties.hs
rename to src/Juvix/Emacs/Properties.hs
index b5d88a9800..cf3e1f30f3 100644
--- a/src/Juvix/Compiler/Concrete/Data/Highlight/Properties.hs
+++ b/src/Juvix/Emacs/Properties.hs
@@ -1,14 +1,28 @@
-module Juvix.Compiler.Concrete.Data.Highlight.Properties where
+module Juvix.Emacs.Properties where
 
 import Data.Aeson (ToJSON)
 import Data.Aeson qualified as Aeson
 import Data.Aeson.TH
-import Juvix.Data.Emacs
+import Juvix.Emacs.Point
+import Juvix.Emacs.SExp
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude
 
+data PropertyId
+  = PropertyIdFace
+  | PropertyIdGoto
+  | PropertyIdInfo
+  | PropertyIdFormat
+
+propertyIdText :: PropertyId -> Text
+propertyIdText = \case
+  PropertyIdFace -> "face"
+  PropertyIdInfo -> "juvix-info"
+  PropertyIdGoto -> "juvix-goto"
+  PropertyIdFormat -> "juvix-format"
+
 data GenericProperty = GenericProperty
-  { _gpropProperty :: Text,
+  { _gpropProperty :: PropertyId,
     _gpropValue :: SExp
   }
 
@@ -65,7 +79,7 @@ instance ToJSON Face where
 data EmacsProperty
   = EPropertyGoto PropertyGoto
   | EPropertyFace PropertyFace
-  | EPropertyDoc PropertyDoc
+  | EPropertyInfo PropertyInfo
 
 type LocEmacsProperty = WithLoc EmacsProperty
 
@@ -78,15 +92,15 @@ newtype PropertyFace = PropertyFace
   { _faceFace :: Face
   }
 
-data PropertyDoc = PropertyDoc
-  { _docText :: Text,
-    _docSExp :: SExp
+data PropertyInfo = PropertyInfo
+  { _infoInfo :: SExp,
+    _infoInit :: SExp
   }
 
 data LocProperties = LocProperties
   { _propertiesGoto :: [WithLoc PropertyGoto],
     _propertiesFace :: [WithLoc PropertyFace],
-    _propertiesDoc :: [WithLoc PropertyDoc]
+    _propertiesInfo :: [WithLoc PropertyInfo]
   }
 
 data RawProperties = RawProperties
@@ -121,7 +135,7 @@ rawProperties LocProperties {..} =
   RawProperties
     { _rawPropertiesGoto = map (rawWithLoc rawGoto) _propertiesGoto,
       _rawPropertiesFace = map (rawWithLoc rawFace) _propertiesFace,
-      _rawPropertiesDoc = map (rawWithLoc rawType) _propertiesDoc
+      _rawPropertiesDoc = map (rawWithLoc rawType) _propertiesInfo
     }
   where
     rawInterval :: Interval -> RawInterval
@@ -137,8 +151,11 @@ rawProperties LocProperties {..} =
     rawWithLoc :: (a -> b) -> WithLoc a -> RawWithLoc b
     rawWithLoc f x = (rawInterval (getLoc x), f (x ^. withLocParam))
 
-    rawType :: PropertyDoc -> RawType
-    rawType PropertyDoc {..} = _docText
+    rawType :: PropertyInfo -> RawType
+    rawType PropertyInfo {..} = case _infoInfo of
+      Symbol s -> s
+      String s -> s
+      _ -> error "unsupported"
 
     rawFace :: PropertyFace -> RawFace
     rawFace PropertyFace {..} = _faceFace
@@ -153,7 +170,7 @@ rawProperties LocProperties {..} =
 instance IsProperty EmacsProperty where
   toProperties = \case
     EPropertyFace p -> toProperties p
-    EPropertyDoc p -> toProperties p
+    EPropertyInfo p -> toProperties p
     EPropertyGoto p -> toProperties p
 
 addGenericProperties :: WithRange (NonEmpty GenericProperty) -> SExp
@@ -166,7 +183,7 @@ addGenericProperties (WithRange i props) =
     propertyList = mkList (concat [[k, v] | (k, v) <- map mkItem (toList props)])
       where
         mkItem :: GenericProperty -> (SExp, SExp)
-        mkItem GenericProperty {..} = (Symbol _gpropProperty, _gpropValue)
+        mkItem GenericProperty {..} = (Symbol (propertyIdText _gpropProperty), _gpropValue)
 
 putProperty :: (IsProperty a) => WithRange a -> SExp
 putProperty = addGenericProperties . fmap toProperties
@@ -185,7 +202,7 @@ instance IsProperty PropertyFace where
   toProperties PropertyFace {..} =
     pure
       GenericProperty
-        { _gpropProperty = "face",
+        { _gpropProperty = PropertyIdFace,
           _gpropValue = toSExp _faceFace
         }
 
@@ -193,21 +210,21 @@ instance IsProperty PropertyGoto where
   toProperties PropertyGoto {..} =
     pure
       GenericProperty
-        { _gpropProperty = "juvix-goto",
+        { _gpropProperty = PropertyIdGoto,
           _gpropValue = gotoPair
         }
     where
       gotoPair = Pair (String (pack (toFilePath _gotoFile))) (Int (_gotoPos ^. locOffset . to (succ . fromIntegral)))
 
-instance IsProperty PropertyDoc where
-  toProperties PropertyDoc {..} =
+instance IsProperty PropertyInfo where
+  toProperties PropertyInfo {..} =
     GenericProperty
-      { _gpropProperty = "help-echo",
-        _gpropValue = String _docText
+      { _gpropProperty = PropertyIdInfo,
+        _gpropValue = _infoInfo
       }
       :| [ GenericProperty
-             { _gpropProperty = "juvix-format",
-               _gpropValue = _docSExp
+             { _gpropProperty = PropertyIdFormat,
+               _gpropValue = _infoInit
              }
          ]
 
@@ -216,5 +233,5 @@ instance ToSExp LocProperties where
     progn
       ( map putPropertyLoc _propertiesFace
           <> map putPropertyLoc _propertiesGoto
-          <> map putPropertyLoc _propertiesDoc
+          <> map putPropertyLoc _propertiesInfo
       )
diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs b/src/Juvix/Emacs/Render.hs
similarity index 87%
rename from src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs
rename to src/Juvix/Emacs/Render.hs
index b55498cdef..e53d22a5ed 100644
--- a/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs
+++ b/src/Juvix/Emacs/Render.hs
@@ -1,10 +1,14 @@
-module Juvix.Compiler.Concrete.Data.Highlight.RenderEmacs where
+module Juvix.Emacs.Render
+  ( renderEmacs,
+    nameKindFace,
+  )
+where
 
 import Data.Text qualified as Text
-import Juvix.Compiler.Concrete.Data.Highlight.Properties
-import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Data.CodeAnn
-import Juvix.Data.Emacs
+import Juvix.Emacs.Point
+import Juvix.Emacs.Properties
+import Juvix.Emacs.SExp
 import Juvix.Prelude
 
 nameKindFace :: NameKind -> Maybe Face
@@ -27,6 +31,7 @@ fromCodeAnn = \case
   AnnKeyword -> Just (EPropertyFace (PropertyFace FaceKeyword))
   AnnDelimiter -> Just (EPropertyFace (PropertyFace FaceDelimiter))
   AnnComment -> Just (EPropertyFace (PropertyFace FaceComment))
+  AnnPragma -> Just (EPropertyFace (PropertyFace FacePragma))
   AnnJudoc -> Just (EPropertyFace (PropertyFace FaceJudoc))
   AnnLiteralString -> Just (EPropertyFace (PropertyFace FaceString))
   AnnLiteralInteger -> Just (EPropertyFace (PropertyFace FaceNumber))
@@ -34,7 +39,6 @@ fromCodeAnn = \case
   AnnImportant -> Nothing
   AnnUnkindedSym -> Nothing
   AnnDef {} -> Nothing
-  -- TODO goto property
   AnnRef {} -> Nothing
 
 data RenderState = RenderState
@@ -46,9 +50,15 @@ data RenderState = RenderState
 
 makeLenses ''RenderState
 
-renderEmacs :: SimpleDocStream CodeAnn -> (Text, SExp)
+renderEmacs :: Doc CodeAnn -> (Text, SExp)
 renderEmacs s =
-  let r = run . execState iniRenderState . go . alterAnnotationsS fromCodeAnn $ s
+  let r =
+        run
+          . execState iniRenderState
+          . go
+          . alterAnnotationsS fromCodeAnn
+          . layoutPretty defaultLayoutOptions
+          $ s
    in (r ^. stateText, progn (map putProperty (r ^. stateProperties)))
   where
     iniRenderState =
diff --git a/src/Juvix/Emacs/SExp.hs b/src/Juvix/Emacs/SExp.hs
new file mode 100644
index 0000000000..e24d596cf6
--- /dev/null
+++ b/src/Juvix/Emacs/SExp.hs
@@ -0,0 +1,78 @@
+module Juvix.Emacs.SExp where
+
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+class ToSExp a where
+  toSExp :: a -> SExp
+
+data SExp
+  = Symbol Text
+  | App [SExp]
+  | Pair SExp SExp
+  | Quote SExp
+  | Backquote SExp
+  | Int Word64
+  | String Text
+
+nil :: SExp
+nil = Symbol "nil"
+
+progn :: [SExp] -> SExp
+progn l = App (Symbol "progn" : l)
+
+putHash :: Text -> SExp -> SExp -> SExp
+putHash tblName key val = App [(Symbol "puthash"), key, val, (Symbol tblName)]
+
+makeHashTable :: SExp
+makeHashTable = App [Symbol "make-hash-table"]
+
+setq :: Text -> SExp -> SExp
+setq varName val = App [Symbol "setq", Symbol varName, val]
+
+mkHashTable :: Text -> [(SExp, SExp)] -> SExp
+mkHashTable tblName items =
+  progn $
+    setq tblName makeHashTable
+      : [putHash tblName key val | (key, val) <- items]
+
+withLocalHashTable :: Text -> [(SExp, SExp)] -> SExp -> SExp
+withLocalHashTable tblName items body =
+  let1
+    (tblName, makeHashTable)
+    . progn
+    $ [putHash tblName key val | (key, val) <- items]
+      ++ [body]
+
+let_ :: [(Text, SExp)] -> SExp -> SExp
+let_ items body =
+  App
+    [ Symbol "let",
+      App [App [(Symbol x), xdef] | (x, xdef) <- items],
+      body
+    ]
+
+let1 :: (Text, SExp) -> SExp -> SExp
+let1 (x, xdef) body = let_ [(x, xdef)] body
+
+mkList :: [SExp] -> SExp
+mkList = Quote . App
+
+instance HasTextBackend SExp where
+  toTextDoc = pretty
+
+renderSExp :: SExp -> Text
+renderSExp =
+  renderStrict
+    . layoutPretty defaultLayoutOptions
+    . pretty
+
+instance Pretty SExp where
+  pretty = \case
+    Symbol s -> pretty s
+    Int s -> pretty s
+    App l -> parens (sep (map pretty l))
+    Pair l r -> parens (pretty l <+> dot <+> pretty r)
+    Backquote l -> pretty '`' <> pretty l
+    Quote l -> pretty '\'' <> pretty l
+    String s -> dquotes (pretty s)
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index 96602606f5..95883bd3ce 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -1189,3 +1189,42 @@ packageBase = "package-base"
 
 rustReturn :: (IsString s) => s
 rustReturn = "return"
+
+starAscii :: (IsString s) => s
+starAscii = "*"
+
+star :: (IsString s) => s
+star = "⋆"
+
+doubleArrowRAscii :: (IsString s) => s
+doubleArrowRAscii = "=>"
+
+doubleArrowR :: (IsString s) => s
+doubleArrowR = "⇒"
+
+index :: (IsString s) => s
+index = "index"
+
+replace :: (IsString s) => s
+replace = "replace"
+
+storage :: (IsString s) => s
+storage = "storage"
+
+neqSymbol :: (IsString s) => s
+neqSymbol = "≠"
+
+neq :: (IsString s) => s
+neq = "neq"
+
+neqSymbolAscii :: (IsString s) => s
+neqSymbolAscii = "/="
+
+nockmaRule :: (IsString s) => s
+nockmaRule = "---"
+
+nockmaLogicAnd :: (IsString s) => s
+nockmaLogicAnd = "&&"
+
+and :: (IsString s) => s
+and = "and"
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index 518f96c995..711ec89608 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -196,7 +196,7 @@ kw' k@Keyword {..} = P.label (unpack _keywordAscii) (reserved <|> normal)
       (w, i) <- interval morpheme
       case keywordMatch k w of
         Just u -> return (KeywordRef k i u)
-        Nothing -> failure Nothing (Set.singleton (Label (fromJust $ nonEmpty $ unpack _keywordAscii)))
+        Nothing -> failure Nothing (Set.singleton (Label (nonEmpty' $ unpack _keywordAscii)))
 
 rawIdentifier' :: (Char -> Bool) -> HashSet Text -> ParsecS r Text
 rawIdentifier' excludedTailChar allKeywords = label "<identifier>" $ P.try $ do
diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs
index ff1083a39a..f47ec946db 100644
--- a/src/Juvix/Prelude/Base/Foundation.hs
+++ b/src/Juvix/Prelude/Base/Foundation.hs
@@ -64,6 +64,7 @@ module Juvix.Prelude.Base.Foundation
     module Text.Read,
     module Control.Monad.Catch,
     module Control.Monad.Zip,
+    module Data.String.Interpolate,
     Data,
     Text,
     pack,
@@ -177,6 +178,7 @@ import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances)
 import Data.Stream (Stream)
 import Data.String
+import Data.String.Interpolate (__i)
 import Data.Text (Text, pack, strip, unpack)
 import Data.Text qualified as Text
 import Data.Text.Encoding
@@ -813,3 +815,20 @@ mappendField t1 t2 = appendFieldWith t1 t2 (<>)
 
 appendFieldWith :: t -> t -> (f -> f -> f) -> Lens' t f -> f
 appendFieldWith t1 t2 joinfun l = joinfun (t1 ^. l) (t2 ^. l)
+
+unicodeSubscript :: Natural -> Text
+unicodeSubscript = pack . map toSubscript . show
+  where
+    toSubscript :: Char -> Char
+    toSubscript = \case
+      '0' -> '₀'
+      '1' -> '₁'
+      '2' -> '₂'
+      '3' -> '₃'
+      '4' -> '₄'
+      '5' -> '₅'
+      '6' -> '₆'
+      '7' -> '₇'
+      '8' -> '₈'
+      '9' -> '₉'
+      _ -> impossible