Skip to content

Commit

Permalink
refactor handlerReload
Browse files Browse the repository at this point in the history
  • Loading branch information
B04902047 committed Feb 20, 2024
1 parent ecde58c commit 289b27f
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 27 deletions.
1 change: 0 additions & 1 deletion src/Server/Handler/CustomMethod.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ import Syntax.Abstract.Util ( programToScopeForSubstitution

import qualified Language.LSP.Types as J
import Data.String (IsString(fromString))
import Language.LSP.Types (Diagnostic(Diagnostic))
import Server.Handler.Diagnostic (makeDiagnostic)


Expand Down
57 changes: 32 additions & 25 deletions src/Server/Handler2/CustomMethod.hs
Original file line number Diff line number Diff line change
Expand Up @@ -118,9 +118,9 @@ rangeAfterReplacedWithHelloWorld range =

-- Reload --

handleReload :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
handleReload filepath onFinsih onError = do
-- load source
reload :: FilePath -> (LoadedProgram -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
reload filepath onFinish onError = do
-- load source
maybeSource <- getSource filepath
case maybeSource of
Nothing -> onError (CannotReadFile filepath)
Expand All @@ -140,32 +140,34 @@ handleReload filepath onFinsih onError = do
Left err -> onError (StructError err)
Right (pos, specs, warnings, redexes, counter) -> do
-- cache all results
cacheProgram filepath LoadedProgram
loadedProgram <- cacheProgram filepath LoadedProgram
{ _highlightingInfos = collectHighlighting concrete
, _abstractProgram = abstract
, _scopingInfo = collectLocationLinks abstract
, _typeCheckingInfo = collectHoverInfo abstract scopeTree
, _proofObligations = List.sort pos
, _specifiations = sortOn locOf specs
, _warnings = warnings
, _redexes = redexes
, _variableCounter = counter
, _abstractProgram = abstract
, _scopingInfo = collectLocationLinks abstract
, _typeCheckingInfo = collectHoverInfo abstract scopeTree
, _proofObligations = List.sort pos
, _specifiations = sortOn locOf specs
, _warnings = warnings
, _redexes = redexes
, _variableCounter = counter
}
-- send warnings as diagnostics
let diagnostics = concatMap collect warnings
sendDiagnostics filepath diagnostics

-- send all hints as reponses for client to render
let (A.Program _ _ globalProperties _ _) = abstract
version' <- bumpVersion
let response :: [ResKind] =
hintsToResponseBody
version'
Nothing
(globalProperties, List.sort pos, sortOn locOf specs, warnings, redexes, counter)
onFinsih response
onFinish loadedProgram
) onError

handleReload :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM ()
handleReload filepath onFinsih onError = do
reload filepath (\loadedProgram -> do
-- send warnings as diagnostics
let warnings = _warnings loadedProgram
let diagnostics = concatMap collect warnings
sendDiagnostics filepath diagnostics

-- send all hints as reponses for client to render
version' <- bumpVersion
let response = loadedProgramToReponse loadedProgram version' Nothing
onFinsih response
) onError

parse :: FilePath -> Text -> Either Error C.Program
parse filepath source =
case Parser.scanAndParse Parser.program filepath source of
Expand Down Expand Up @@ -199,6 +201,11 @@ typeCheck abstract = do
Left e -> Left (TypeError e)
Right (_, scopeTree) -> return scopeTree

loadedProgramToReponse :: LoadedProgram -> Int -> Maybe Range -> [ResKind]
loadedProgramToReponse loadedProgram@(LoadedProgram _ abstract@(A.Abstract _ globalProperties _) _ _ proofObligations specs warnings _ _)
version rangeToInspect
= _

hintsToResponseBody :: Int -> Maybe Range -> ([Expr], [PO], [Spec], [StructWarning], IntMap (Int, A.Expr), Int) -> [ResKind]
hintsToResponseBody version rangeToInspect _hints@(globalProperties, proofObligations, specs, warnings, redexes, counter) =
[ ResMarkPOs rangesOfPOs
Expand Down
3 changes: 2 additions & 1 deletion src/Server/Handler2/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,10 +61,11 @@ editText range textToReplace onSuccess = do
_newText = textToReplace
}

cacheProgram :: FilePath -> LoadedProgram -> ServerM ()
cacheProgram :: FilePath -> LoadedProgram -> ServerM LoadedProgram
cacheProgram filepath loadedProgram = do
ref <- lift $ asks loadedPrograms
liftIO $ modifyIORef' ref (Map.insert filepath loadedProgram)
return loadedProgram

dumpProgram :: FilePath -> ServerM (Maybe LoadedProgram)
dumpProgram filepath = do
Expand Down

0 comments on commit 289b27f

Please sign in to comment.