chore: adapt to elab branch

Manual/Classes.lean

@@ -159,7 +159,7 @@ use the command `set_option checkBinderAnnotations false` to disable the check
 
 ::::example "Class vs Structure Constructors"
 A very small algebraic hierarchy can be represented either as structures ({name}`S.Magma`, {name}`S.Semigroup`, and {name}`S.Monoid` below), a mix of structures and classes ({name}`C1.Monoid`), or only using classes ({name}`C2.Magma`, {name}`C2.Semigroup`, and {name}`C2.Monoid`):
-````lean
+```lean
 namespace S
 structure Magma (α : Type u) where
   op : α → α → α
@@ -192,7 +192,7 @@ class Monoid (α : Type u) extends Semigroup α where
   ident_left : ∀ x, op ident x = x
   ident_right : ∀ x, op x ident = x
 end C2
-````
+```
 
 
 {name}`S.Monoid.mk` and {name}`C1.Monoid.mk` have identical signatures, because the parent of the class {name}`C1.Monoid` is not itself a class:
@@ -258,7 +258,7 @@ Two instances of the same class with the same parameters are not necessarily ide
 ::::example "Instances are Not Unique"
 
 This implementation of binary heap insertion is buggy:
-````lean
+```lean
 structure Heap (α : Type u) where
   contents : Array α
 deriving Repr
@@ -275,7 +275,7 @@ def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
 def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
   let i := xs.contents.size
   {xs with contents := xs.contents.push x}.bubbleUp i
-````
+```
 
 The problem is that a heap constructed with one {name}`Ord` instance may later be used with another, leading to the breaking of the heap invariant.
 

Manual/Elaboration.lean

@@ -139,10 +139,10 @@ When interacting with Lean code, much more information is needed than when simpl
 For example, Lean's interactive environment can be used to view the types of selected expressions, to step through all the intermediate states of a proof, to view documentation, and highlight all occurrences of a bound variable.
 The information necessary to use Lean interactively is stored in a side table called the  {deftech}_info trees_ during elaboration.
 
-````lean (show := false)
+```lean (show := false)
 open Lean.Elab (Info)
 deriving instance TypeName for Unit
-````
+```
 
 
 Info trees relate metadata to the user's original syntax.

Manual/Intro.lean

@@ -73,19 +73,19 @@ tag := "code-samples"
 This document contains many Lean code examples.
 They are formatted as follows:
 
-````lean
+```lean
 def hello : IO Unit := IO.println "Hello, world!"
-````
+```
 
 Compiler output (which may be errors, warnings, or just information) is shown both in the code and separately:
 
-````lean (name := output) (error := true)
+```lean (name := output) (error := true)
 #eval s!"The answer is {2 + 2}"
 
 theorem bogus : False := by sorry
 
 example := Nat.succ "two"
-````
+```
 
 Informative output, such as the result of {keywordOf Lean.Parser.Command.eval}`#eval`, is shown like this:
 ```leanOutput output (severity := information)
@@ -183,7 +183,7 @@ tag := "reference-boxes"
 Definitions, inductive types, syntax formers, and tactics have specific descriptions.
 These descriptions are marked as follows:
 
-::::keepEnv
+
 ```lean
 /--
 Evenness: a number is even if it can be evenly divided by two.
@@ -197,7 +197,7 @@ inductive Even : Nat → Prop where
 
 {docstring Even}
 
-::::
+
 
 # Open-Source Licenses
 %%%

Manual/Language/InductiveTypes.lean

@@ -305,12 +305,13 @@ Constructors can be invoked anonymously by enclosing their explicit arguments in
 
 ::::example "Anonymous constructors"
 
-:::keepEnv
+
 ```lean (show:=false)
-axiom α : Type
+variable {α : Type u}
 ```
+
 The type {lean}`AtLeastOne α` is similar to `List α`, except there's always at least one element present:
-:::
+
 
 ```lean
 inductive AtLeastOne (α : Type u) : Type u where
@@ -366,9 +367,9 @@ tag := "inductive-types-runtime-special-support"
 
 Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler:
 :::keepEnv
-````lean (show := false)
+```lean (show := false)
 axiom α : Prop
-````
+```
 
  * The representation of the fixed-width integer types {lean}`UInt8`, …, {lean}`UInt64`, {lean}`Int8`, …, {lean}`Int64`, and {lean}`USize` depends on the whether the code is compiled for a 32- or 64-bit architecture.
    Fixed-width integer types that are strictly smaller than the architecture's pointer type are stored unboxed by setting the lowest bit of a pointer to `1`.
@@ -473,7 +474,7 @@ The memory order of the fields is derived from the types and order of the fields
 * Fields of type {lean}`USize`
 * Other scalar fields, in decreasing order by size
 
-Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
+Within each group the fields are ordered in declaration order. *Warning*: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
 
 * To access fields of the first kind, use {c}`lean_ctor_get(val, i)` to get the `i`th non-scalar field.
 * To access {lean}`USize` fields, use {c}`lean_ctor_get_usize(val, n+i)` to get the {c}`i`th `USize` field and {c}`n` is the total number of fields of the first kind.

Manual/Language/InductiveTypes/Structures.lean

@@ -507,7 +507,6 @@ example (t : Triple α) : t.fst = t.toPair.fst := rfl
 ::::
 
 :::: example "No structure subtyping"
-:::keepEnv
 Given these definitions of even numbers, even prime numbers, and a concrete even prime:
 ```lean
 structure EvenNumber where
@@ -543,7 +542,6 @@ but is expected to have type
   EvenNumber : Type
 ```
 because values of type {name}`EvenPrime` are not also values of type {name}`EvenNumber`.
-:::
 ::::
 
 

Manual/Meta/Example.lean

@@ -45,13 +45,13 @@ def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α  → m β)
 
 def isLeanBlock : TSyntax `block → CoreM Bool
   | `(block|```$nameStx:ident $_args*|$_contents:str```) => do
-    let name ← realizeGlobalConstNoOverloadWithInfo nameStx
+    let name ← realizeGlobalConstNoOverload nameStx
     return name == ``Verso.Genre.Manual.InlineLean.lean
   | _ => pure false
 
 
-@[directive_expander «example»]
-def «example» : DirectiveExpander
+@[directive_elab «example»]
+def «example» : DirectiveElab
   | args, contents => do
     let cfg ← ExampleConfig.parse.run args
 
@@ -65,12 +65,23 @@ def «example» : DirectiveExpander
     -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them
     let blocks ←
       if cfg.keep then
-        prioritizedElab (isLeanBlock ·) elabBlock contents
+        prioritizedElab (isLeanBlock ·) elabBlock' contents
       else
-        withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents
+        InlineLean.withIsolatedExamplesEnv <| prioritizedElab (isLeanBlock ·) elabBlock' contents
+
+    let it ← DocElabM.inlineType
+    let bt ← DocElabM.blockType
+
+    let description ← description.mapM (Term.elabTerm · (some it))
+
     -- Examples are represented using the first block to hold the description. Storing it in the JSON
     -- entails repeated (de)serialization.
-    pure #[← ``(Block.other (Block.example $(quote cfg.tag)) #[Block.para #[$description,*], $blocks,*])]
+    let g ← DocElabM.genreExpr
+    let exampleBlock : Expr := .app (.const ``Block.example []) (toExpr cfg.tag)
+    let descr : Expr := mkApp2 (.const ``Block.para []) g (← Meta.mkArrayLit it description.toList)
+    let blocks := #[descr] ++ blocks
+    return mkApp3 (.const ``Block.other []) g exampleBlock (← Meta.mkArrayLit bt blocks.toList)
+
 
 @[block_extension «example»]
 def example.descr : BlockDescr where
@@ -147,16 +158,14 @@ r#".example {
   ]
 
 
-def Block.keepEnv : Block where
-  name := `Manual.example
-
 -- TODO rename to `withoutModifyingEnv` or something more clear
 @[directive_expander keepEnv]
 def keepEnv : DirectiveExpander
   | args, contents => do
     let () ← ArgParse.done.run args
     PointOfInterest.save (← getRef) "keepEnv" (kind := .package)
-    withoutModifyingEnv <| withSaveInfoContext <| contents.mapM elabBlock
+    InlineLean.withIsolatedExamplesEnv <|
+      withSaveInfoContext <| contents.mapM elabBlock
 
 
 @[block_extension keepEnv]