Config option to suppress proofstate styling (#1966)

haskell · Jun 25, 2021 · 2915ae9 · 2915ae9
1 parent a1e7193
commit 2915ae9
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 16 deletions.
diff --git 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
@@ -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
@@ -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 = "<span style='color:#ef4026;'>"
-renderAnn Hypoth = "```haskell\n"
-renderAnn Status = "<span style='color:#6495ED;'>"
-
-renderUnann :: Ann -> T.Text
-renderUnann Goal = "</span>"
-renderUnann Hypoth = "\n```\n"
-renderUnann Status = "</span>"
+renderAnn :: Bool -> Ann -> T.Text
+renderAnn False _ = ""
+renderAnn _ Goal = "<span style='color:#ef4026;'>"
+renderAnn _ Hypoth = "```haskell\n"
+renderAnn _ Status = "<span style='color:#6495ED;'>"
+
+renderUnann :: Bool -> Ann -> T.Text
+renderUnann False _ = ""
+renderUnann _ Goal = "</span>"
+renderUnann _ Hypoth = "\n```\n"
+renderUnann _ Status = "</span>"
 
 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
@@ -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
   }
 
 ------------------------------------------------------------------------------