1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65

import Lean
import LeanTeX.SlideDSL
import LeanTeX.SlideRegistry
import LeanTeX.PackageRegistry
import LeanTeX.PreambleRegistry
import LeanTeX.LatexCommandRegistry
import LeanTeX.LatexGen

def beamerPreamble (packages: String) (preamble: String) : String :=
   s!"\\documentclass[14pt,aspectratio=169,xcolor=\{usenames,dvipsnames,svgnames}]\{beamer}\n\\usepackage\{tikz}\n{packages}\n{preamble}\n\\begin\{document}"
def beamerPostamble : String := "\\end{document}\n%%% Local Variables:\n%%% mode: LaTeX\n%%% TeX-master: t\n%%% End:\n"

structure LeanTeXConfig where
  slides: List Slide
  packages: String
  preamble: String

  latexCommand: Option String
  latexOptions: List String

  preambleTemplate: Option (forall packages preamble:String, String)


section Meta
open Lean Elab Command Term Meta
syntax (name := getConfig) "#leantex_config" ident : command
@[command_elab getConfig]
unsafe def elabLeanTexConfig : CommandElab
| `(command| #leantex_config $name:ident) => do
   let slides <- liftTermElabM LeanTeX.loadSlidesStx
   let packages <- Syntax.mkStrLit <$> liftTermElabM LeanTeX.getPackageStr
   let preamble <- liftTermElabM LeanTeX.getPreambleStr
   let latexCommand <- liftTermElabM LeanTeX.getLaTeXCommand
   let latexOptions <- liftTermElabM LeanTeX.getLaTeXCommandOptions
   let preambleTemplate <- liftTermElabM LeanTeX.getPreambleTemplateCommand
   elabCommand $ <- `(command| def $name : LeanTeXConfig :=
       LeanTeXConfig.mk
          $slides
          $packages
          $preamble
          $latexCommand
          $latexOptions
          $preambleTemplate
   )
| _ => throwUnsupportedSyntax


end Meta
open Lean Meta

unsafe def generateSlides (config: LeanTeXConfig) : IO Unit := do
   let tex := config.slides.foldl (init := "") fun acc s => acc ++ renderSlide s
   let preambleTemplate := config.preambleTemplate.getD beamerPreamble
   let slides_tex := (preambleTemplate config.packages config.preamble ++ tex ++ beamerPostamble)
   let cmd := config.latexCommand.getD "pdflatex"
   let opts := config.latexOptions.toArray
   println! s!"{slides_tex}"
   if not $ <- ("build" : System.FilePath).pathExists then
      IO.FS.createDir "build"
   if <- ("static" : System.FilePath).pathExists then
       let _ <- IO.Process.run { cmd := "cp", args := #[ "-R", ".", "../build" ], cwd := "static" }
   IO.FS.writeFile "build/slides.tex" slides_tex
   let res <- IO.Process.spawn { cmd := cmd, args := opts ++ #["-shell-escape", "slides.tex"], cwd := "build"}
   let _ <- res.wait
   return ()