agda2lagda-0.2021.6.1: src/Render.hs

-- | Render the parsed items.

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}

module Render
  ( lagdaTex
  ) where

import Util

import qualified LexicalStructure as L
import Markup
import Version

-- | Render into plain literate LaTeX Agda.

lagdaTex :: [L.Item] -> String
lagdaTex its = unlines $ concat
   [ ["%% This file was automatically generated by agda2lagda " ++ version ++ "."]
   , [""]
   , map render $ markup its
   ]
  where
  render = \case
    TextItem it -> renderTex it
    CommItem s  -> unlines $ map ("%% " ++) $ lines s
    CodeItem s  -> concat
      [ "\\begin{code}\n"
      , s
      , "\\end{code}\n"
      ]

-- | Render a markup item

renderTex :: TextItem -> String
renderTex = \case
  Paragraph p -> unlines p
  Heading 1 s -> "\\heading{" ++ s ++ "}\n"
  Heading 2 s -> "\\subheading{" ++ s ++ "}\n"
  Itemize ps  -> unlines $ concat $
    [ [ "\\begin{itemize}\n" ]
    , map (unlines . ("\\item" :)) ps
    , [ "\\end{itemize}" ]
    ]