diff --git a/lakefile.lean b/lakefile.lean
index cc75f68..e42d4a8 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,13 +4,13 @@ open Lake DSL
 package «subverso» where
   -- add package configuration options here
 
-lean_lib SubversoHighlighting where
+lean_lib SubVersoHighlighting where
   srcDir := "src/highlighting"
-  roots := #[`Subverso.Highlighting]
+  roots := #[`SubVerso.Highlighting]
 
-lean_lib SubversoExamples where
+lean_lib SubVersoExamples where
   srcDir := "src/examples"
-  roots := #[`Subverso.Examples]
+  roots := #[`SubVerso.Examples]
 
 @[default_target]
 lean_exe «subverso-tests» where
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
new file mode 100644
index 0000000..1d38f85
--- /dev/null
+++ b/src/examples/SubVerso/Examples.lean
@@ -0,0 +1,148 @@
+import SubVerso.Highlighting
+import SubVerso.Examples.Env
+import Lean.Environment
+
+namespace SubVerso.Examples
+
+open SubVerso Highlighting
+
+open Lean Elab Command Term
+
+scoped syntax "%ex" "{" ident (" : " term)? "}" "{" term "}" : term
+scoped syntax "%ex" "{" ident "}" "{" tactic "}" : tactic
+scoped syntax "%ex" "{" ident "}" "{" doElem "}" : doElem
+
+
+class MonadMessageState (m : Type → Type v) where
+  getMessages : m MessageLog
+  setMessages : MessageLog → m Unit
+
+instance : MonadMessageState TermElabM where
+  getMessages := do return (← getThe Core.State).messages
+  setMessages msgs := modifyThe Core.State ({· with messages := msgs})
+
+instance : MonadMessageState CommandElabM where
+  getMessages := do return (← get).messages
+  setMessages msgs := modify ({· with messages := msgs})
+
+open MonadMessageState in
+def savingNewMessages [Monad m] [MonadFinally m] [MonadMessageState m]
+    (act : m α) : m (α × MessageLog) := do
+  let startMessages ← getMessages
+  let mut endMessages := .empty
+  setMessages .empty
+  let res ← try
+    let res ← act
+    endMessages ← getMessages
+    pure res
+  finally
+    setMessages (startMessages ++ endMessages)
+  pure (res, endMessages)
+
+scoped syntax "%example" ident command command* "%end" : command
+
+example : TermElabM Unit := logError "foo"
+
+partial def extractExamples (stx : Syntax) : StateT (NameMap Syntax) Id Syntax := do
+  if let `(term|%ex { $n:ident }{ $tm:term }) := stx then
+    let next ← extractExamples tm
+    -- Save the erased version in case there's nested examples
+    modify fun st => st.insert n.getId next
+    pure next
+  else
+    match stx with
+    | .node info kind args => pure <| .node info kind (← args.mapM extractExamples)
+    | _ => pure stx
+
+elab_rules : command
+  | `(%example $name:ident $cmd $cmds* %end) => do
+    let allCommands := #[cmd] ++ cmds
+    let (allCommands, termExamples) := allCommands.mapM extractExamples .empty
+    let ((), newMessages) ← savingNewMessages (allCommands.forM elabCommand)
+    let trees ← getInfoTrees
+    let hl ← allCommands.mapM fun c => liftTermElabM (highlight c newMessages.toList.toArray trees)
+    let freshMsgs ← newMessages.toList.mapM fun m => do pure (m.severity, ← m.toString)
+    let .original leading startPos _ _ := allCommands[0]!.getHeadInfo
+      | throwErrorAt allCommands[0]! "Failed to get source position"
+    let .original _ _ trailing stopPos := allCommands.back.getTailInfo
+      | throwErrorAt allCommands.back "Failed to get source position"
+    let text ← getFileMap
+    let str := text.source.extract leading.startPos trailing.stopPos
+    modifyEnv fun ρ => highlighted.addEntry ρ (name.getId, {highlighted := hl, original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
+    for (name, term) in termExamples do
+      let hl ← liftTermElabM (highlight term newMessages.toList.toArray trees)
+      let .original leading startPos _ _ := term.getHeadInfo
+        | throwErrorAt term "Failed to get source position"
+      let .original _ _ trailing stopPos := term.getTailInfo
+        | throwErrorAt term "Failed to get source position"
+      let str := text.source.extract leading.startPos trailing.stopPos
+      modifyEnv fun ρ => highlighted.addEntry ρ (name, {highlighted := #[hl], original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
+
+scoped syntax "%dump" ident : command
+
+elab_rules : command
+  | `(%dump%$kw $name:ident) => do
+    let st := highlighted.getState (← getEnv)
+    if let some json := st.find? name.getId then
+      logInfoAt kw m!"{toString json}"
+    else
+      throwErrorAt name "No highlighting found for '{name}'"
+
+open System in
+partial def loadExamples (leanProject : FilePath) : IO (NameMap Json) := do
+  -- Validate that the path is really a Lean project
+  let lakefile := leanProject / "lakefile.lean"
+  if !(← lakefile.pathExists) then
+    throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project"
+  -- Build the facet
+  let res ← IO.Process.output {
+    cmd := "lake"
+    args := #["build", ":examples"]
+    cwd := leanProject
+  }
+  if res.exitCode != 0 then
+    throw <| .userError <|
+      "Build process failed." ++
+      decorateOut "stdout" res.stdout ++
+      decorateOut "stderr" res.stderr
+  let hlDir := leanProject / ".lake" / "build" / "examples"
+  collectExamples .anonymous hlDir
+where
+  decorateOut (name : String) (out : String) : String :=
+    if out.isEmpty then "" else s!"\n{name}:\n{out}\n"
+  collectExamples (name : Name) (dir : FilePath) : IO (NameMap Json) := do
+    let contents ← dir.readDir
+    let mut out := {}
+    for f in contents do
+      match (← f.path.metadata).type with
+      | .dir =>
+        let sub ← collectExamples (.str name f.fileName) f.path
+        out := out.mergeBy (fun _ _ j2 => j2) sub
+      | .file =>
+        if f.path.extension == some "json" then
+          if let some mod := f.path.fileStem then
+            let name' : Name := .str name mod
+            let contents := Json.parse (← IO.FS.readFile f.path)
+            match contents with
+            | .error err => throw <| .userError s!"Couldn't parse {f.path} as JSON: {err}"
+            | .ok val =>
+              out := out.insert name' val
+      | _ => pure ()
+    return out
+
+
+%example test3
+def wxyz (n : Nat) := 1 + 3 + n
+#check wxyz
+def xyz (n : Nat) := 1 + %ex{test2}{3 + n}
+%end
+
+--%process_highlights
+
+-- %example test
+-- #eval 5
+-- %end
+
+-- %dump test
+%dump test2
+%dump test3
diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean
new file mode 100644
index 0000000..fda414f
--- /dev/null
+++ b/src/examples/SubVerso/Examples/Env.lean
@@ -0,0 +1,54 @@
+import Lean
+import SubVerso.Highlighting
+
+open Lean
+
+namespace SubVerso.Examples
+open SubVerso.Highlighting
+
+instance : ToJson Position where
+  toJson | ⟨l, c⟩ => toJson (l, c)
+
+instance : FromJson Position where
+  fromJson?
+    | .arr #[l, c] => Position.mk <$> fromJson? l <*> fromJson? c
+    | other => .error s!"Couldn't decode position from {other}"
+
+example : fromJson? (toJson (⟨1, 5⟩ : Position)) = .ok (⟨1, 5⟩ : Position) := rfl
+
+instance : ToJson MessageSeverity where
+  toJson
+    | .error => "error"
+    | .warning => "warning"
+    | .information => "information"
+
+instance : FromJson MessageSeverity where
+  fromJson?
+    | "error" => .ok .error
+    | "warning" => .ok .warning
+    | "information" => .ok .information
+    | other => .error s!"Expected 'error', 'warning', or 'information', got {other}"
+
+theorem MessageSeverity.fromJson_toJson_ok (s : MessageSeverity) : fromJson? (toJson s) = .ok s := by
+  cases s <;> simp [toJson, fromJson?]
+
+structure Example where
+  highlighted : Array Highlighted
+  messages : List (MessageSeverity × String)
+  original : String
+  start : Lean.Position
+  stop : Lean.Position
+deriving ToJson, FromJson
+
+initialize highlighted : PersistentEnvExtension (NameMap Json) (Name × Example) (NameMap Json) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {}
+    addImportedFn := fun imported => do
+      let mut s := {}
+      for imp in imported do
+        for found in imp do
+          s := s.mergeBy (fun _ _ json => json) found
+      pure s
+    addEntryFn := fun s (n, val) => s.insert n (toJson val)
+    exportEntriesFn := fun s => #[s]
+  }
diff --git a/src/highlighting/SubVerso/Highlighting.lean b/src/highlighting/SubVerso/Highlighting.lean
new file mode 100644
index 0000000..0a0ae0d
--- /dev/null
+++ b/src/highlighting/SubVerso/Highlighting.lean
@@ -0,0 +1,2 @@
+import SubVerso.Highlighting.Highlighted
+import SubVerso.Highlighting.Code
diff --git a/src/highlighting/Subverso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
similarity index 99%
rename from src/highlighting/Subverso/Highlighting/Code.lean
rename to src/highlighting/SubVerso/Highlighting/Code.lean
index 1e3322f..3bcdc93 100644
--- a/src/highlighting/Subverso/Highlighting/Code.lean
+++ b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -1,14 +1,14 @@
 import Lean
 import Lean.Widget.TaggedText
 
-import Subverso.Highlighting.Highlighted
+import SubVerso.Highlighting.Highlighted
 
 open Lean Elab
 open Lean.Widget (TaggedText)
 open Lean.Widget
 open Lean.PrettyPrinter (InfoPerPos)
 
-namespace Subverso.Highlighting
+namespace SubVerso.Highlighting
 
 partial def Token.Kind.priority : Token.Kind → Nat
   | .var .. => 2
diff --git a/src/highlighting/Subverso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
similarity index 99%
rename from src/highlighting/Subverso/Highlighting/Highlighted.lean
rename to src/highlighting/SubVerso/Highlighting/Highlighted.lean
index 526c32f..c4a1529 100644
--- a/src/highlighting/Subverso/Highlighting/Highlighted.lean
+++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
@@ -2,7 +2,7 @@ import Lean
 
 open Lean
 
-namespace Subverso.Highlighting
+namespace SubVerso.Highlighting
 
 deriving instance Repr for Std.Format.FlattenBehavior
 deriving instance Repr for Std.Format
diff --git a/src/highlighting/Subverso/Highlighting.lean b/src/highlighting/Subverso/Highlighting.lean
deleted file mode 100644
index ab51c69..0000000
--- a/src/highlighting/Subverso/Highlighting.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Subverso.Highlighting.Highlighted
-import Subverso.Highlighting.Code