c0342c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add command line option to control REPL colours

c0342c7David Christiansen13 years ago

src/Idris/AbsSyntax.hs+4

compare with master

unifiedsplit

@@ -481,6 +481,10 @@ allImportDirs :: IState -> Idris [FilePath]

481allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

482 return ("." : reverse optdirs)

483

484+colourise :: Idris Bool

485+colourise = do i <- getIState

486+ return $ idris_colourRepl i

487+

484impShow :: Idris Bool

488impShow :: Idris Bool

485impShow = do i <- getIState

489impShow = do i <- getIState

486 return (opt_showimp (idris_options i))

490 return (opt_showimp (idris_options i))

src/Idris/AbsSyntaxTree.hs+6−3

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

120 compiled_so :: Maybe String,

121 idris_dynamic_libs :: [DynamicLib],

122 idris_language_extensions :: [LanguageExt],

123− idris_outputmode :: OutputMode

123+ idris_outputmode :: OutputMode,

124+ idris_colourRepl :: Bool

124 }

125 }

125

126

126data SizeChange = Smaller | Same | Bigger | Unknown

127data SizeChange = Smaller | Same | Bigger | Unknown

@@ -177,6 +178,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

177 emptyContext emptyContext emptyContext emptyContext

178 emptyContext emptyContext emptyContext emptyContext

178 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

179 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

179 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

180 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

181+ True

180

182

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

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

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

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

@@ -235,6 +237,7 @@ data Opt = Filename String

235 | Ver

237 | Ver

236 | Usage

238 | Usage

237 | Quiet

239 | Quiet

240+ | ColourREPL Bool

238 | Ideslave

241 | Ideslave

239 | ShowLibs

242 | ShowLibs

240 | ShowLibdir

243 | ShowLibdir

@@ -248,8 +251,8 @@ data Opt = Filename String

248 | DefaultTotal

251 | DefaultTotal

249 | DefaultPartial

252 | DefaultPartial

250 | WarnPartial

253 | WarnPartial

251− | NoCoverage

254+ | NoCoverage

252− | ErrContext

255+ | ErrContext

253 | ShowImpl

256 | ShowImpl

254 | Verbose

257 | Verbose

255 | IBCSubDir String

258 | IBCSubDir String

src/Idris/REPL.hs+28−10

@@ -304,8 +304,9 @@ process fn (Eval t)

304 logLvl 3 $ "Raw: " ++ show (tm', ty')

305 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

306 imp <- impShow

307+ c <- colourise

307− iResult (showImp (Just ist) imp True (delab ist tm') ++ " : " ++

308+ iResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

308− showImp (Just ist) imp True (delab ist ty'))

309+ showImp (Just ist) imp c (delab ist ty'))

309process fn (ExecVal t)

310process fn (ExecVal t)

310 = do ctxt <- getContext

311 = do ctxt <- getContext

311 ist <- getIState

312 ist <- getIState

@@ -314,15 +315,17 @@ process fn (ExecVal t)

314 let ty' = normaliseAll ctxt [] ty

315 let ty' = normaliseAll ctxt [] ty

315 res <- execute tm

316 res <- execute tm

316 imp <- impShow

317 imp <- impShow

318+ c <- colourise

317− iResult (showImp (Just ist) imp True (delab ist res) ++ " : " ++

319+ iResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++

318− showImp (Just ist) imp True (delab ist ty'))

320+ showImp (Just ist) imp c (delab ist ty'))

319process fn (Check (PRef _ n))

321process fn (Check (PRef _ n))

320 = do ctxt <- getContext

322 = do ctxt <- getContext

321 ist <- getIState

323 ist <- getIState

322 imp <- impShow

324 imp <- impShow

325+ c <- colourise

323 case lookupNames n ctxt of

326 case lookupNames n ctxt of

324 ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++

327 ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++

325− showImp (Just ist) imp True (delabTy ist n)) ts

328+ showImp (Just ist) imp c (delabTy ist n)) ts

326 iResult ""

329 iResult ""

327 [] -> iFail $ "No such variable " ++ show n

330 [] -> iFail $ "No such variable " ++ show n

328process fn (Check t)

331process fn (Check t)

@@ -330,11 +333,12 @@ process fn (Check t)

330 ctxt <- getContext

333 ctxt <- getContext

331 ist <- getIState

334 ist <- getIState

332 imp <- impShow

335 imp <- impShow

336+ c <- colourise

333 let ty' = normaliseC ctxt [] ty

337 let ty' = normaliseC ctxt [] ty

334 case tm of

338 case tm of

335 TType _ -> iResult ("Type : Type 1")

339 TType _ -> iResult ("Type : Type 1")

336− _ -> iResult (showImp (Just ist) imp True (delab ist tm) ++ " : " ++

340+ _ -> iResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

337− showImp (Just ist) imp True (delab ist ty))

341+ showImp (Just ist) imp c (delab ist ty))

338

342

339process fn (DocStr n) = do i <- getIState

343process fn (DocStr n) = do i <- getIState

340 case lookupCtxtName n (idris_docstrings i) of

344 case lookupCtxtName n (idris_docstrings i) of

@@ -364,8 +368,9 @@ process fn (Defn n) = do i <- getIState

364 [t] -> iputStrLn (showTotal t i)

368 [t] -> iputStrLn (showTotal t i)

365 _ -> return ()

369 _ -> return ()

366 where printCase i (_, lhs, rhs)

370 where printCase i (_, lhs, rhs)

371+ = do c <- colourise

367− = do iputStrLn (showImp (Just i) True False (delab i lhs) ++ " = " ++

372+ iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

368− showImp (Just i) True False (delab i rhs))

373+ showImp (Just i) True c (delab i rhs))

369process fn (TotCheck n) = do i <- getIState

374process fn (TotCheck n) = do i <- getIState

370 case lookupTotal n (tt_ctxt i) of

375 case lookupTotal n (tt_ctxt i) of

371 [t] -> iResult (showTotal t i)

376 [t] -> iResult (showTotal t i)

@@ -502,10 +507,11 @@ process fn (Pattelab t)

502

507

503process fn (Missing n)

508process fn (Missing n)

504 = do i <- getIState

509 = do i <- getIState

510+ c <- colourise

505 case lookupCtxt n (idris_patdefs i) of

511 case lookupCtxt n (idris_patdefs i) of

506 [] -> return ()

512 [] -> return ()

507 [(_, tms)] ->

513 [(_, tms)] ->

508− iResult (showSep "\n" (map (showImp (Just i) True False) tms))

514+ iResult (showSep "\n" (map (showImp (Just i) True c) tms))

509 _ -> iFail $ "Ambiguous name"

515 _ -> iFail $ "Ambiguous name"

510process fn (DynamicLink l) = do i <- getIState

516process fn (DynamicLink l) = do i <- getIState

511 let lib = trim l

517 let lib = trim l

@@ -627,6 +633,10 @@ parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

627parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

633parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

628parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

634parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

629parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

635parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

636+parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns

637+parseArgs ("--color":ns) = ColourREPL True : parseArgs ns

638+parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns

639+parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns

630parseArgs (n:ns) = Filename n : (parseArgs ns)

640parseArgs (n:ns) = Filename n : (parseArgs ns)

631

641

632helphead =

642helphead =

@@ -740,6 +750,10 @@ idrisMain opts =

740 [expr] -> return (Just expr)

750 [expr] -> return (Just expr)

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

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

742 putIState (i { default_total = True })

752 putIState (i { default_total = True })

753+ case opt getColour opts of

754+ [] -> return ()

755+ xs -> do i <- getIState

756+ putIState (i { idris_colourRepl = last xs })

743 mapM_ addLangExt (opt getLanguageExt opts)

757 mapM_ addLangExt (opt getLanguageExt opts)

744 setREPL runrepl

758 setREPL runrepl

745 setQuiet (quiet || isJust script)

759 setQuiet (quiet || isJust script)

@@ -876,6 +890,10 @@ getOptLevel :: Opt -> Maybe Int

876getOptLevel (OptLevel x) = Just x

890getOptLevel (OptLevel x) = Just x

877getOptLevel _ = Nothing

891getOptLevel _ = Nothing

878

892

893+getColour :: Opt -> Maybe Bool

894+getColour (ColourREPL b) = Just b

895+getColour _ = Nothing

896+

879opt :: (Opt -> Maybe a) -> [Opt] -> [a]

897opt :: (Opt -> Maybe a) -> [Opt] -> [a]

880opt = mapMaybe

898opt = mapMaybe

881

899

src/Main.hs+1

@@ -80,6 +80,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

80 "Usage: idris [input file] [options]\n" ++

81 "Options:\n" ++

82 "\t--quiet Quiet mode (for editors)\n" ++

83+ "\t--[no]colour Control REPL colour highlighting" ++

83 "\t--check Type check only\n" ++

84 "\t--check Type check only\n" ++

84 "\t-o [file] Specify output filename\n" ++

85 "\t-o [file] Specify output filename\n" ++

85 "\t-i [dir] Add directory to the list of import paths\n" ++

86 "\t-i [dir] Add directory to the list of import paths\n" ++