c5de844 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Catch some lingering renames that I missed

There were some instances of ideslave left. Now fixed.

commitc5de844a310d596376f21946c0f8806a766604f9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 15 Feb 2015, 17:27 (12 years ago) parent40d094d

3 files changed+91−89

compare with master

unifiedsplit

src/Idris/Output.hs+7−5 src/Idris/Prover.hs+4−4 src/Idris/REPL.hs+80−80

src/Idris/Output.hs+7−5

@@ -152,11 +152,13 @@ iputStrLn s = do i <- getIState

152152 IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

153153

154154

155−ideslavePutSExp :: SExpable a => String -> a -> Idris ()

156−ideslavePutSExp cmd info = do i <- getIState

157− case idris_outputmode i of

158− IdeMode n h -> runIO . hPutStrLn h $ convSExp cmd info n

159− _ -> return ()

155+idemodePutSExp :: SExpable a => String -> a -> Idris ()

156+idemodePutSExp cmd info = do i <- getIState

157+ case idris_outputmode i of

158+ IdeMode n h ->

159+ runIO . hPutStrLn h $

160+ convSExp cmd info n

161+ _ -> return ()

160162

161163-- TODO: send structured output similar to the metavariable list

162164iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

src/Idris/Prover.hs+4−4

@@ -67,12 +67,12 @@ assumptionNames e

6767prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

6868prove opt ctxt lit n ty

6969 = do let ps = initElaborator n ctxt ty

70− ideslavePutSExp "start-proof-mode" n

70+ idemodePutSExp "start-proof-mode" n

7171 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

7272 iLOG $ "Adding " ++ show tm

7373 i <- getIState

7474 case idris_outputmode i of

75− IdeMode _ _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

75+ IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, showProof lit n prf)

7676 _ -> iputStrLn $ showProof lit n prf

7777 let proofs = proof_list i

7878 putIState (i { proof_list = (n, prf) : proofs })

@@ -198,7 +198,7 @@ receiveInput h e =

198198 Just (IdeMode.REPLCompletions prefix) ->

199199 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

200200 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]

201− ideslavePutSExp "return" good

201+ idemodePutSExp "return" good

202202 receiveInput h e

203203 Just (IdeMode.Interpret cmd) -> return (Just cmd)

204204 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))

@@ -254,7 +254,7 @@ ploop fn d prompt prf e h

254254 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

255255 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

256256 (\err -> return (False, e, False, prf, Left err))

257− ideslavePutSExp "write-proof-state" (prf', length prf')

257+ idemodePutSExp "write-proof-state" (prf', length prf')

258258 case res of

259259 Left err -> do ist <- getIState

260260 iRenderError $ pprintErr ist err

src/Idris/REPL.hs+80−80

@@ -241,8 +241,8 @@ initIdemodeSocket = do

241241 return h

242242

243243-- | Run the IdeMode

244−ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()

245−ideslaveStart s orig mods

244+idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()

245+idemodeStart s orig mods

246246 = do h <- runIO $ if s then initIdemodeSocket else return stdout

247247 setIdeMode True h

248248 i <- getIState

@@ -252,10 +252,10 @@ ideslaveStart s orig mods

252252 case mods of

253253 a:_ -> runIdeModeCommand h n i "" [] (IdeMode.LoadFile a Nothing)

254254 _ -> return ()

255− ideslave h orig mods

255+ idemode h orig mods

256256

257−ideslave :: Handle -> IState -> [FilePath] -> Idris ()

258−ideslave h orig mods

257+idemode :: Handle -> IState -> [FilePath] -> Idris ()

258+idemode h orig mods

259259 = do idrisCatch

260260 (do let inh = if h == stdout then stdin else h

261261 len' <- runIO $ IdeMode.getLen inh

@@ -277,7 +277,7 @@ ideslave h orig mods

277277 Nothing -> iPrintError "did not understand" )

278278 (\e -> do iPrintError $ show e))

279279 (\e -> do iPrintError $ show e)

280− ideslave h orig mods

280+ idemode h orig mods

281281

282282-- | Run IDEMode commands

283283runIdeModeCommand :: Handle -- ^^ The handle for communication

@@ -312,7 +312,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

312312 _ -> return ()

313313 iRenderError $ pprintErr ist e)

314314 Success (Right cmd) -> idrisCatch

315− (ideslaveProcess fn cmd)

315+ (idemodeProcess fn cmd)

316316 (\e -> getIState >>= iRenderError . flip pprintErr e)

317317 Success (Left err) -> iPrintError err

318318runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

@@ -338,19 +338,19 @@ runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename toline) =

338338 (idris_parsedSpan i)

339339 in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

340340 Just x -> iPrintError $ "didn't load " ++ filename

341− ideslave h orig mods

341+ idemode h orig mods

342342runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

343343 case splitName name of

344344 Left err -> iPrintError err

345− Right n -> process "(ideslave)"

346− (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

345+ Right n -> process "(idemode)"

346+ (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

347347runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =

348348 case parseConst orig name of

349− Success c -> process "(ideslave)" (DocStr (Right c))

349+ Success c -> process "(idemode)" (DocStr (Right c))

350350 Failure _ ->

351351 case splitName name of

352352 Left err -> iPrintError err

353− Right n -> process "(ideslave)" (DocStr (Left n))

353+ Right n -> process "(idemode)" (DocStr (Left n))

354354runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355355 process fn (CaseSplitAt False line (sUN name))

356356runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

@@ -494,7 +494,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =

494494runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

495495 case splitName name of

496496 Left err -> iPrintError err

497− Right n -> process "(ideslave)" (PrintDef n)

497+ Right n -> process "(idemode)" (PrintDef n)

498498runIdeModeCommand h id orig fn modes (IdeMode.ErrString e) =

499499 do ist <- getIState

500500 let out = displayS . renderPretty 1.0 60 $ pprintErr ist e

@@ -532,76 +532,76 @@ splitName s = case reverse $ splitOn "." s of

532532 unparen ('(':x:xs) | last xs == ')' = init (x:xs)

533533 unparen str = str

534534

535−ideslaveProcess :: FilePath -> Command -> Idris ()

536−ideslaveProcess fn Warranty = process fn Warranty

537−ideslaveProcess fn Help = process fn Help

538−ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

539− iPrintResult "changed directory to"

540−ideslaveProcess fn (ModImport f) = process fn (ModImport f)

541−ideslaveProcess fn (Eval t) = process fn (Eval t)

542−ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)

543− iPrintResult "defined"

544−ideslaveProcess fn (Undefine n) = process fn (Undefine n)

545−ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

546−ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

547−ideslaveProcess fn (Check t) = process fn (Check t)

548−ideslaveProcess fn (DocStr n) = process fn (DocStr n)

549−ideslaveProcess fn Universes = process fn Universes

550−ideslaveProcess fn (Defn n) = do process fn (Defn n)

551− iPrintResult ""

552−ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

553−ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

554− iPrintResult ""

555−ideslaveProcess fn (Search ps t) = process fn (Search ps t)

556−ideslaveProcess fn (Spec t) = process fn (Spec t)

557−-- RmProof and AddProof not supported!

558−ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

559−ideslaveProcess fn (HNF t) = process fn (HNF t)

560−--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

561−ideslaveProcess fn (TestInline t) = process fn (TestInline t)

562−

563−ideslaveProcess fn Execute = do process fn Execute

535+idemodeProcess :: FilePath -> Command -> Idris ()

536+idemodeProcess fn Warranty = process fn Warranty

537+idemodeProcess fn Help = process fn Help

538+idemodeProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

539+ iPrintResult "changed directory to"

540+idemodeProcess fn (ModImport f) = process fn (ModImport f)

541+idemodeProcess fn (Eval t) = process fn (Eval t)

542+idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)

543+ iPrintResult "defined"

544+idemodeProcess fn (Undefine n) = process fn (Undefine n)

545+idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

546+idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

547+idemodeProcess fn (Check t) = process fn (Check t)

548+idemodeProcess fn (DocStr n) = process fn (DocStr n)

549+idemodeProcess fn Universes = process fn Universes

550+idemodeProcess fn (Defn n) = do process fn (Defn n)

564551 iPrintResult ""

565−ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

566− iPrintResult ""

567−ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

552+idemodeProcess fn (TotCheck n) = process fn (TotCheck n)

553+idemodeProcess fn (DebugInfo n) = do process fn (DebugInfo n)

554+ iPrintResult ""

555+idemodeProcess fn (Search ps t) = process fn (Search ps t)

556+idemodeProcess fn (Spec t) = process fn (Spec t)

557+-- RmProof and AddProof not supported!

558+idemodeProcess fn (ShowProof n') = process fn (ShowProof n')

559+idemodeProcess fn (HNF t) = process fn (HNF t)

560+--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!

561+idemodeProcess fn (TestInline t) = process fn (TestInline t)

562+

563+idemodeProcess fn Execute = do process fn Execute

564+ iPrintResult ""

565+idemodeProcess fn (Compile codegen f) = do process fn (Compile codegen f)

566+ iPrintResult ""

567+idemodeProcess fn (LogLvl i) = do process fn (LogLvl i)

568+ iPrintResult ""

569+idemodeProcess fn (Pattelab t) = process fn (Pattelab t)

570+idemodeProcess fn (Missing n) = process fn (Missing n)

571+idemodeProcess fn (DynamicLink l) = do process fn (DynamicLink l)

572+ iPrintResult ""

573+idemodeProcess fn ListDynamic = do process fn ListDynamic

568574 iPrintResult ""

569−ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

570−ideslaveProcess fn (Missing n) = process fn (Missing n)

571−ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

572− iPrintResult ""

573−ideslaveProcess fn ListDynamic = do process fn ListDynamic

574− iPrintResult ""

575−ideslaveProcess fn Metavars = process fn Metavars

576−ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

577− iPrintResult ""

578−ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

579− iPrintResult ""

580−ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

581− iPrintResult ""

582−ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

583− iPrintResult ""

584−ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)

575+idemodeProcess fn Metavars = process fn Metavars

576+idemodeProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

577+ iPrintResult ""

578+idemodeProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

585579 iPrintResult ""

586−ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)

587− iPrintResult ""

588−ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

589−ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

590−ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)

591−ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)

592−ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

593−ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

594−ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

595−ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

596−ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

580+idemodeProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

581+ iPrintResult ""

582+idemodeProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

583+ iPrintResult ""

584+idemodeProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)

597585 iPrintResult ""

598−ideslaveProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)

599− iPrintResult ""

600−ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

601−ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

602−ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)

603−ideslaveProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm)

604−ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

586+idemodeProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)

587+ iPrintResult ""

588+idemodeProcess fn (SetOpt x) = process fn (SetOpt x)

589+idemodeProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

590+idemodeProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)

591+idemodeProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)

592+idemodeProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

593+idemodeProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

594+idemodeProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

595+idemodeProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

596+idemodeProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

597+ iPrintResult ""

598+idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)

599+ iPrintResult ""

600+idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n)

601+idemodeProcess fn (CallsWho n) = process fn (CallsWho n)

602+idemodeProcess fn (PrintDef n) = process fn (PrintDef n)

603+idemodeProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm)

604+idemodeProcess fn _ = iPrintError "command not recognized or not supported"

605605

606606

607607-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

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

16131613 startServer port orig mods

16141614 runInputT (replSettings (Just historyFile)) $ repl orig mods efile

16151615 let idesock = IdemodeSocket `elem` opts

1616− when (idesl) $ ideslaveStart idesock orig inputs

1616+ when (idesl) $ idemodeStart idesock orig inputs

16171617 ok <- noErrors

16181618 when (not ok) $ runIO (exitWith (ExitFailure 1))

16191619 where