From 502e81dd7e65ce3547eb51dcfd35d5d47b12505b Mon Sep 17 00:00:00 2001 From: Vince Date: Tue, 20 Feb 2024 17:08:06 +0800 Subject: [PATCH] add concreteProgram as a field to data LoadedProgram --- src/Server/Handler2/CustomMethod/Refine.hs | 3 ++- src/Server/Handler2/CustomMethod/Reload.hs | 3 ++- src/Server/Monad.hs | 4 +++- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Server/Handler2/CustomMethod/Refine.hs b/src/Server/Handler2/CustomMethod/Refine.hs index 79608576..21f57d23 100644 --- a/src/Server/Handler2/CustomMethod/Refine.hs +++ b/src/Server/Handler2/CustomMethod/Refine.hs @@ -35,7 +35,8 @@ handler specRange filledText = do refine :: LoadedProgram -> Range -> Text -> (LoadedProgram, Maybe Range) refine loadedProgram specRange filledText = LoadedProgram - { _highlightingInfos = _ + { _concreteProgram = _ + , _highlightingInfos = _ , _abstractProgram = _ , _scopingInfo = _ , _typeCheckingInfo = _ diff --git a/src/Server/Handler2/CustomMethod/Reload.hs b/src/Server/Handler2/CustomMethod/Reload.hs index 6ca045fc..5222085a 100644 --- a/src/Server/Handler2/CustomMethod/Reload.hs +++ b/src/Server/Handler2/CustomMethod/Reload.hs @@ -71,7 +71,8 @@ reload filepath onFinish onError = do Right (pos, specs, warnings, redexes, counter) -> do -- cache all results loadedProgram <- cacheProgram filepath LoadedProgram - { _highlightingInfos = collectHighlighting concrete + { _concreteProgram = concrete + , _highlightingInfos = collectHighlighting concrete , _abstractProgram = abstract , _scopingInfo = collectLocationLinks abstract , _typeCheckingInfo = collectHoverInfo abstract scopeTree diff --git a/src/Server/Monad.hs b/src/Server/Monad.hs index 85182f31..f8e63c3a 100644 --- a/src/Server/Monad.hs +++ b/src/Server/Monad.hs @@ -55,6 +55,7 @@ import qualified Server.SrcLoc as SrcLoc import GCL.WP.Type (StructWarning) import Server.IntervalMap (IntervalMap) import Syntax.Abstract as A +import Syntax.Concrete as C import GCL.Predicate (PO, Spec) import Data.IntMap (IntMap) @@ -151,7 +152,8 @@ data GlobalEnv = GlobalEnv } data LoadedProgram = LoadedProgram - { _highlightingInfos :: [J.SemanticTokenAbsolute] + { _concreteProgram :: C.Program + , _highlightingInfos :: [J.SemanticTokenAbsolute] , _abstractProgram :: A.Program , _scopingInfo :: IntervalMap J.LocationLink , _typeCheckingInfo :: IntervalMap (J.Hover, A.Type)