b709748 · Idris-dev · git.iko.soy

docs/reference/ide-protocol.rst+6

compare with master

unifiedsplit

@@ -177,6 +177,12 @@ The following keys are available:

177 ``link-href``

178 provides a URL that the corresponding text is a link to.

179

180+ ``quasiquotation``

181+ states that the region is quasiquoted.

182+

183+ ``antiquotation``

184+ states that the region is antiquoted.

185+

180 ``tt-term``

186 ``tt-term``

181 A serialized representation of the Idris core term corresponding to the region of text.

187 A serialized representation of the Idris core term corresponding to the region of text.

182

188

src/Idris/AbsSyntaxTree.hs+3−2

@@ -242,7 +242,8 @@ data IState = IState {

242 -- (instances appear twice; also as a funtion name)

243 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

244 idris_exports :: [Name], -- ^ Functions with ExportList

245− idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output

245+ idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output

246+ idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

246 }

247 }

247

248

248-- Required for parsers library, and therefore trifecta

249-- Required for parsers library, and therefore trifecta

@@ -330,7 +331,7 @@ idrisInit = IState initContext S.empty []

330 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

331 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

331 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

332 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

332 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

333 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

333− AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] []

334+ AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

334

335

335-- | The monad for the main REPL - reading and processing files and updating

336-- | The monad for the main REPL - reading and processing files and updating

336-- global state (hence the IO inner monad).

337-- global state (hence the IO inner monad).

src/Idris/Core/TT.hs+5−3

@@ -159,10 +159,10 @@ instance Show FC where

159 show (FileFC f) = f

160

161-- | Output annotation for pretty-printed name - decides colour

162−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving Show

162+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)

163

164-- | Text formatting output

165−data TextFormatting = BoldText | ItalicText | UnderlineText deriving Show

165+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)

166

167-- | Output annotations for pretty-printing

168data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -186,7 +186,9 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

186 -- resolved. If a file path is present, then

187 -- the namespace represents a module imported

188 -- from that file.

189+ | AnnQuasiquote

190+ | AnnAntiquote

189− deriving Show

191+ deriving (Show, Eq)

190

192

191-- | Used for error reflection

193-- | Used for error reflection

192data ErrorReportPart = TextPart String

194data ErrorReportPart = TextPart String

src/Idris/IdeMode.hs+2

@@ -163,6 +163,8 @@ instance SExpable OutputAnnotation where

163 toSExp $ [(SymbolAtom "namespace", StringAtom (intercalate "." (map T.unpack ns)))] ++

164 [(SymbolAtom "decor", SymbolAtom $ if isJust file then "module" else "namespace")] ++

165 maybeProps [("source-file", file)]

166+ toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]

167+ toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]

166

168

167encodeTerm :: [(Name, Bool)] -> Term -> String

169encodeTerm :: [(Name, Bool)] -> Term -> String

168encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

170encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

src/Idris/Output.hs+13

@@ -196,6 +196,15 @@ prettyDocumentedIst ist (name, ty, docs) =

196 where ppTm = pprintDelab ist

197 norm = normaliseAll (tt_ctxt ist) []

198

199+sendParserHighlighting :: Idris ()

200+sendParserHighlighting =

201+ do ist <- getIState

202+ let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist

203+ sendHighlighting hs

204+ putIState ist {idris_parserHighlights = []}

205+ where wrap (fc, a) = (FC' fc, a)

206+ unwrap (fc', a) = (unwrapFC fc', a)

207+

199sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

208sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

200sendHighlighting highlights =

209sendHighlighting highlights =

201 do ist <- getIState

210 do ist <- getIState

@@ -276,6 +285,8 @@ renderExternal fmt width doc

276 decorate HTMLOutput (AnnNamespace _ _) = id

285 decorate HTMLOutput (AnnNamespace _ _) = id

277 decorate HTMLOutput (AnnLink url) =

286 decorate HTMLOutput (AnnLink url) =

278 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"

287 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"

288+ decorate HTMLOutput AnnQuasiquote = id

289+ decorate HTMLOutput AnnAntiquote = id

279

290

280 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

291 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

281 latex "IdrisType"

292 latex "IdrisType"

@@ -305,6 +316,8 @@ renderExternal fmt width doc

305 decorate LaTeXOutput (AnnErr _) = id

316 decorate LaTeXOutput (AnnErr _) = id

306 decorate LaTeXOutput (AnnNamespace _ _) = id

317 decorate LaTeXOutput (AnnNamespace _ _) = id

307 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")

318 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")

319+ decorate LaTeXOutput AnnQuasiquote = id

320+ decorate LaTeXOutput AnnAntiquote = id

308

321

309 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

322 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

310 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

323 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

src/Idris/ParseExpr.hs+20−9

@@ -147,14 +147,17 @@ extension syn ns rules =

147 ruleGroup _ _ = False

148

149 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

150− extensionSymbol (Keyword n) = do reserved (show n); return Nothing

150+ extensionSymbol (Keyword n) = do fc <- reservedFC (show n)

151+ highlightP fc AnnKeyword

152+ return Nothing

151 extensionSymbol (Expr n) = do tm <- expr syn

153 extensionSymbol (Expr n) = do tm <- expr syn

152 return $ Just (n, SynTm tm)

154 return $ Just (n, SynTm tm)

153 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

155 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

154 return $ Just (n, SynTm tm)

156 return $ Just (n, SynTm tm)

155 extensionSymbol (Binding n) = do b <- fst <$> name

157 extensionSymbol (Binding n) = do b <- fst <$> name

156 return $ Just (n, SynBind b)

158 return $ Just (n, SynBind b)

157− extensionSymbol (Symbol s) = do symbol s

159+ extensionSymbol (Symbol s) = do fc <- symbolFC s

160+ highlightP fc AnnKeyword

158 return Nothing

161 return Nothing

159 dropn :: Name -> [(Name, a)] -> [(Name, a)]

162 dropn :: Name -> [(Name, a)] -> [(Name, a)]

160 dropn n [] = []

163 dropn n [] = []

@@ -645,14 +648,19 @@ constraintArg syn = do symbol "@{"

645

648

646-}

649-}

647quasiquote :: SyntaxInfo -> IdrisParser PTerm

650quasiquote :: SyntaxInfo -> IdrisParser PTerm

648−quasiquote syn = do symbol "`("

651+quasiquote syn = do startFC <- symbolFC "`("

649 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,

652 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,

650 inPattern = False }

653 inPattern = False }

651− g <- optional $ do

654+ g <- optional $

652− symbol ":"

655+ do fc <- symbolFC ":"

653− expr syn { inPattern = False } -- don't allow antiquotes

656+ ty <- expr syn { inPattern = False } -- don't allow antiquotes

654− symbol ")"

657+ return (ty, fc)

658+ endFC <- symbolFC ")"

659+ mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]

660+ case g of

661+ Just (_, fc) -> highlightP fc AnnKeyword

662+ _ -> return ()

655− return $ PQuasiquote e g

663+ return $ PQuasiquote e (fst <$> g)

656 <?> "quasiquotation"

664 <?> "quasiquotation"

657

665

658{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

666{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

@@ -662,8 +670,11 @@ quasiquote syn = do symbol "`("

662-}

670-}

663unquote :: SyntaxInfo -> IdrisParser PTerm

671unquote :: SyntaxInfo -> IdrisParser PTerm

664unquote syn = do guard (syn_in_quasiquote syn > 0)

672unquote syn = do guard (syn_in_quasiquote syn > 0)

665− symbol "~"

673+ startFC <- symbolFC "~"

666 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }

674 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }

675+ endFC <- getFC

676+ highlightP startFC AnnKeyword

677+ highlightP (spanFC startFC endFC) AnnAntiquote

667 return $ PUnquote e

678 return $ PUnquote e

668 <?> "unquotation"

679 <?> "unquotation"

669

680

src/Idris/ParseHelpers.hs+9

@@ -79,6 +79,10 @@ runparser p i inputname =

79 parseString (runInnerParser (evalStateT p i))

80 (Directed (UTF8.fromString inputname) 0 0 0 0)

81

82+highlightP :: FC -> OutputAnnotation -> IdrisParser ()

83+highlightP fc annot = do ist <- get

84+ put ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist}

85+

82noDocCommentHere :: String -> IdrisParser ()

86noDocCommentHere :: String -> IdrisParser ()

83noDocCommentHere msg =

87noDocCommentHere msg =

84 optional (do fc <- getFC

88 optional (do fc <- getFC

@@ -260,6 +264,11 @@ lchar = token . char

260symbol :: MonadicParsing m => String -> m String

264symbol :: MonadicParsing m => String -> m String

261symbol = Tok.symbol

265symbol = Tok.symbol

262

266

267+symbolFC :: MonadicParsing m => String -> m FC

268+symbolFC str = do (FC file (l, c) _) <- getFC

269+ Tok.symbol str

270+ return $ FC file (l, c) (l, c + length str)

271+

263-- | Parses a reserved identifier

272-- | Parses a reserved identifier

264reserved :: MonadicParsing m => String -> m ()

273reserved :: MonadicParsing m => String -> m ()

265reserved = Tok.reserve idrisStyle

274reserved = Tok.reserve idrisStyle

src/Idris/Parser.hs+4−1

@@ -98,7 +98,8 @@ import System.IO

98moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

99moduleHeader = try (do docs <- optional docComment

100 noArgs docs

101− reserved "module"

101+ modFC <- reservedFC "module"

102+ highlightP modFC AnnKeyword

102 (i, ifc) <- identifier

103 (i, ifc) <- identifier

103 option ';' (lchar ';')

104 option ';' (lchar ';')

104 let modName = moduleName i

105 let modName = moduleName i

@@ -1430,6 +1431,7 @@ loadSource lidr f toline

1430 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1431 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1431 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1432 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1432 reportParserWarnings

1433 reportParserWarnings

1434+ sendParserHighlighting

1433

1435

1434 -- process and check module aliases

1436 -- process and check module aliases

1435 let modAliases = M.fromList

1437 let modAliases = M.fromList

@@ -1480,6 +1482,7 @@ loadSource lidr f toline

1480 ibc_write ist

1482 ibc_write ist

1481 }

1483 }

1482 _ -> return ()

1484 _ -> return ()

1485+ sendParserHighlighting

1483

1486

1484 -- Parsing done, now process declarations

1487 -- Parsing done, now process declarations

1485

1488