Aelve Codesearch

grep over package repositories
Please provide a string to search for.
3+ characters are required.
Index updated about a month ago

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/Interaction/Highlighting/Generate.hs
    modMap <- sourceToModule
    kinds  <- nameKinds hlLevel decl

    let nameInfo = mconcat $ map (generate modMap file kinds) names

    -- Constructors are only highlighted after type checking, since they
    -- can be overloaded.
    constructorInfo <- case hlLevel of
      Full{} -> generateConstructorInfo modMap file kinds decl

            
src/full/Agda/Interaction/Highlighting/Generate.hs
                                       , nameInfo
                                       , warnInfo
                                       ])
                       `mappend`
                     curTokens

    when updateState $ do
      stSyntaxInfo `modifyTCLens` mappend syntaxInfo
      stTokens     `setTCLens` (prevTokens `mappend` postTokens)

    ifTopLevelAndHighlightingLevelIs NonInteractive $
      printHighlightingInfo KeepHighlighting syntaxInfo
  where
  -- All names mentioned in the syntax tree (not bound variables).

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  -- All names mentioned in the syntax tree (not bound variables).
  names :: [A.AmbiguousQName]
  names =
    (map I.unambiguous $
     filter (not . isExtendedLambdaName) $
     universeBi decl) ++
    universeBi decl

  -- Bound variables, dotted patterns, record fields, module names,

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    getLam (A.DomainFull {}) = mempty

    getTyped :: A.TypedBinding -> File
    getTyped (A.TBind _ xs _) = mconcat $ map (bound . Common.namedArg) xs
    getTyped A.TLet{}         = mempty

    getPatSynArgs :: A.Declaration -> File
    getPatSynArgs (A.PatternSynDef _ xs _) = mconcat $ map (bound . A.BindName . Common.unArg) xs
    getPatSynArgs _                        = mempty

    getPattern' :: IsProjP e => A.Pattern' e -> File
    getPattern' (A.VarP x)    = bound x
    getPattern' (A.AsP _ x _) = bound x

            
src/full/Agda/Interaction/Highlighting/Generate.hs

    getModuleName :: A.ModuleName -> File
    getModuleName m@(A.MName { A.mnameToList = xs }) =
      mconcat $ map (mod isTopLevelModule) xs
      where
      isTopLevelModule =
        case mapMaybe (join .
                  fmap (Strict.toLazy . P.srcFile) .
                  P.rStart .
                  A.nameBindingSite) xs of
          f : _ -> Map.lookup f modMap ==
                   Just (C.toTopLevelModuleName $ A.mnameToConcrete m)
          []    -> False

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    getModuleInfo (SI.ModuleInfo { SI.minfoAsTo   = asTo
                                 , SI.minfoAsName = name }) =
      singleton (rToR asTo) (parserBased { aspect = Just Symbol })
        `mappend`
      maybe mempty asName name

-- | Generate and return the syntax highlighting information for the
-- tokens in the given file.


            
src/full/Agda/Interaction/Highlighting/Generate.hs

-- | Compute syntax highlighting for the given tokens.
tokenHighlighting :: [T.Token] -> CompressedFile
tokenHighlighting = merge . map tokenToCFile
  where
  -- Converts an aspect and a range to a file.
  aToF a r = singletonC (rToR r) (mempty { aspect = Just a })

  -- Merges /sorted, non-overlapping/ compressed files.

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  aToF a r = singletonC (rToR r) (mempty { aspect = Just a })

  -- Merges /sorted, non-overlapping/ compressed files.
  merge = CompressedFile . concat . map ranges

  tokenToCFile :: T.Token -> CompressedFile
  tokenToCFile (T.TokSetN (i, _))               = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokPropN (i, _))              = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokKeyword T.KwSet  i)        = aToF PrimitiveType (P.getRange i)

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  tokenToCFile (T.TokDummy {})                  = mempty
  tokenToCFile (T.TokEOF {})                    = mempty

-- | A function mapping names to the kind of name they stand for.

type NameKinds = A.QName -> Maybe NameKind

-- | Builds a 'NameKinds' function.


            
src/full/Agda/Interaction/Highlighting/Generate.hs
  local    <- case hlLevel of
    Full{} -> fix <$> useTC stSignature
    _      -> return HMap.empty
      -- Traverses the syntax tree and constructs a map from qualified
      -- names to name kinds. TODO: Handle open public.
  let syntax = foldr ($) HMap.empty $ map declToKind $ universeBi decl
  let merged = unions [local, imported, syntax]
  return (\n -> HMap.lookup n merged)
  where
  fix = HMap.map (defnToKind . theDef) . (^. sigDefinitions)

  -- | The 'M.Axiom' constructor is used to represent various things
  -- which are not really axioms, so when maps are merged 'Postulate's
  -- are thrown away whenever possible. The 'declToKind' function
  -- below can return several explanations for one qualified name; the
  -- 'Postulate's are bogus.
  merge Postulate k = k
  merge _     Macro = Macro  -- If the abstract syntax says macro, it's a macro.

            
src/full/Agda/Interaction/Highlighting/Generate.hs
-- | Generate syntax highlighting for termination errors.

terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting termErrs = functionDefs `mappend` callSites
  where
    m            = parserBased { otherAspects = Set.singleton TerminationProblem }
    functionDefs = Fold.foldMap (\x -> singleton (rToR $ bindingSite x) m) $
                   concatMap M.termErrFunctions termErrs
    callSites    = Fold.foldMap (\r -> singleton (rToR r) m) $

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    functionDefs = Fold.foldMap (\x -> singleton (rToR $ bindingSite x) m) $
                   concatMap M.termErrFunctions termErrs
    callSites    = Fold.foldMap (\r -> singleton (rToR r) m) $
                   concatMap (map M.callInfoRange . M.termErrCalls) termErrs

-- | Generate syntax highlighting for not-strictly-positive inductive
-- definitions.

-- TODO: highlight also the problematic occurrences

            
src/full/Agda/Interaction/Highlighting/Generate.hs
positivityErrorHighlighting q os =
  several (rToR <$> P.getRange q : rs) m
  where
    rs = map (\(OccursWhere r _ _) -> r) (Fold.toList os)
    m  = parserBased { otherAspects = Set.singleton PositivityProblem }

deadcodeHighlighting :: P.Range -> File
deadcodeHighlighting r = singleton (rToR $ P.continuousPerLine r) m
  where m = parserBased { otherAspects = Set.singleton Deadcode }

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  constraintInfo <- computeUnsolvedConstraints

  printHighlightingInfo KeepHighlighting
    (compress $ metaInfo `mappend` constraintInfo)

-- | Generates syntax highlighting information for unsolved meta
-- variables.

computeUnsolvedMetaWarnings :: TCM File

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  let notBlocked m = not <$> isBlockedTerm m
  ms <- filterM notBlocked =<< getOpenMetas

  rs <- mapM getMetaRange (ms \\ is)
  return $ metasHighlighting rs

metasHighlighting :: [P.Range] -> File
metasHighlighting rs = several (map (rToR . P.continuousPerLine) rs)
                     $ parserBased { otherAspects = Set.singleton UnsolvedMeta }

-- | Generates syntax highlighting information for unsolved constraints
--   (ideally: that are not connected to a meta variable).


            
src/full/Agda/Interaction/Highlighting/Generate.hs

constraintsHighlighting :: Constraints -> File
constraintsHighlighting cs =
  several (map (rToR . P.continuousPerLine) rs)
          (parserBased { otherAspects = Set.singleton UnsolvedConstraint })
  where
  -- get ranges of interesting unsolved constraints
  rs = (`mapMaybe` (map theConstraint cs)) $ \case
    Closure{ clValue = IsEmpty r t           } -> Just r
    Closure{ clEnv = e, clValue = ValueCmp{} } -> Just $ getRange (envRange e)
    Closure{ clEnv = e, clValue = ElimCmp{}  } -> Just $ getRange (envRange e)
    Closure{ clEnv = e, clValue = TypeCmp{}  } -> Just $ getRange (envRange e)
    Closure{ clEnv = e, clValue = TelCmp{}   } -> Just $ getRange (envRange e)

            
src/full/Agda/Interaction/Highlighting/Generate.hs
generate modMap file kinds (A.AmbQ qs) =
  Fold.foldMap (\ q -> nameToFileA modMap file q include m) qs
  where
    ks   = map kinds (Fold.toList qs)
    -- Ulf, 2014-06-03: [issue1064] It's better to pick the first rather
    -- than doing no highlighting if there's an ambiguity between an
    -- inductive and coinductive constructor.
    kind = case [ k | Just k <- ks ] of
             k : _ -> Just k

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    -- concrete name, so either they are all operators, or none of
    -- them are.
    m isOp  = parserBased { aspect = Just $ Name kind isOp }
    include = allEqual (map bindingSite $ Fold.toList qs)

-- | Converts names to suitable 'File's.

nameToFile :: SourceToModule
              -- ^ Maps source file paths to module names.

            
src/full/Agda/Interaction/Highlighting/Generate.hs
nameToFile modMap file xs x fr m mR =
  -- We don't care if we get any funny ranges.
  if all (== Strict.Just file) fileNames then
    frFile `mappend`
    several (map rToR rs)
            (aspects { definitionSite = mFilePos })
   else
    mempty
  where
  aspects    = m $ C.isOperator x

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    mempty
  where
  aspects    = m $ C.isOperator x
  fileNames  = mapMaybe (fmap P.srcFile . P.rStart . P.getRange) (x : xs)
  frFile     = singleton (rToR fr) (aspects { definitionSite = notHere <$> mFilePos })
  rs         = map P.getRange (x : xs)

  -- The fixity declaration should not get a symbolic anchor.
  notHere d = d { defSiteHere = False }

  mFilePos  :: Maybe DefinitionSite

            
src/full/Agda/Interaction/Highlighting/Generate.hs
             r
             m
             (if include then Just $ bindingSite x else Nothing)
    `mappend` notationFile
  where
    -- Andreas, 2016-09-08, for issue #2140:
    -- Range of name from fixity declaration:
    fr = theNameRange $ A.nameFixity $ A.qnameName x
    -- Somehow we import fixity ranges from other files, we should ignore them.

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    -- (I do not understand how we get them as they should not be serialized...)
    r = if P.rangeFile fr == Strict.Just file then fr else P.noRange

    notationFile = mconcat $ map genPartFile $ theNotation $ A.nameFixity $ A.qnameName x
    boundAspect = parserBased{ aspect = Just $ Name (Just Bound) False }
    genPartFile (BindHole r i)   = several [rToR r, rToR $ getRange i] boundAspect
    genPartFile (NormalHole r i) = several [rToR r, rToR $ getRange i] boundAspect
    genPartFile WildHole{}       = mempty
    genPartFile (IdPart x)       = singleton (rToR $ P.getRange x) (m False)

            
src/full/Agda/Interaction/Highlighting/Generate.hs
concreteBase = A.nameConcrete . A.qnameName

concreteQualifier :: I.QName -> [C.Name]
concreteQualifier = map A.nameConcrete . A.mnameToList . A.qnameModule

bindingSite :: I.QName -> P.Range
bindingSite = A.nameBindingSite . A.qnameName

-- | Remember a name disambiguation (during type checking).

            
src/full/Agda/Interaction/Highlighting/HTML.hs
import System.FilePath
import System.Directory

import Text.Blaze.Html5 hiding (code, map, title)
import qualified Text.Blaze.Html5 as Html5
import Text.Blaze.Html5.Attributes as Attr
import Text.Blaze.Html.Renderer.Text
  -- The imported operator (!) attaches an Attribute to an Html value
  -- The defined operator (!!) attaches a list of such Attributes

            
src/full/Agda/Interaction/Highlighting/HTML.hs

      -- Pull source code and highlighting info from the state and
      -- generate all the web pages.
      mapM_ (\(n, mi) ->
              let i  = TCM.miInterface mi
                  ft = TCM.iFileType i in
              generatePage dir ft
                (highlightOnlyCode htmlHighlight ft)
                (highlightedFileExt htmlHighlight ft) n

            
src/full/Agda/Interaction/Highlighting/HTML.hs
     -> CompressedFile -- ^ Highlighting information.
     -> [TokenInfo]
tokenStream contents info =
  map (\cs -> case cs of
          (mi, (pos, _)) : _ ->
            (pos, map (snd . snd) cs, fromMaybe mempty mi)
          [] -> __IMPOSSIBLE__) $
  List.groupBy ((==) `on` fst) $
  map (\(pos, c) -> (IntMap.lookup pos infoMap, (pos, c))) $
  zip [1..] (T.unpack contents)
  where
  infoMap = toMap (decompress info)

-- | Constructs the HTML displaying the code.

            
src/full/Agda/Interaction/Highlighting/HTML.hs
         -- Explicitly written all cases, so people
         -- get compile error when adding new file types
         -- when they forget to modify the code here
         RstFileType  -> map mkRst . splitByMarkup
         MdFileType   -> map mkMd . chunksOf 2 . splitByMarkup
         AgdaFileType -> map mkHtml
         -- Any points for using this option?
         TexFileType  -> map mkMd . chunksOf 2 . splitByMarkup
         OrgFileType  -> map mkOrg . splitByMarkup
  else map mkHtml
  where
  trd (_, _, a) = a

  splitByMarkup :: [TokenInfo] -> [[TokenInfo]]
  splitByMarkup = splitWhen $ (== Just Markup) . aspect . trd

            
src/full/Agda/Interaction/Highlighting/HTML.hs

  -- | Proposed in #3373, implemented in #3384
  mkRst :: [TokenInfo] -> Html
  mkRst = mconcat . (toHtml rstDelimiter :) . map go
    where
      go token@(_, s, mi) = if aspect mi == Just Background
        then preEscapedToHtml s
        else mkHtml token


            
src/full/Agda/Interaction/Highlighting/HTML.hs
      go _      = __IMPOSSIBLE__

  mkOrg :: [TokenInfo] -> Html
  mkOrg = mconcat . map go
    where
      go token@(_, s, mi) = if aspect mi == Just Background
        then preEscapedToHtml s
        else mkHtml token


            
src/full/Agda/Interaction/Highlighting/HTML.hs
    posAttributes :: [Attribute]
    posAttributes = concat
      [ [Attr.id $ stringValue $ show pos ]
      , toList $ fmap link $ definitionSite mi
      , class_ (stringValue $ unwords classes) <$ guard (not $ null classes)
      ]

    -- | Named anchor (not reliable, but useful in the general case for outside refs).
    nameAttributes :: [Attribute]