From fa3399bcbb2f40c8ca0c9aebdb9dfb9cd5ec0aac Mon Sep 17 00:00:00 2001
From: Daniil Maximov <daniil31415it@gmail.com>
Date: Fri, 16 Aug 2024 23:44:03 +0300
Subject: [PATCH] [ new ] add docs-for-type-of IDE command

---
 src/Idris/IDEMode/REPL.idr   |  6 +++++-
 src/Protocol/IDE/Command.idr | 30 ++++++++++++++++++++----------
 2 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr
index 06d3496a6e..80bd225377 100644
--- a/src/Idris/IDEMode/REPL.idr
+++ b/src/Idris/IDEMode/REPL.idr
@@ -199,6 +199,10 @@ process (MakeWith l n)
     = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN $ mkUserName n)))
 process (DocsFor n modeOpt)
     = replWrap $ Idris.REPL.process (Doc $ APTerm (PRef EmptyFC (UN $ mkUserName n)))
+process (DocsForTypeOf n modeOpt)
+    = do (REPL (TermChecked itm ity)) <- Idris.REPL.process $ (Check $ PRef replFC (UN $ mkUserName n))
+           | err => pure $ REPL $ REPLError (pretty0 $ show err)
+         process (DocsFor (prettyBy Syntax ity) modeOpt)
 process (Apropos n)
     = do todoCmd "apropros"
          pure $ REPL $ Printed emptyDoc
@@ -513,5 +517,5 @@ replIDE
          case res of
               REPL _ => printError $ reflow "Running idemode but output isn't"
               IDEMode _ inf outf => do
-                send outf (ProtocolVersion 2 1) -- TODO: Move this info somewhere more central
+                send outf (ProtocolVersion 2 2) -- TODO: Move this info somewhere more central
                 loop
diff --git a/src/Protocol/IDE/Command.idr b/src/Protocol/IDE/Command.idr
index ac537a0302..97f48624c8 100644
--- a/src/Protocol/IDE/Command.idr
+++ b/src/Protocol/IDE/Command.idr
@@ -40,6 +40,7 @@ data IDECommand
      | MakeCase Integer String
      | MakeWith Integer String
      | DocsFor String (Maybe DocMode)
+     | DocsForTypeOf String (Maybe DocMode)
      | Directive String
      | Apropos String
      | Metavariables Integer
@@ -56,6 +57,11 @@ data IDECommand
      | Version
      | GetOptions
 
+getDocModeOption : List SExp -> Maybe $ Maybe DocMode
+getDocModeOption [] = Just Nothing
+getDocModeOption [SymbolAtom "overview"] = Just $ Just Overview
+getDocModeOption [SymbolAtom "full"    ] = Just $ Just Full
+getDocModeOption _ = Nothing
 
 getIDECommand : SExp -> Maybe IDECommand
 getIDECommand (SExpList [SymbolAtom "interpret", StringAtom cmd])
@@ -106,14 +112,14 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
     = Just $ MakeCase l n
 getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
     = Just $ MakeWith l n
-getIDECommand (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
+getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
     = do -- Maybe monad
-         modeOpt <- case modeTail of
-                      []                      => Just Nothing
-                      [SymbolAtom "overview"] => Just $ Just Overview
-                      [SymbolAtom "full"    ] => Just $ Just Full
-                      _ => Nothing
+         modeOpt <- getDocModeOption modeTail
          Just $ DocsFor n modeOpt
+getIDECommand (SExpList (SymbolAtom "docs-for-type-of" :: StringAtom n :: modeTail))
+    = do -- Maybe monad
+         modeOpt <- getDocModeOption modeTail
+         Just $ DocsForTypeOf n modeOpt
 getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
     = Just $ Apropos n
 getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])
@@ -148,6 +154,11 @@ export
 FromSExpable IDECommand where
   fromSExp = getIDECommand
 
+getDocModeTail : Maybe DocMode -> List SExp
+getDocModeTail Nothing = []
+getDocModeTail (Just Overview) = [SymbolAtom "overview"]
+getDocModeTail (Just Full) = [SymbolAtom "full"]
+
 putIDECommand : IDECommand -> SExp
 putIDECommand (Interpret cmd)                 = (SExpList [SymbolAtom "interpret", StringAtom cmd])
 putIDECommand (LoadFile fname Nothing)        = (SExpList [SymbolAtom "load-file", StringAtom fname])
@@ -172,11 +183,10 @@ putIDECommand GenerateDefNext                 = SymbolAtom "generate-def-next"
 putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
 putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
 putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
-putIDECommand (DocsFor n modeOpt)             = let modeTail = case modeOpt of
-                                                                 Nothing       => []
-                                                                 Just Overview => [SymbolAtom "overview"]
-                                                                 Just Full     => [SymbolAtom "full"] in
+putIDECommand (DocsFor n modeOpt)             = let modeTail = getDocModeTail modeOpt in
                                                 (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
+putIDECommand (DocsForTypeOf n modeOpt)       = let modeTail = getDocModeTail modeOpt in
+                                                (SExpList (SymbolAtom "docs-for-type-of" :: StringAtom n :: modeTail))
 putIDECommand (Apropos n)                     = (SExpList [SymbolAtom "apropos", StringAtom n])
 putIDECommand (Metavariables n)               = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
 putIDECommand (WhoCalls n)                    = (SExpList [SymbolAtom "who-calls", StringAtom n])