@@ -25,65 +25,66 @@ open Lean Elab Term Command in
2525/--
2626Extract the marked exercises and example code.
2727-/
28- partial def buildExercises (mode : Mode) (logError : String → IO Unit) ( cfg : Config) (_state : TraverseState) (text : Part Manual) : IO Unit := do
28+ partial def buildExercises (mode : Mode) (cfg : Config) (_state : TraverseState) (text : Part Manual) : BuildLogT IO Unit := do
2929 let .multi := mode
3030 | pure ()
31- let code := (← part text |>.run {}).snd
32- let dest := cfg.destination / "example-code"
33- let some mainDir := mainFileName.parent
34- | throw <| IO.userError "Can't find directory of `BookGenMain.lean`"
35-
36- IO.FS.createDirAll <| dest
37- for ⟨fn, f⟩ in code do
38- -- Make sure the path is relative to that of this one
39- if let some fn' := fn.dropPrefix? mainDir.toString then
40- let fn' := (fn'.dropWhile (· ∈ System.FilePath.pathSeparators)).copy
41- let fn := dest / fn'
42- fn.parent.forM IO.FS.createDirAll
43- if (← fn.pathExists) then IO.FS.removeFile fn
44- IO.FS.writeFile fn f
45- else
46- logError s! "Couldn't save example code. The path '{ fn} ' is not underneath '{ mainDir} '."
31+ let logger ← readThe (Logger IO)
32+ saveExampleCode logger cfg text
4733
4834where
49- part : Part Manual → StateT (HashMap String String) IO Unit
35+ saveExampleCode (logger : Verso.Logger IO) (cfg : Config) (text : Part Manual) : IO Unit := do
36+ let code := (← part logger text |>.run {}).snd
37+ let dest := cfg.destination / "example-code"
38+ let some mainDir := mainFileName.parent
39+ | throw <| IO.userError "Can't find directory of `BookGenMain.lean`"
40+
41+ IO.FS.createDirAll <| dest
42+ for ⟨fn, f⟩ in code do
43+ -- Make sure the path is relative to that of this one
44+ if let some fn' := fn.dropPrefix? mainDir.toString then
45+ let fn' := fn'.toString.dropWhile (· ∈ System.FilePath.pathSeparators : Char → Bool)
46+ let fn := dest / fn'.copy
47+ fn.parent.forM IO.FS.createDirAll
48+ if (← fn.pathExists) then IO.FS.removeFile fn
49+ IO.FS.writeFile fn f
50+ else
51+ logger.reportError s! "Couldn't save example code. The path '{ fn} ' is not underneath '{ mainDir} '."
52+ part (logger : Verso.Logger IO) : Part Manual → StateT (HashMap String String) IO Unit
5053 | .mk _ _ _ intro subParts => do
51- for b in intro do block b
52- for p in subParts do part p
53- block : Block Manual → StateT (HashMap String String) IO Unit
54+ for b in intro do block logger b
55+ for p in subParts do part logger p
56+ block (logger : Verso.Logger IO) : Block Manual → StateT (HashMap String String) IO Unit
5457 | .other which contents => do
5558 if which.name == ``Block.savedLean then
5659 let .arr #[.str fn, .str code] := which.data
57- | logError s! "Failed to deserialize saved Lean data { which.data} "
60+ | logger.reportError s! "Failed to deserialize saved Lean data { which.data} "
5861 modify fun saved =>
59- saved.alter fn fun prior =>
60- let prior := prior.getD ""
61- some (prior ++ code ++ "\n " )
62+ let prior := saved[fn]?.getD ""
63+ saved.insert fn (prior ++ code ++ "\n " )
6264
6365 if which.name == ``Block.savedImport then
6466 let .arr #[.str fn, .str code] := which.data
65- | logError s! "Failed to deserialize saved Lean import data { which.data} "
67+ | logger.reportError s! "Failed to deserialize saved Lean import data { which.data} "
6668 modify fun saved =>
67- saved.alter fn fun prior =>
68- let prior := prior.getD ""
69- some (code.trimAsciiEnd.copy ++ "\n " ++ prior)
69+ let prior := saved[fn]?.getD ""
70+ saved.insert fn (code.trimAsciiEnd.copy ++ "\n " ++ prior)
7071
71- for b in contents do block b
72+ for b in contents do block logger b
7273 | .concat bs | .blockquote bs =>
73- for b in bs do block b
74+ for b in bs do block logger b
7475 | .ol _ lis | .ul lis =>
7576 for li in lis do
76- for b in li.contents do block b
77+ for b in li.contents do block logger b
7778 | .dl dis =>
7879 for di in dis do
79- for b in di.desc do block b
80+ for b in di.desc do block logger b
8081 | .para .. | .code .. => pure ()
8182
8283
8384def config : RenderConfig where
8485 emitTeX := false
8586 emitHtmlSingle := .no
8687 emitHtmlMulti := .immediately
87- htmlDepth := 2
88+ htmlDepth := 1
8889
8990def main := manualMain (%doc IrisTutorialBook) (extraSteps := [buildExercises]) (config := config)
0 commit comments