packages feed

agda-language-server 0.2.6.2.2.1 → 0.2.6.3.0

raw patch · 23 files changed

+280/−94 lines, 23 filesdep ~AgdaPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: Agda

API changes (from Hackage documentation)

- Render.Concrete: instance Render.Class.Render Agda.Syntax.Common.GenPart
+ Render.Concrete: instance Render.Class.Render Agda.Syntax.Common.NotationPart
+ Render.Concrete: instance Render.Class.Render a => Render.Class.Render (Agda.Syntax.Common.Ranged a)
+ Render.Position: instance Render.Class.Render Agda.Syntax.Position.RangeFile
+ Render.RichText: instance Data.Aeson.Types.ToJSON.ToJSON Agda.Syntax.Position.RangeFile
- Agda.Convert: explainWhyInScope :: FilePath -> String -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> TCM Doc
+ Agda.Convert: explainWhyInScope :: String -> FilePath -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> TCM Doc

Files

CHANGELOG.md view
@@ -4,20 +4,30 @@  The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v0.2.6.3.0 - 2023-11-23++### Changed+- Embed Agda-2.6.3.+- Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26),+  and with Cabal also on 9.4 and 9.6.++### Added+- Build flag `Agda-2-6-2-2` to embed Agda-2.6.2.2 rather than 2.6.3.+ ## v0.2.6.2.2.1 - 2023-11-21  ### Added  - Building with `lsp-1.6`.-  Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26)+  Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26).  ## v0.2.6.2.2 - 2023-11-21  ### Changed -- Bundle Agda-2.6.2.2-- Versioning scheme: _x.a.b.c.d.y_ where _a.b.c.d_ is the 4-digit Agda version (2.6.2.2), _x_ is 0 but may be bumped for revolutionary changes to the agda-language-server, and _y_ is for patch releases-- Builds with `lsp` < 1.5 on GHC 8.10 (LTS 18.28) and 9.0 (LTS 19.33)+- Embed Agda-2.6.2.2.+- Versioning scheme: _x.a.b.c.d.y_ where _a.b.c.d_ is the 4-digit Agda version (2.6.2.2), _x_ is 0 but may be bumped for revolutionary changes to the agda-language-server, and _y_ is for patch releases.+- Builds with `lsp` < 1.5 on GHC 8.10 (LTS 18.28) and 9.0 (LTS 19.33).  ## v0.2.1 - 2021-10-25
agda-language-server.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           agda-language-server-version:        0.2.6.2.2.1+version:        0.2.6.3.0 synopsis:       An implementation of language server protocal (LSP) for Agda 2. description:    Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> category:       Development@@ -22,13 +22,19 @@     CHANGELOG.md     package.yaml     stack.yaml-    stack-8.10.yaml-    stack-9.0.yaml+    stack-8.10-Agda-2.6.2.2.yaml+    stack-9.0-Agda-2.6.2.2.yaml+    stack-9.2-Agda-2.6.2.2.yaml  source-repository head   type: git   location: https://github.com/banacorn/agda-language-server +flag Agda-2-6-2-2+  description: Embed Agda-2.6.2.2 (rather than 2.6.3)+  manual: True+  default: False+ library   exposed-modules:       Agda@@ -66,7 +72,7 @@       TypeOperators   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans   build-depends:-      Agda ==2.6.2.2+      Agda     , aeson     , base >=4.7 && <5     , bytestring@@ -80,6 +86,12 @@     , strict     , text   default-language: Haskell2010+  if flag(Agda-2-6-2-2)+    build-depends:+        Agda ==2.6.2.2+  else+    build-depends:+        Agda ==2.6.3  executable als   main-is: Main.hs@@ -93,7 +105,7 @@       TypeOperators   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans   build-depends:-      Agda ==2.6.2.2+      Agda     , aeson     , agda-language-server     , base >=4.7 && <5@@ -108,6 +120,12 @@     , strict     , text   default-language: Haskell2010+  if flag(Agda-2-6-2-2)+    build-depends:+        Agda ==2.6.2.2+  else+    build-depends:+        Agda ==2.6.3  test-suite als-test   type: exitcode-stdio-1.0@@ -149,7 +167,7 @@       TypeOperators   ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans   build-depends:-      Agda ==2.6.2.2+      Agda     , aeson     , base >=4.7 && <5     , bytestring@@ -167,3 +185,9 @@     , tasty-quickcheck     , text   default-language: Haskell2010+  if flag(Agda-2-6-2-2)+    build-depends:+        Agda ==2.6.2.2+  else+    build-depends:+        Agda ==2.6.3
package.yaml view
@@ -1,5 +1,5 @@ name:                agda-language-server-version:             0.2.6.2.2.1+version:             0.2.6.3.0 github:              "banacorn/agda-language-server" license:             MIT author:              "Ting-Gian LUA"@@ -11,8 +11,9 @@ - CHANGELOG.md - package.yaml - stack.yaml-- stack-8.10.yaml-- stack-9.0.yaml+- stack-8.10-Agda-2.6.2.2.yaml+- stack-9.0-Agda-2.6.2.2.yaml+- stack-9.2-Agda-2.6.2.2.yaml  # Metadata used when publishing your package synopsis:            An implementation of language server protocal (LSP) for Agda 2.@@ -23,14 +24,24 @@ # common to point users to the README.md file. description:         Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> -default-extensions:-- LambdaCase-- OverloadedStrings-- TypeOperators+flags:+  Agda-2-6-2-2:+    description: Embed Agda-2.6.2.2 (rather than 2.6.3)+    manual: true+    default: false +when:+- condition: flag(Agda-2-6-2-2)+  then:+    dependencies:+    - Agda == 2.6.2.2+  else:+    dependencies:+    - Agda == 2.6.3+ dependencies:   - base >= 4.7 && < 5-  - Agda == 2.6.2.2+  - Agda   - aeson   - bytestring   - containers@@ -42,6 +53,11 @@   - stm   - text   - process++default-extensions:+- LambdaCase+- OverloadedStrings+- TypeOperators  library:   source-dirs: src
src/Agda.hs view
@@ -1,4 +1,6 @@ {-# OPTIONS_GHC -Wno-missing-methods #-}++{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-}  module Agda@@ -17,6 +19,9 @@                                                 , CommandState(optionsOnReload)                                                 , IOTCM                                                 , initCommandState+#if MIN_VERSION_Agda(2,6,3)+                                                , parseIOTCM+#endif                                                 ) import           Agda.Interaction.InteractionTop                                                 ( initialiseCommandQueue@@ -52,6 +57,7 @@ import           Control.Exception              ( SomeException                                                 , catch                                                 )+import           Control.Monad import           Control.Monad.Except import           Control.Monad.Reader import           Control.Monad.State@@ -88,7 +94,7 @@     -- keep reading command     commands <- liftIO $ initialiseCommandQueue (readCommand env) -    -- get command line options +    -- get command line options     options  <- getCommandLineOptions      -- start the loop@@ -159,31 +165,37 @@       provideCommand iotcm       return $ CmdRes Nothing +#if !MIN_VERSION_Agda(2,6,3) parseIOTCM :: String -> Either String IOTCM parseIOTCM raw = case listToMaybe $ reads raw of   Just (x, ""     ) -> Right x   Just (_, remnent) -> Left $ "not consumed: " ++ remnent   _                 -> Left $ "cannot read: " ++ raw+#endif  --------------------------------------------------------------------------------  getCommandLineOptions   :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions getCommandLineOptions = do-  -- command line options from ARGV +  -- command line options from ARGV   argv   <- asks (optRawAgdaOptions . envOptions)   -- command line options from agda-mode   config <- asks (configRawAgdaOptions . envConfig)-  -- concatenate both +  -- concatenate both   let merged = argv <> config    result <- runExceptT $ do-    (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions builtinBackends-                                                          merged-                                                          defaultOptions+    let p = parseBackendOptions builtinBackends merged defaultOptions+#if MIN_VERSION_Agda(2,6,3)+    let (r, _warns) = runOptM p+    (bs, opts) <- ExceptT $ pure r+#else+    (bs, opts) <- ExceptT $ runOptM p+#endif     return opts   case result of-    -- something bad happened, use the default options instead +    -- something bad happened, use the default options instead     Left  _    -> commandLineOptions     Right opts -> return opts
src/Agda/Convert.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Agda.Convert where  import Render ( Block(..), Inlines, renderATop, Render(..) )@@ -33,10 +35,11 @@ import Agda.Utils.Maybe (catMaybes) import Agda.Utils.Null (empty) import Agda.Utils.Pretty hiding (render)-import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) ) +import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) ) import Agda.Utils.String (delimiter) import Agda.Utils.Time (CPUTime) import Agda.VersionCommit (versionWithCommitInfo)+import Control.Monad import Control.Monad.State hiding (state) import qualified Data.Aeson as JSON import qualified Data.ByteString.Lazy.Char8 as BS8@@ -130,7 +133,7 @@     indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info))  fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo-fromDisplayInfo = \case +fromDisplayInfo = \case   Info_CompilationOk _ ws -> do     -- filter     let filteredWarnings = filterTCWarnings (tcWarnings ws)@@ -255,8 +258,13 @@           "Definitions about"             <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)     return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]+#if MIN_VERSION_Agda(2,6,3)+  Info_WhyInScope (WhyInScopeData q cwd v xs ms) -> do+    doc <- explainWhyInScope (prettyShow q) cwd v xs ms+#else   Info_WhyInScope s cwd v xs ms -> do     doc <- explainWhyInScope s cwd v xs ms+#endif     return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]   Info_Context ii ctx -> do     doc <- localTCState (prettyResponseContexts ii False ctx)@@ -373,8 +381,8 @@   return $ "Highlighting failed to scope check expression in " ++ show ii  explainWhyInScope ::-  FilePath ->   String ->+  FilePath ->   Maybe LocalVar ->   [AbstractName] ->   [AbstractModule] ->@@ -577,12 +585,12 @@     -- raw     rawExpr <- prettyATop expr     let rawType = show $ align 10 [(rawAttribute ++ rawCtxName, ":" <+> rawExpr <+> parenSep extras)]-    -- rendered  +    -- rendered     renderedExpr <- renderATop expr     let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2       -- (Render.fsep $ Render.punctuate "," extras) -    -- result +    -- result     let typeItem = Unlabeled renderedType (Just rawType) Nothing      valueItem <- case letv of
src/Agda/Parser.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Agda.Parser where  --------------------------------------------------------------------------------@@ -5,6 +7,9 @@ import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser) import Agda.Syntax.Parser.Tokens (Token) import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')+#if MIN_VERSION_Agda(2,6,3)+import Agda.Syntax.Position (RangeFile(RangeFile))+#endif import Agda.Utils.FileName (mkAbsolute) import Monad ( ServerM ) import Control.Monad.State@@ -22,10 +27,22 @@ tokenAt uri source position = case LSP.uriToFilePath uri of   Nothing -> return Nothing   Just filepath -> do+    let file =+#if MIN_VERSION_Agda(2,6,3)+          RangeFile (mkAbsolute filepath) Nothing+#else+          mkAbsolute filepath+#endif     (result, _warnings) <- liftIO $       runPMIO $ do         -- parse the file and get all tokens-        (tokens, _fileType) <- parseFile tokensParser (mkAbsolute filepath) (unpack source)+        (r, _fileType) <- parseFile tokensParser file (unpack source)+        let tokens =+#if MIN_VERSION_Agda(2,6,3)+              fst r+#else+              r+#endif         -- find the token at the position         return $ find (pointedBy position) tokens     case result of
src/Agda/Position.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Agda.Position   ( ToOffset(..)   , makeToOffset@@ -31,12 +33,17 @@ -- | LSP Range -> Agda Range toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range toAgdaRange table path (LSP.Range start end) = Range-  (Strict.Just (AbsolutePath path))+  (Strict.Just $ mkRangeFile $ AbsolutePath path)   (Seq.singleton interval)  where   interval :: IntervalWithoutFile   interval = Interval (toAgdaPositionWithoutFile table start)                       (toAgdaPositionWithoutFile table end)+#if MIN_VERSION_Agda(2,6,3)+  mkRangeFile path = RangeFile path Nothing+#else+  mkRangeFile = id+#endif  -- | LSP Position -> Agda PositionWithoutFile toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
src/Render/Common.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Render.Common where  import Agda.Syntax.Common@@ -30,7 +32,11 @@  -- | MetaId instance Render MetaId where+#if MIN_VERSION_Agda(2,6,3)+  render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m+#else   render (MetaId n) = text $ "_" ++ show n+#endif  -- | Relevance instance Render Relevance where
src/Render/Concrete.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE RankNTypes #-}@@ -12,7 +13,7 @@ import           Agda.Syntax.Concrete import           Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled) --import           Agda.Syntax.Position (noRange)-import           Agda.Utils.List1 as List1 (toList, fromList) +import           Agda.Utils.List1 as List1 (toList, fromList) import qualified Agda.Utils.List1 as List1 import qualified Agda.Utils.List2 as List2 import Agda.Utils.Float (toStringWithoutDotZero)@@ -29,6 +30,9 @@  -------------------------------------------------------------------------------- +instance Render a => Render (Ranged a) where+  render = render . rangedThing+ instance Render a => Render (WithHiding a) where   render w = renderHiding w id $ render $ dget w @@ -108,8 +112,10 @@     Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]     RecUpdate _ e xs ->       sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]+#if !MIN_VERSION_Agda(2,6,3)     ETel [] -> "()"     ETel tel -> fsep $ fmap render tel+#endif     Quote _ -> "quote"     QuoteTerm _ -> "quoteTerm"     Unquote _ -> "unquote"@@ -447,6 +453,10 @@       UnquoteDef _ xs t ->         fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]       Pragma pr -> sep ["{-#" <+> render pr, "#-}"]+#if MIN_VERSION_Agda(2,6,3)+      UnquoteData _ x xs e ->+        fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ]+#endif     where       namedBlock s ds =         fsep@@ -459,11 +469,11 @@   YesEta   -> "eta-equality"   NoEta () -> "no-eta-equality" -pRecordDirective :: +pRecordDirective ::   RecordDirective ->   Inlines pRecordDirective = \case-  Induction ind -> render (rangedThing ind)+  Induction ind -> render ind   Constructor n inst -> hsep [ pInst, "constructor", render n ] where     pInst = case inst of       InstanceDef{} -> "instance"@@ -551,6 +561,10 @@   render (PolarityPragma _ q occs) =     hsep ("POLARITY" : render q : fmap render occs)   render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"+#if MIN_VERSION_Agda(2,6,3)+  render (NotProjectionLikePragma _ q) =+    hsep [ "NOT_PROJECTION_LIKE", render q ]+#endif  instance Render Fixity where   render (Fixity _ Unrelated _) = __IMPOSSIBLE__@@ -561,11 +575,20 @@         RightAssoc -> "infixr"         NonAssoc -> "infix" +#if MIN_VERSION_Agda(2,6,3)+instance Render NotationPart where+  render = \case+    IdPart  x  -> text $ rangedThing x+    HolePart{} -> "_"+    VarPart {} -> "_"+    WildPart{} -> "_"+#else instance Render GenPart where   render (IdPart x) = text $ rangedThing x   render BindHole {} = "_"   render NormalHole {} = "_"   render WildHole {} = "_"+#endif  instance Render Fixity' where   render (Fixity' fix nota _)
src/Render/Interaction.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Render.Interaction where  import qualified Data.Set                      as Set@@ -98,6 +100,10 @@     "Check lock" <+> render lk <+> "allows" <+> render t   render (UsableAtMod modality t) =     "Is usable at" <+> render modality <+> render t+#if MIN_VERSION_Agda(2,6,3)+  render (DataSort _name expr) =+    fsep [ "Sort", render expr, "allows data/record definitions" ]+#endif  -- | IPBoundary' instance Render c => Render (IPBoundary' c) where
src/Render/Internal.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-}  module Render.Internal where@@ -20,7 +21,12 @@         IdS -> "idS"         EmptyS _ -> "emptyS"         t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]-        Strengthen _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho+#if MIN_VERSION_Agda(2,6,3)+        Strengthen _ _ rho ->+#else+        Strengthen _ rho ->+#endif+          mparens (p > 9) $ "strS" <+> pr 10 rho         Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho         Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho @@ -154,6 +160,9 @@       MetaS x es -> renderPrec p $ MetaV x es       DefS d es -> renderPrec p $ Def d es       DummyS s -> parens $ text s+#if MIN_VERSION_Agda(2,6,3)+      IntervalUniv -> "IntervalUniv"+#endif  instance Render Type where   renderPrec p (El _ a) = renderPrec p a@@ -200,3 +209,6 @@   render (UnblockOnAny us)      = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)   render (UnblockOnMeta m)      = render m   render (UnblockOnProblem pid) = "problem" <+> render pid+#if MIN_VERSION_Agda(2,6,3)+  render (UnblockOnDef q)       = "definition" <+> render q+#endif
src/Render/Position.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-}  module Render.Position where@@ -11,6 +12,11 @@ instance Render AbsolutePath where   render = text . filePath +#if MIN_VERSION_Agda(2,6,3)+instance Render RangeFile where+  render = render . rangeFilePath  -- TODO rangeFileName ?+#endif+ --------------------------------------------------------------------------------  instance Render a => Render (Position' (Strict.Maybe a)) where@@ -19,7 +25,7 @@     render f <> ":" <> render l <> "," <> render c  instance Render PositionWithoutFile where-  render p = render (p {srcFile = Strict.Nothing} :: Position)+  render (Pn () _ l c) = render l <> "," <> render c  instance Render IntervalWithoutFile where   render (Interval s e) = start <> "-" <> end
src/Render/RichText.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} @@ -56,13 +57,13 @@ -------------------------------------------------------------------------------- -- | Block elements -data Block +data Block   -- for blocks like "Goal" & "Have"-  = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String +  = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String   -- for ordinary goals & context   | Unlabeled Inlines (Maybe String) (Maybe Agda.Range)   -- headers-  | Header String  +  | Header String   deriving (Generic)  instance ToJSON Block@@ -85,7 +86,7 @@       cons :: Inline -> Seq Inline -> Seq Inline       cons (Text s c) (Text t d :<| xs)         -- merge 2 adjacent Text if they have the same classnames-        | c == d    = Text (s <> t) c :<| xs +        | c == d    = Text (s <> t) c :<| xs         | otherwise = Text s c :<| Text t d :<| xs       cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs       cons (Text s c) (Horz (Inlines t:ts) :<| xs)@@ -118,7 +119,7 @@     elemIsEmpty (Parn _) = False     elemIsEmpty (PrHz _) = False -infixr 6 <+> +infixr 6 <+>  (<+>) :: Inlines -> Inlines -> Inlines x <+> y@@ -168,7 +169,7 @@     Vert [Inlines]   | -- | Parenthese     Parn Inlines-  | -- | Parenthese around a Horizontal, special case +  | -- | Parenthese around a Horizontal, special case     PrHz [Inlines]   deriving (Generic) @@ -181,8 +182,8 @@   show (Hole i) = "?" ++ show i   show (Horz xs) = unwords (map show $ toList xs)   show (Vert xs) = unlines (map show $ toList xs)-  show (Parn x) = "(" <> show x <> ")" -  show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")" +  show (Parn x) = "(" <> show x <> ")"+  show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")"  -------------------------------------------------------------------------------- @@ -202,6 +203,11 @@ instance ToJSON Agda.AbsolutePath where   toJSON (Agda.AbsolutePath path) = toJSON path +#if MIN_VERSION_Agda(2,6,3)+instance ToJSON Agda.RangeFile where+  toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path+#endif+ --------------------------------------------------------------------------------  -- | Utilities / Combinators@@ -290,7 +296,7 @@ showIndex = map toSubscriptDigit . show  ----------------------------------------------------------------------------------- +-- -- | Picking the appropriate set of special characters depending on -- whether we are allowed to use unicode or have to limit ourselves -- to ascii.
src/Render/TypeChecking.hs view
@@ -4,12 +4,13 @@ import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Positivity.Occurrence import Render.Class+import Render.Common import Render.RichText  instance Render NamedMeta where-  render (NamedMeta "" (MetaId x)) = render x-  render (NamedMeta "_" (MetaId x)) = render x-  render (NamedMeta s (MetaId x)) = "_" <> text s <> render x+  render (NamedMeta ""  x) = render x+  render (NamedMeta "_" x) = render x+  render (NamedMeta s   x) = "_" <> text s <> render x  instance Render Occurrence where   render =
src/Server.hs view
@@ -9,9 +9,8 @@  import qualified Agda import           Control.Concurrent             ( writeChan )-import           Control.Monad.Reader           ( MonadIO(liftIO)-                                                , void-                                                )+import           Control.Monad                  ( void )+import           Control.Monad.Reader           ( MonadIO(liftIO) ) import           Data.Aeson                     ( FromJSON                                                 , ToJSON                                                 )
src/Server/Handler.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Server.Handler where  import           Agda                           ( getCommandLineOptions@@ -63,7 +65,7 @@ runCommandM program = do   env <- ask   runAgda $ do-    -- get command line options +    -- get command line options     options <- getCommandLineOptions      -- we need to set InteractionOutputCallback else it would panic@@ -86,7 +88,12 @@   let norm = AsIs   -- localStateCommandM: restore TC state afterwards, do we need this here?   typ <- localStateCommandM $ do-    e <- lift $ runPM $ parse exprParser (unpack text)+#if MIN_VERSION_Agda(2,6,3)+    (e, _attrs)+#else+    e+#endif+       <- lift $ runPM $ parse exprParser (unpack text)     lift $ atTopLevel $ do       concreteToAbstract_ e >>= typeInCurrent norm
src/Switchboard.hs view
@@ -3,6 +3,7 @@ import Monad import Control.Concurrent import qualified Server.ResponseController as ResponseController+import Control.Monad import Control.Monad.Reader import qualified Agda import qualified Data.Aeson as JSON@@ -12,7 +13,7 @@ import Data.IORef import Options (Config) -data Switchboard = Switchboard +data Switchboard = Switchboard   { sbPrintLog :: ThreadId   , sbSendResponse :: ThreadId   , sbRunAgda :: ThreadId@@ -21,7 +22,7 @@  -- | All channels go in and out from here new :: Env -> IO Switchboard-new env = do +new env = do   ctxEnvIORef <- newIORef Nothing   Switchboard     <$> forkIO (keepPrintingLog env)@@ -29,9 +30,9 @@     <*> forkIO (runReaderT Agda.start env)     <*> pure ctxEnvIORef --- | For sending reactions to the client +-- | For sending reactions to the client setupLanguageContextEnv :: Switchboard -> LanguageContextEnv Config -> IO ()-setupLanguageContextEnv switchboard ctxEnv = do +setupLanguageContextEnv switchboard ctxEnv = do   writeIORef (sbLanguageContextEnv switchboard) (Just ctxEnv)  destroy :: Switchboard -> IO ()@@ -56,7 +57,7 @@   response <- readChan (envResponseChan env)    result <- readIORef ctxEnvIORef-  forM_ result $ \ctxEnv -> do +  forM_ result $ \ctxEnv -> do     runLspT ctxEnv $ do       callback <- liftIO $ ResponseController.dispatch (envResponseController env)
+ stack-8.10-Agda-2.6.2.2.yaml view
@@ -0,0 +1,21 @@+resolver: lts-18.28+compiler: ghc-8.10.7+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor++packages:+- .++# Use some newer versions than in the lts-18.28 snapshot+extra-deps:+- Agda-2.6.2.2+- text-icu-0.8.0.1+- lsp-1.2.0.1+- lsp-types-1.3.0.1++flags:+  agda-language-server:+    Agda-2-6-2-2: true+  Agda:+    # optimise-heavily: true+    enable-cluster-counting: true
− stack-8.10.yaml 
@@ -1,19 +0,0 @@-resolver: lts-18.28-compiler: ghc-8.10.7-# Allow a newer minor version of GHC than the snapshot specifies-compiler-check: newer-minor--packages:-- .--# Use some newer versions than in the lts-18.28 snapshot-extra-deps:-- Agda-2.6.2.2-- text-icu-0.8.0.1-- lsp-1.2.0.1-- lsp-types-1.3.0.1--flags:-  Agda:-    # optimise-heavily: true-    enable-cluster-counting: true
+ stack-9.0-Agda-2.6.2.2.yaml view
@@ -0,0 +1,19 @@+resolver: lts-19.33+compiler: ghc-9.0.2+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor++packages:+- .++# Use some newer versions than in the lts-19.33 snapshot+extra-deps:+- text-icu-0.8.0.1+# - Agda-2.6.2.2  # This is the lts-19.33 version of Agda++flags:+  agda-language-server:+    Agda-2-6-2-2: true+  Agda:+    # optimise-heavily: true+    enable-cluster-counting: true
− stack-9.0.yaml 
@@ -1,16 +0,0 @@-resolver: lts-19.33-compiler: ghc-9.0.2-# Allow a newer minor version of GHC than the snapshot specifies-compiler-check: newer-minor--packages:-- .--# Use some newer versions than in the lts-19.33 snapshot-extra-deps:-- text-icu-0.8.0.1--flags:-  Agda:-    # optimise-heavily: true-    enable-cluster-counting: true
+ stack-9.2-Agda-2.6.2.2.yaml view
@@ -0,0 +1,17 @@+resolver: lts-20.26+compiler: ghc-9.2.8+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor++packages:+- .++extra-deps:+- Agda-2.6.2.2++flags:+  agda-language-server:+    Agda-2-6-2-2: true+  Agda:+    # optimise-heavily: true+    enable-cluster-counting: true
stack.yaml view
@@ -6,6 +6,9 @@ packages: - . +extra-deps:+- Agda-2.6.3+ flags:   Agda:     # optimise-heavily: true