d634c32 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2395 from david-christiansen/highlight-file

Dump highlighting info

commitd634c32bfa9dda884fcc66058aea0a1681696310 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 24 Jun 2015, 18:11 (11 years ago) parenta3407cb 0280b22

8 files changed+42−9

compare with master

unifiedsplit

CHANGELOG+4 src/Idris/AbsSyntax.hs+5 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/CmdOptions.hs+1−1 src/Idris/IdeMode.hs+1−1 src/Idris/Output.hs+18−1 src/Idris/Parser.hs+8−3 src/Idris/REPL.hs+1−1

CHANGELOG+4

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

1414 compiler output

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

1616 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+

1721

1822New in 0.9.18:

1923--------------

src/Idris/AbsSyntax.hs+5

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

694694getCmdLine = do i <- getIState

695695 return (opt_cmdline (idris_options i))

696696

697+getDumpHighlighting :: Idris Bool

698+getDumpHighlighting = do ist <- getIState

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

700+ where findC = elem DumpHighlights

701+

697702getDumpDefun :: Idris (Maybe FilePath)

698703getDumpDefun = do i <- getIState

699704 return $ findC (opt_cmdline (idris_options i))

src/Idris/AbsSyntaxTree.hs+4−2

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

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

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

243243 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

245246 }

246247

247248-- Required for parsers library, and therefore trifecta

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

329330 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

330331 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

331332 (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 [] []

333334

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

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

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

484485 | AutoWidth -- ^ Automatically adjust terminal width

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

486487 | UseConsoleWidth ConsoleWidth

488+ | DumpHighlights

487489 deriving (Show, Eq)

488490

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

src/Idris/CmdOptions.hs+1−1

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

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

142142

143143 <|> (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")

145145

146146 where

147147 getExt s = case maybeRead s of

src/Idris/IdeMode.hs+1−1

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

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

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

77import Text.Printf

88import Numeric

src/Idris/Output.hs+18−1

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

1818import System.Console.Haskeline.MonadException

1919 (MonadException (controlIO), RunIO (RunIO))

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

21+import System.FilePath (replaceExtension)

2122

2223import Prelude hiding ((<$>))

2324

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

198199sendHighlighting highlights =

199200 do ist <- getIState

200201 case idris_outputmode ist of

201− RawOutput _ -> return ()

202+ RawOutput _ -> updateIState $

203+ \ist -> ist { idris_highlightedRegions =

204+ highlights ++ idris_highlightedRegions ist }

202205 IdeMode n h ->

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

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

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

213216 where fullFC (FC _ _ _) = True

214217 fullFC _ = False

215218

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 = [] }

216233

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

218235renderExternal fmt width doc

src/Idris/Parser.hs+8−3

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

15351535 Just docs -> addModDoc syntax mname docs

15361536

15371537

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

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

15391539 ok <- noErrors

15401540 when ok $

1541− idrisCatch (do writeIBC f ibc; clearIBC)

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

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

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

1543+ hl <- getDumpHighlighting

1544+ when hl $

1545+ idrisCatch (writeHighlights f)

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

1547+ clearHighlights

15431548 i <- getIState

15441549 putIState (i { default_total = def_total,

15451550 hide_list = [] })

src/Idris/REPL.hs+1−1

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

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

16161616 putIState (i { default_total = True })

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

1618−

1618+

16191619

16201620

16211621 mapM_ addLangExt (opt getLanguageExt opts)