Remove slice dependency

Author: pimotte

WaterproofGenre.lean

@@ -4,7 +4,6 @@
 
 import Verso
 import Lean.Elab
-import SubVerso.Examples.Slice
 import SubVerso.Highlighting
 import Init.Data.ToString.Basic
 import Verso.Code
@@ -19,7 +18,6 @@ open Verso.Doc Elab
 open Lean.Quote
 open Lean Syntax
 
-open SubVerso.Examples.Slice
 open SubVerso.Highlighting
 
 structure Block where
@@ -49,7 +47,6 @@ def processString (altStr : String) :  DocElabM (Array (TSyntax `term)) := do
   let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}, {header := ""}]}
   let mut pstate := {pos := 0, recovering := false}
   let mut exercises := #[]
-  let mut solutions := #[]
 
   repeat
     let scope := cmdState.scopes.head!
@@ -58,14 +55,9 @@ def processString (altStr : String) :  DocElabM (Array (TSyntax `term)) := do
     pstate := ps'
     cmdState := {cmdState with messages := messages}
 
-    -- dbg_trace "Unsliced is {cmd}"
-    let slices : Slices ← DocElabM.withFileMap (FileMap.ofString altStr) (sliceSyntax cmd)
-    let sol := slices.sliced.getD "solution" slices.residual
-    solutions := solutions.push sol
-
     cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `DemoTextbook.Exts.lean, stx := cmd})) do
       let mut cmdState := cmdState
-      match (← liftM <| EIO.toIO' <| (Command.elabCommand sol cctx).run cmdState) with
+      match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with
       | Except.error e => logError e.toMessageData
       | Except.ok ((), s) =>
         cmdState := s