agda2lagda-0.2020.11.1: src/Render.hs

-- | Render the parsed items.

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

module Render
  ( lagdaTex
  , gobbleTrailingBlockCommentClosers
  ) where

import Data.Char
  (isSpace)

import LexicalStructure
  (Item, pattern TextItem, pattern CommItem, pattern CodeItem)
import Util
  (updateLast)

-- | Render into plain literate LaTeX Agda.

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

-- | Paragraphs followed by a line of dashes are turned into @\heading{}@s.

renderHeadingsTex :: String -> String
renderHeadingsTex = unlines . loop [] . lines
  where
  -- acc holds the current paragraph in reverse line order
  loop acc = \case
    [] -> reverse acc
    l : ls
      -- If we encounter a blank line, the paragraph ends: reset search for heading.
      | all isSpace l -> reverse ("":acc) ++ loop [] ls
      -- If we find a line of dashes, the current paragraph is a heading (unless it is empty).
      | all (=='-') l ->
          if null acc then loop [] ls
          else [ "\\heading{" ++ unwords (reverse acc) ++ "}" ] ++ loop [] ls
      -- Otherwise continue the current paragraph.
      | otherwise     -> loop (l:acc) ls

-- | Text lines at the end of file consisting solely of words "-}" are
-- discarded, to accommodate for a hack that makes it easy to comment
-- out everything to the end of the file.
-- https://github.com/agda/agda/issues/4953#issuecomment-702720296

gobbleTrailingBlockCommentClosers :: [Item] -> [Item]
gobbleTrailingBlockCommentClosers = updateLast $ \case
  TextItem s -> TextItem $ reverse $ loop $ reverse s
  i -> i
  where
  loop = \case
    -- Drop trailing spaces.
    c:cs | isSpace c -> loop cs
    -- Drop trailing block comment closers.
    '}':'-':cs -> loop cs
    -- Keep rest.
    s -> s