d634c32 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

@@ -14,6 +14,10 @@ New in 0.9.19:

14 compiler output

15* An interactive shell, similar to the prover, for running reflected elaborator

16 actions. Access it with :elab from the REPL.

17+* New command-line option --highlight that causes Idris to save highlighting

18+ information when successfully type checking. The information is in the same

19+ format sent by the IDE mode, and is saved in a file with the extension ".idh".

20+

17

21

18New in 0.9.18:

22New in 0.9.18:

19--------------

23--------------

src/Idris/AbsSyntax.hs+5

@@ -694,6 +694,11 @@ getCmdLine :: Idris [Opt]

694getCmdLine = do i <- getIState

695 return (opt_cmdline (idris_options i))

696

697+getDumpHighlighting :: Idris Bool

698+getDumpHighlighting = do ist <- getIState

699+ return (findC (opt_cmdline (idris_options ist)))

700+ where findC = elem DumpHighlights

701+

697getDumpDefun :: Idris (Maybe FilePath)

702getDumpDefun :: Idris (Maybe FilePath)

698getDumpDefun = do i <- getIState

703getDumpDefun = do i <- getIState

699 return $ findC (opt_cmdline (idris_options i))

704 return $ findC (opt_cmdline (idris_options i))

src/Idris/AbsSyntaxTree.hs+4−2

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

241 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance

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

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

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

245 }

246 }

246

247

247-- Required for parsers library, and therefore trifecta

248-- Required for parsers library, and therefore trifecta

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

329 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

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

330 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

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

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

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

333

334

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

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

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

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

@@ -484,6 +485,7 @@ data Opt = Filename String

484 | AutoWidth -- ^ Automatically adjust terminal width

485 | AutoWidth -- ^ Automatically adjust terminal width

485 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

486 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover

486 | UseConsoleWidth ConsoleWidth

487 | UseConsoleWidth ConsoleWidth

488+ | DumpHighlights

487 deriving (Show, Eq)

489 deriving (Show, Eq)

488

490

489data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

491data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm

src/Idris/CmdOptions.hs+1−1

@@ -141,7 +141,7 @@ parseFlags = many $

141 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

142

143 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

144−

144+ <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

145

146 where

147 getExt s = case maybeRead s of

src/Idris/IdeMode.hs+1−1

@@ -2,7 +2,7 @@

2

3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

4

5−module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

5+module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where

6

7import Text.Printf

8import Numeric

src/Idris/Output.hs+18−1

@@ -18,6 +18,7 @@ import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

18import System.Console.Haskeline.MonadException

19 (MonadException (controlIO), RunIO (RunIO))

20import System.IO (stdout, Handle, hPutStrLn)

21+import System.FilePath (replaceExtension)

21

22

22import Prelude hiding ((<$>))

23import Prelude hiding ((<$>))

23

24

@@ -198,7 +199,9 @@ sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

198sendHighlighting highlights =

199sendHighlighting highlights =

199 do ist <- getIState

200 do ist <- getIState

200 case idris_outputmode ist of

201 case idris_outputmode ist of

201− RawOutput _ -> return ()

202+ RawOutput _ -> updateIState $

203+ \ist -> ist { idris_highlightedRegions =

204+ highlights ++ idris_highlightedRegions ist }

202 IdeMode n h ->

205 IdeMode n h ->

203 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

206 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

204 | (fc, annot) <- highlights, fullFC fc

207 | (fc, annot) <- highlights, fullFC fc

@@ -213,6 +216,20 @@ sendHighlighting highlights =

213 where fullFC (FC _ _ _) = True

216 where fullFC (FC _ _ _) = True

214 fullFC _ = False

217 fullFC _ = False

215

218

219+-- | Write the highlighting information to a file, for use in external tools

220+-- or in editors that don't support the IDE protocol

221+writeHighlights :: FilePath -> Idris ()

222+writeHighlights f =

223+ do ist <- getIState

224+ let hs = reverse $ idris_highlightedRegions ist

225+ let hfile = replaceExtension f "idh"

226+ let annots = toSExp [ (fc, fancifyAnnots ist False annot)

227+ | (fc@(FC _ _ _), annot) <- hs

228+ ]

229+ runIO $ writeFile hfile $ sExpToString annots

230+

231+clearHighlights :: Idris ()

232+clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }

216

233

217renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

234renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

218renderExternal fmt width doc

235renderExternal fmt width doc

src/Idris/Parser.hs+8−3

@@ -1535,11 +1535,16 @@ loadSource lidr f toline

1535 Just docs -> addModDoc syntax mname docs

1536

1537

1538− -- Finally, write an ibc if checking was successful

1538+ -- Finally, write an ibc and highlights if checking was successful

1539 ok <- noErrors

1540 when ok $

1541− idrisCatch (do writeIBC f ibc; clearIBC)

1541+ do idrisCatch (do writeIBC f ibc; clearIBC)

1542− (\c -> return ()) -- failure is harmless

1542+ (\c -> return ()) -- failure is harmless

1543+ hl <- getDumpHighlighting

1544+ when hl $

1545+ idrisCatch (writeHighlights f)

1546+ (const $ return ()) -- failure is harmless

1547+ clearHighlights

1543 i <- getIState

1548 i <- getIState

1544 putIState (i { default_total = def_total,

1549 putIState (i { default_total = def_total,

1545 hide_list = [] })

1550 hide_list = [] })

src/Idris/REPL.hs+1−1

@@ -1615,7 +1615,7 @@ idrisMain opts =

1615 when (DefaultTotal `elem` opts) $ do i <- getIState

1616 putIState (i { default_total = True })

1617 setColourise $ not quiet && last ((not isWindows) : opt getColour opts)

1618−

1618+

1619

1620

1621 mapM_ addLangExt (opt getLanguageExt opts)