module Agda.Interaction.Highlighting.Vim where import Control.Monad.Trans import Data.Function ( on ) import qualified Data.List as List import qualified Data.Map as Map import Data.Maybe import System.FilePath import Agda.Syntax.Scope.Base import Agda.Syntax.Common import Agda.Syntax.Concrete.Name as CName import Agda.TypeChecking.Monad import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Tuple import Agda.Utils.Pretty vimFile :: FilePath -> FilePath vimFile file = case splitFileName file of (path, name) -> path "" <.> name <.> "vim" escape :: String -> String escape = concatMap esc where escchars :: String escchars = "$\\^.*~[]" esc c | c `elem` escchars = ['\\',c] | otherwise = [c] wordBounded :: String -> String wordBounded s0 = concat ["\\<", s0, "\\>"] keyword :: String -> [String] -> String keyword _ [] = "" keyword cat ws = "syn keyword " ++ unwords (cat : ws) match :: String -> [String] -> String match _ [] = "" match cat ws = "syn match " ++ cat ++ " \"" ++ List.intercalate "\\|" (map (wordBounded . escape) ws) ++ "\"" matches :: [String] -> [String] -> [String] -> [String] -> [String] -> [String] -> [String] matches cons icons defs idefs flds iflds = map snd $ List.sortBy (compare `on` fst) $ cons' ++ defs' ++ icons' ++ idefs' where cons' = foo "agdaConstructor" $ classify length cons icons' = foo "agdaInfixConstructor" $ classify length icons defs' = foo "agdaFunction" $ classify length defs idefs' = foo "agdaInfixFunction" $ classify length idefs classify f = List.groupBy ((==) `on` f) . List.sortBy (compare `on` f) foo :: String -> [[String]] -> [(Int, String)] foo cat = map (length . head /\ match cat) toVim :: NamesInScope -> String toVim ns = unlines $ matches mcons micons mdefs midefs mflds miflds where cons = [ x | (x, con:_) <- Map.toList ns, isJust $ isConName $ anameKind con ] defs = [ x | (x, def:_) <- Map.toList ns, isDefName (anameKind def) ] flds = [ x | (x, fld:_) <- Map.toList ns, anameKind fld == FldName ] mcons = map prettyShow cons mdefs = map prettyShow defs mflds = map prettyShow flds micons = concatMap parts cons midefs = concatMap parts defs miflds = concatMap parts flds parts n | isOperator n = map rawNameToString $ nameStringParts n | otherwise = [] generateVimFile :: FilePath -> TCM () generateVimFile file = do scope <- getScope liftIO $ UTF8.writeFile (vimFile file) $ toVim $ names scope where names = nsNames . everythingInScope