diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 125995e992..2c95db5d61 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -136,8 +136,11 @@ properties :: Properties
, 'PropertyKey "max_use_ctor_actions" 'TInteger
, 'PropertyKey "timeout_duration" 'TInteger
, 'PropertyKey "auto_gas" 'TInteger
+ , 'PropertyKey "proofstate_styling" 'TBoolean
]
properties = emptyProperties
+ & defineBooleanProperty #proofstate_styling
+ "Should Wingman emit styling markup when showing metaprogram proof states?" True
& defineIntegerProperty #auto_gas
"The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." 4
& defineIntegerProperty #timeout_duration
@@ -162,6 +165,7 @@ getTacticConfig pId =
<$> usePropertyLsp #max_use_ctor_actions pId properties
<*> usePropertyLsp #timeout_duration pId properties
<*> usePropertyLsp #auto_gas pId properties
+ <*> usePropertyLsp #proofstate_styling pId properties
getIdeDynflags
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index 8ebf7a9d15..44b2a535c6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -8,14 +8,13 @@ module Wingman.Metaprogramming.Parser where
import qualified Control.Monad.Combinators.Expr as P
import qualified Control.Monad.Error.Class as E
-import Control.Monad.Reader (ask)
import Data.Functor
import Data.Maybe (listToMaybe)
import qualified Data.Text as T
import qualified Refinery.Tactic as R
import qualified Text.Megaparsec as P
import Wingman.Auto
-import Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext, getCurrentDefinitions)
+import Wingman.Machinery (useNameFromHypothesis, useNameFromContext, getCurrentDefinitions)
import Wingman.Metaprogramming.Lexer
import Wingman.Metaprogramming.Parser.Documentation
import Wingman.Metaprogramming.ProofState (proofState, layout)
@@ -454,7 +453,9 @@ attempt_it rsl ctx jdg program =
tt
pure $ case res of
Left tes -> Left $ wrapError $ show tes
- Right rtr -> Right $ layout $ proofState rtr
+ Right rtr -> Right
+ $ layout (cfg_proofstate_styling $ ctxConfig ctx)
+ $ proofState rtr
parseMetaprogram :: T.Text -> TacticsM ()
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
index 4bfa95cec8..5563b75c63 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
@@ -43,24 +43,26 @@ data Ann
forceMarkdownNewlines :: String -> String
forceMarkdownNewlines = unlines . fmap (<> " ") . lines
-layout :: Doc Ann -> String
-layout
+layout :: Bool -> Doc Ann -> String
+layout use_styling
= forceMarkdownNewlines
. T.unpack
. renderSimplyDecorated id
- renderAnn
- renderUnann
+ (renderAnn use_styling)
+ (renderUnann use_styling)
. layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)
-renderAnn :: Ann -> T.Text
-renderAnn Goal = ""
-renderAnn Hypoth = "```haskell\n"
-renderAnn Status = ""
-
-renderUnann :: Ann -> T.Text
-renderUnann Goal = ""
-renderUnann Hypoth = "\n```\n"
-renderUnann Status = ""
+renderAnn :: Bool -> Ann -> T.Text
+renderAnn False _ = ""
+renderAnn _ Goal = ""
+renderAnn _ Hypoth = "```haskell\n"
+renderAnn _ Status = ""
+
+renderUnann :: Bool -> Ann -> T.Text
+renderUnann False _ = ""
+renderUnann _ Goal = ""
+renderUnann _ Hypoth = "\n```\n"
+renderUnann _ Status = ""
proofState :: RunTacticResults -> Doc Ann
proofState RunTacticResults{rtr_subgoals} =
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 758d3e408c..6c8da524e3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -87,6 +87,7 @@ data Config = Config
{ cfg_max_use_ctor_actions :: Int
, cfg_timeout_seconds :: Int
, cfg_auto_gas :: Int
+ , cfg_proofstate_styling :: Bool
}
deriving (Eq, Ord, Show)
@@ -95,6 +96,7 @@ emptyConfig = Config
{ cfg_max_use_ctor_actions = 5
, cfg_timeout_seconds = 2
, cfg_auto_gas = 4
+ , cfg_proofstate_styling = True
}
------------------------------------------------------------------------------