@@ -36,6 +36,7 @@ import Ide.LocalBindings (bindings, mostSpecificSpan, holify)
36
36
import Ide.Plugin (mkLspCommand )
37
37
import Ide.Plugin.Tactic.Machinery
38
38
import Ide.Plugin.Tactic.Tactics
39
+ import Ide.Plugin.Tactic.Types
39
40
import Ide.TreeTransform (transform , graft , useAnnotatedSource )
40
41
import Ide.Types
41
42
import Language.Haskell.LSP.Core (clientCapabilities )
@@ -60,23 +61,10 @@ tacticDesc :: T.Text -> T.Text
60
61
tacticDesc name = " fill the hole using the " <> name <> " tactic"
61
62
62
63
------------------------------------------------------------------------------
63
- -- | The list of tactics exposed to the outside world. These are attached to
64
- -- actual tactics via 'commandTactic' and are contextually provided to the
65
- -- editor via 'commandProvider'.
66
- data TacticCommand
67
- = Auto
68
- | Split
69
- | Intro
70
- | Intros
71
- | Destruct
72
- | Homomorphism
73
- deriving (Eq , Ord , Show , Enum , Bounded )
74
-
75
64
76
65
enabledTactics :: [TacticCommand ]
77
66
enabledTactics = [Intros , Destruct , Homomorphism ]
78
67
79
-
80
68
------------------------------------------------------------------------------
81
69
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
82
70
-- UI.
@@ -94,18 +82,6 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
94
82
tcCommandName :: TacticCommand -> T. Text
95
83
tcCommandName = T. pack . show
96
84
97
-
98
- ------------------------------------------------------------------------------
99
- -- | Generate a title for the command.
100
- tacticTitle :: TacticCommand -> T. Text -> T. Text
101
- tacticTitle Auto _ = " Auto"
102
- tacticTitle Split _ = " Auto"
103
- tacticTitle Intro _ = " Intro"
104
- tacticTitle Intros _ = " Introduce lambda"
105
- tacticTitle Destruct var = " Case split on " <> var
106
- tacticTitle Homomorphism var = " Homomorphic case split on " <> var
107
-
108
-
109
85
------------------------------------------------------------------------------
110
86
-- | Mapping from tactic commands to their contextual providers. See 'provide',
111
87
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
0 commit comments