gdris

 1module Menu
 2
 3import Gopher
 4
 5import Data.Nat
 6import Data.Strings
 7
 8-- String used to seperate metadata from primary data in menu entries.
 9sep : String
10sep = " │ "
11
12-- Returns the maximum amount of characters required to display an entry type.
13maxTypeWidth : (List Item) -> Nat
14maxTypeWidth = foldr (\(MkItem ty _ _ _), acc => max (length $ show ty) acc) 0
15
16-- Adds spaces as padding to the end of the given String.
17padToWidth : String -> Nat -> String
18padToWidth str n = if (Strings.length str) >= n
19                    then str
20                    else padToWidth (str ++ " ") n
21
22-- Returns amount of digits required to display number in decimal.
23digitsReq : Nat -> Nat
24digitsReq n = if n `div` 10 > 0
25    then 1 + (digitsReq $ n `div` 10)
26    else 1
27
28public export
29showMenu : (List Item) -> String
30showMenu xs = trim $ showMenu' (digitsReq $ length xs) (maxTypeWidth xs) 0 xs
31    where
32        showItem : Nat -> Item -> String
33        showItem max (MkItem ty desc _ _) = (padToWidth (show ty) max) ++ sep ++ desc
34
35        showMenu' : Nat -> Nat -> Nat -> (List Item) -> String
36        showMenu' _ _ _ [] = ""
37        showMenu' maxNum maxTy n (x :: xs) = (padToWidth (show n) maxNum) ++
38                                             " " ++ showItem maxTy x ++ "\n" ++
39                                             (showMenu' maxNum maxTy (n + 1) xs)