{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module Yi.Mode.Abella
( abellaModeEmacs
, abella
, abellaEval
, abellaEvalFromProofPoint
, abellaUndo
, abellaGet
, abellaSend
) where
import Lens.Micro.Platform (use, (%~), (&), (.=), (.~))
import Control.Monad (join, when)
import Data.Binary (Binary)
import Data.Char (isSpace)
import Data.Default (Default)
import Data.Maybe (isJust)
import qualified Data.Text as T (isInfixOf, snoc, unpack)
import Data.Typeable (Typeable)
import Yi.Buffer
import Yi.Core (sendToProcess)
import Yi.Editor
import Yi.Keymap (YiM, topKeymapA)
import Yi.Keymap.Keys (Event, choice, ctrlCh, (<||), (?*>>!))
import qualified Yi.Lexer.Abella as Abella (Token, lexer)
import Yi.MiniBuffer (CommandArguments (..))
import qualified Yi.Mode.Interactive as Interactive (spawnProcess)
import Yi.Mode.Common (TokenBasedMode, anyExtension, styleMode)
import qualified Yi.Rope as R (YiString, toText)
import Yi.Types (YiVariable)
abellaModeGen :: (Char -> [Event]) -> TokenBasedMode Abella.Token
abellaModeGen :: (Char -> [Event]) -> TokenBasedMode Token
abellaModeGen Char -> [Event]
abellaBinding = StyleLexer AlexState HlState Token AlexInput
-> TokenBasedMode Token
forall (l :: * -> *) s t i.
Show (l s) =>
StyleLexer l s t i -> TokenBasedMode t
styleMode StyleLexer AlexState HlState Token AlexInput
Abella.lexer
TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& (Text -> Identity Text)
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax. Lens' (Mode syntax) Text
modeNameA ((Text -> Identity Text)
-> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> Text -> TokenBasedMode Token -> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Text
"abella"
TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& ((String -> YiString -> Bool)
-> Identity (String -> YiString -> Bool))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax. Lens' (Mode syntax) (String -> YiString -> Bool)
modeAppliesA (((String -> YiString -> Bool)
-> Identity (String -> YiString -> Bool))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> (String -> YiString -> Bool)
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [String] -> String -> YiString -> Bool
forall a. [String] -> String -> a -> Bool
anyExtension [String
"thm"]
TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& (Maybe (BufferM ()) -> Identity (Maybe (BufferM ())))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax. Lens' (Mode syntax) (Maybe (BufferM ()))
modeToggleCommentSelectionA ((Maybe (BufferM ()) -> Identity (Maybe (BufferM ())))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> Maybe (BufferM ())
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ BufferM () -> Maybe (BufferM ())
forall a. a -> Maybe a
Just (YiString -> BufferM ()
toggleCommentB YiString
"%")
TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& ((KeymapSet -> KeymapSet) -> Identity (KeymapSet -> KeymapSet))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax. Lens' (Mode syntax) (KeymapSet -> KeymapSet)
modeKeymapA (((KeymapSet -> KeymapSet) -> Identity (KeymapSet -> KeymapSet))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> (KeymapSet -> KeymapSet)
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Keymap -> Identity Keymap) -> KeymapSet -> Identity KeymapSet
Lens' KeymapSet Keymap
topKeymapA ((Keymap -> Identity Keymap) -> KeymapSet -> Identity KeymapSet)
-> (Keymap -> Keymap) -> KeymapSet -> KeymapSet
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Keymap -> Keymap -> Keymap
forall (f :: * -> *) w e a.
MonadInteract f w e =>
f a -> f a -> f a
(<||)
([Keymap] -> Keymap
forall (m :: * -> *) w e a.
(MonadInteract m w e, MonadFail m) =>
[m a] -> m a
choice
[ Char -> [Event]
abellaBinding Char
'p' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaUndo
, Char -> [Event]
abellaBinding Char
'e' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaEval
, Char -> [Event]
abellaBinding Char
'n' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaNext
, Char -> [Event]
abellaBinding Char
'a' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaAbort
, Char -> [Event]
abellaBinding Char
'\r' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaEvalFromProofPoint
])
abellaModeEmacs :: TokenBasedMode Abella.Token
abellaModeEmacs :: TokenBasedMode Token
abellaModeEmacs = (Char -> [Event]) -> TokenBasedMode Token
abellaModeGen (\Char
ch -> [Char -> Event
ctrlCh Char
'c', Char -> Event
ctrlCh Char
ch])
newtype AbellaBuffer = AbellaBuffer {AbellaBuffer -> Maybe BufferRef
_abellaBuffer :: Maybe BufferRef}
deriving (AbellaBuffer
AbellaBuffer -> Default AbellaBuffer
forall a. a -> Default a
def :: AbellaBuffer
$cdef :: AbellaBuffer
Default, Typeable, Get AbellaBuffer
[AbellaBuffer] -> Put
AbellaBuffer -> Put
(AbellaBuffer -> Put)
-> Get AbellaBuffer
-> ([AbellaBuffer] -> Put)
-> Binary AbellaBuffer
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [AbellaBuffer] -> Put
$cputList :: [AbellaBuffer] -> Put
get :: Get AbellaBuffer
$cget :: Get AbellaBuffer
put :: AbellaBuffer -> Put
$cput :: AbellaBuffer -> Put
Binary)
instance YiVariable AbellaBuffer
getProofPointMark :: BufferM Mark
getProofPointMark :: BufferM Mark
getProofPointMark = Maybe String -> BufferM Mark
getMarkB (Maybe String -> BufferM Mark) -> Maybe String -> BufferM Mark
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"p"
getTheoremPointMark :: BufferM Mark
getTheoremPointMark :: BufferM Mark
getTheoremPointMark = Maybe String -> BufferM Mark
getMarkB (Maybe String -> BufferM Mark) -> Maybe String -> BufferM Mark
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"t"
abellaEval :: YiM ()
abellaEval :: YiM ()
abellaEval = do
YiString
reg <- BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM YiString -> YiM YiString)
-> (BufferM YiString -> BufferM YiString)
-> BufferM YiString
-> YiM YiString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BufferM YiString -> BufferM YiString
forall a. BufferM a -> BufferM a
savingPointB (BufferM YiString -> YiM YiString)
-> BufferM YiString -> YiM YiString
forall a b. (a -> b) -> a -> b
$ do
BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
BufferM ()
leftB
Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> BufferM Region -> BufferM YiString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TextUnit -> BufferM Region
regionOfNonEmptyB TextUnit
unitSentence
YiString -> YiM ()
abellaSend YiString
reg
abellaEvalFromProofPoint :: YiM ()
abellaEvalFromProofPoint :: YiM ()
abellaEvalFromProofPoint = YiString -> YiM ()
abellaSend (YiString -> YiM ()) -> YiM YiString -> YiM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer BufferM YiString
f
where f :: BufferM YiString
f = do Mark
mark <- BufferM Mark
getProofPointMark
Point
p <- Getting Point FBuffer Point -> BufferM Point
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Getting Point FBuffer Point -> BufferM Point)
-> Getting Point FBuffer Point -> BufferM Point
forall a b. (a -> b) -> a -> b
$ Mark -> Getting Point FBuffer Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA Mark
mark
Point
cur <- BufferM Point
pointB
Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA Mark
mark ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Point
cur
Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> Region -> BufferM YiString
forall a b. (a -> b) -> a -> b
$ Point -> Point -> Region
mkRegion Point
p Point
cur
abellaNext :: YiM ()
abellaNext :: YiM ()
abellaNext = do
YiString
reg <- BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM YiString -> YiM YiString)
-> BufferM YiString -> YiM YiString
forall a b. (a -> b) -> a -> b
$ BufferM ()
rightB BufferM () -> BufferM YiString -> BufferM YiString
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> BufferM Region -> BufferM YiString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TextUnit -> BufferM Region
regionOfNonEmptyB TextUnit
unitSentence)
YiString -> YiM ()
abellaSend YiString
reg
BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
TextUnit -> Direction -> BufferM ()
moveB TextUnit
unitSentence Direction
Forward
BufferM ()
rightB
BufferM Bool -> BufferM () -> BufferM ()
forall a. BufferM Bool -> BufferM a -> BufferM ()
untilB_ (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace (Char -> Bool) -> BufferM Char -> BufferM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Char
readB) BufferM ()
rightB
BufferM Bool -> BufferM () -> BufferM ()
forall a. BufferM Bool -> BufferM a -> BufferM ()
untilB_ ((Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') (Char -> Bool) -> BufferM Char -> BufferM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Char
readB) (BufferM () -> BufferM ()) -> BufferM () -> BufferM ()
forall a b. (a -> b) -> a -> b
$ BufferM ()
moveToEol BufferM () -> BufferM () -> BufferM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BufferM ()
rightB BufferM () -> BufferM () -> BufferM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BufferM ()
firstNonSpaceB
BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
abellaUndo :: YiM ()
abellaUndo :: YiM ()
abellaUndo = do
YiString -> YiM ()
abellaSend YiString
"undo."
BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
TextUnit -> Direction -> BufferM ()
moveB TextUnit
unitSentence Direction
Backward
BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
abellaAbort :: YiM ()
abellaAbort :: YiM ()
abellaAbort = do
YiString -> YiM ()
abellaSend YiString
"abort."
BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
Point -> BufferM ()
moveTo (Point -> BufferM ()) -> BufferM Point -> BufferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Getting Point FBuffer Point -> BufferM Point
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Getting Point FBuffer Point -> BufferM Point)
-> (Mark -> Getting Point FBuffer Point) -> Mark -> BufferM Point
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> Getting Point FBuffer Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> BufferM Point) -> BufferM Mark -> BufferM Point
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BufferM Mark
getTheoremPointMark
BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
abella :: CommandArguments -> YiM BufferRef
abella :: CommandArguments -> YiM BufferRef
abella (CommandArguments [Text]
args) = do
BufferRef
b <- String -> [String] -> YiM BufferRef
Interactive.spawnProcess String
"abella" (Text -> String
T.unpack (Text -> String) -> [Text] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
args)
EditorM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor (EditorM () -> YiM ())
-> (Maybe BufferRef -> EditorM ()) -> Maybe BufferRef -> YiM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbellaBuffer -> EditorM ()
forall (m :: * -> *) a.
(MonadEditor m, YiVariable a, Functor m) =>
a -> m ()
putEditorDyn (AbellaBuffer -> EditorM ())
-> (Maybe BufferRef -> AbellaBuffer)
-> Maybe BufferRef
-> EditorM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe BufferRef -> AbellaBuffer
AbellaBuffer (Maybe BufferRef -> YiM ()) -> Maybe BufferRef -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferRef -> Maybe BufferRef
forall a. a -> Maybe a
Just BufferRef
b
BufferRef -> YiM BufferRef
forall (m :: * -> *) a. Monad m => a -> m a
return BufferRef
b
abellaGet :: YiM BufferRef
abellaGet :: YiM BufferRef
abellaGet = YiM BufferRef -> YiM BufferRef
forall (m :: * -> *) a. MonadEditor m => m a -> m a
withOtherWindow (YiM BufferRef -> YiM BufferRef) -> YiM BufferRef -> YiM BufferRef
forall a b. (a -> b) -> a -> b
$ do
AbellaBuffer Maybe BufferRef
mb <- EditorM AbellaBuffer -> YiM AbellaBuffer
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor EditorM AbellaBuffer
forall (m :: * -> *) a.
(MonadEditor m, YiVariable a, Default a, Functor m) =>
m a
getEditorDyn
case Maybe BufferRef
mb of
Maybe BufferRef
Nothing -> CommandArguments -> YiM BufferRef
abella ([Text] -> CommandArguments
CommandArguments [])
Just BufferRef
b -> do
Bool
stillExists <- Maybe FBuffer -> Bool
forall a. Maybe a -> Bool
isJust (Maybe FBuffer -> Bool) -> YiM (Maybe FBuffer) -> YiM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferRef -> YiM (Maybe FBuffer)
forall (m :: * -> *).
MonadEditor m =>
BufferRef -> m (Maybe FBuffer)
findBuffer BufferRef
b
if Bool
stillExists
then do EditorM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor (EditorM () -> YiM ()) -> EditorM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferRef -> EditorM ()
switchToBufferE BufferRef
b
BufferRef -> YiM BufferRef
forall (m :: * -> *) a. Monad m => a -> m a
return BufferRef
b
else CommandArguments -> YiM BufferRef
abella ([Text] -> CommandArguments
CommandArguments [])
abellaSend :: R.YiString -> YiM ()
abellaSend :: YiString -> YiM ()
abellaSend YiString
cmd' = do
let cmd :: Text
cmd = YiString -> Text
R.toText YiString
cmd'
Bool -> YiM () -> YiM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text
"Theorem" Text -> Text -> Bool
`T.isInfixOf` Text
cmd) (YiM () -> YiM ()) -> YiM () -> YiM ()
forall a b. (a -> b) -> a -> b
$
BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getTheoremPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
BufferRef
b <- YiM BufferRef
abellaGet
BufferRef -> BufferM () -> YiM ()
forall (m :: * -> *) a.
MonadEditor m =>
BufferRef -> BufferM a -> m a
withGivenBuffer BufferRef
b BufferM ()
botB
BufferRef -> String -> YiM ()
sendToProcess BufferRef
b (String -> YiM ()) -> (Text -> String) -> Text -> YiM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> YiM ()) -> Text -> YiM ()
forall a b. (a -> b) -> a -> b
$ Text
cmd Text -> Char -> Text
`T.snoc` Char
'\n'