diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
index 1d38f85..c153b6e 100644
--- a/src/examples/SubVerso/Examples.lean
+++ b/src/examples/SubVerso/Examples.lean
@@ -68,28 +68,30 @@ elab_rules : command
       | 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 mod ← getMainModule
+    modifyEnv fun ρ => highlighted.addEntry ρ (mod, name.getId, {highlighted := hl, original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
+    for (tmName, 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})
+      modifyEnv fun ρ => highlighted.addEntry ρ (mod, name.getId ++ tmName, {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)
+    let mod ← getMainModule
+    let st := highlighted.getState (← getEnv) |>.find? mod |>.getD {}
     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
+partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example)) := do
   -- Validate that the path is really a Lean project
   let lakefile := leanProject / "lakefile.lean"
   if !(← lakefile.pathExists) then
@@ -110,23 +112,28 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap Json) := do
 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
+  collectExamples (modName : Name) (dir : FilePath) : IO (NameMap (NameMap Example)) := 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
+        let sub ← collectExamples (.str modName f.fileName) f.path
+        out := out.mergeBy (fun _ j1 j2 => j1.mergeBy (fun _ _ x => x) 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 name' : Name := .str modName 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
+              let .ok o := val.getObj?
+                | throw <| IO.userError "Expected JSON object in '{f.path}'"
+              for ⟨exName, exJson⟩ in o.toArray do
+                match FromJson.fromJson? (α := Example) exJson with
+                | .error err => throw <| IO.userError s!"Couldn't deserialized example: {err}"
+                | .ok ex => out := out.insert name' (out.find? name' |>.getD {} |>.insert exName.toName ex)
       | _ => pure ()
     return out
 
@@ -144,5 +151,5 @@ def xyz (n : Nat) := 1 + %ex{test2}{3 + n}
 -- %end
 
 -- %dump test
-%dump test2
+%dump test3.test2
 %dump test3
diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean
index fda414f..3db33c6 100644
--- a/src/examples/SubVerso/Examples/Env.lean
+++ b/src/examples/SubVerso/Examples/Env.lean
@@ -40,15 +40,17 @@ structure Example where
   stop : Lean.Position
 deriving ToJson, FromJson
 
-initialize highlighted : PersistentEnvExtension (NameMap Json) (Name × Example) (NameMap Json) ←
+initialize highlighted : PersistentEnvExtension (NameMap (NameMap Json)) (Name × Name × Example) (NameMap (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
+          s := s.mergeBy (fun _ exs1 exs2 => exs1.mergeBy (fun _ _ v => v) exs2) found
       pure s
-    addEntryFn := fun s (n, val) => s.insert n (toJson val)
+    addEntryFn := fun s (mod, ex, val) =>
+      let forMod := s.find? mod |>.getD .empty
+      s.insert mod (forMod.insert ex (toJson val))
     exportEntriesFn := fun s => #[s]
   }
diff --git a/src/examples/Subverso/Examples.lean b/src/examples/Subverso/Examples.lean
deleted file mode 100644
index c153b6e..0000000
--- a/src/examples/Subverso/Examples.lean
+++ /dev/null
@@ -1,155 +0,0 @@
-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
-    let mod ← getMainModule
-    modifyEnv fun ρ => highlighted.addEntry ρ (mod, name.getId, {highlighted := hl, original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs})
-    for (tmName, 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 ρ (mod, name.getId ++ tmName, {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 mod ← getMainModule
-    let st := highlighted.getState (← getEnv) |>.find? mod |>.getD {}
-    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 (NameMap Example)) := 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 (modName : Name) (dir : FilePath) : IO (NameMap (NameMap Example)) := do
-    let contents ← dir.readDir
-    let mut out := {}
-    for f in contents do
-      match (← f.path.metadata).type with
-      | .dir =>
-        let sub ← collectExamples (.str modName f.fileName) f.path
-        out := out.mergeBy (fun _ j1 j2 => j1.mergeBy (fun _ _ x => x) j2) sub
-      | .file =>
-        if f.path.extension == some "json" then
-          if let some mod := f.path.fileStem then
-            let name' : Name := .str modName 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 =>
-              let .ok o := val.getObj?
-                | throw <| IO.userError "Expected JSON object in '{f.path}'"
-              for ⟨exName, exJson⟩ in o.toArray do
-                match FromJson.fromJson? (α := Example) exJson with
-                | .error err => throw <| IO.userError s!"Couldn't deserialized example: {err}"
-                | .ok ex => out := out.insert name' (out.find? name' |>.getD {} |>.insert exName.toName ex)
-      | _ => 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 test3.test2
-%dump test3
diff --git a/src/examples/Subverso/Examples/Env.lean b/src/examples/Subverso/Examples/Env.lean
deleted file mode 100644
index 3db33c6..0000000
--- a/src/examples/Subverso/Examples/Env.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-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 (NameMap Json)) (Name × Name × Example) (NameMap (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 _ exs1 exs2 => exs1.mergeBy (fun _ _ v => v) exs2) found
-      pure s
-    addEntryFn := fun s (mod, ex, val) =>
-      let forMod := s.find? mod |>.getD .empty
-      s.insert mod (forMod.insert ex (toJson val))
-    exportEntriesFn := fun s => #[s]
-  }