0fdbc0b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1921 from david-christiansen/idemode

0fdbc0bDavid Christiansen12 years ago

src/Idris/Output.hs+7−5

compare with master

unifiedsplit

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

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

153

154

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

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

156−ideslavePutSExp cmd info = do i <- getIState

156+idemodePutSExp cmd info = do i <- getIState

157− case idris_outputmode i of

157+ case idris_outputmode i of

158+ IdeMode n h ->

159+ runIO . hPutStrLn h $

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

160+ convSExp cmd info n

159− _ -> return ()

161+ _ -> return ()

160

162

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

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

162iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

164iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

src/Idris/Prover.hs+4−4

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

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

68prove opt ctxt lit n ty

69 = do let ps = initElaborator n ctxt ty

70− ideslavePutSExp "start-proof-mode" n

70+ idemodePutSExp "start-proof-mode" n

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

72 iLOG $ "Adding " ++ show tm

73 i <- getIState

74 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)

76 _ -> iputStrLn $ showProof lit n prf

77 let proofs = proof_list i

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

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

198 Just (IdeMode.REPLCompletions prefix) ->

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

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

201− ideslavePutSExp "return" good

201+ idemodePutSExp "return" good

202 receiveInput h e

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

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

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

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

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

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

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

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

258 case res of

259 Left err -> do ist <- getIState

260 iRenderError $ pprintErr ist err

src/Idris/REPL.hs+80−80

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

241 return h

242

243-- | Run the IdeMode

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

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

245−ideslaveStart s orig mods

245+idemodeStart s orig mods

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

247 setIdeMode True h

248 i <- getIState

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

252 case mods of

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

254 _ -> return ()

255− ideslave h orig mods

255+ idemode h orig mods

256

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

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

258−ideslave h orig mods

258+idemode h orig mods

259 = do idrisCatch

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

261 len' <- runIO $ IdeMode.getLen inh

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

277 Nothing -> iPrintError "did not understand" )

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

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

280− ideslave h orig mods

280+ idemode h orig mods

281

282-- | Run IDEMode commands

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

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

312 _ -> return ()

313 iRenderError $ pprintErr ist e)

314 Success (Right cmd) -> idrisCatch

315− (ideslaveProcess fn cmd)

315+ (idemodeProcess fn cmd)

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

317 Success (Left err) -> iPrintError err

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

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

338 (idris_parsedSpan i)

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

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

341− ideslave h orig mods

341+ idemode h orig mods

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

343 case splitName name of

344 Left err -> iPrintError err

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

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

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

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

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

348 case parseConst orig name of

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

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

350 Failure _ ->

351 case splitName name of

352 Left err -> iPrintError err

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

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

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

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

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

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

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

495 case splitName name of

496 Left err -> iPrintError err

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

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

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

499 do ist <- getIState

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

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

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

533 unparen str = str

534

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

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

536−ideslaveProcess fn Warranty = process fn Warranty

536+idemodeProcess fn Warranty = process fn Warranty

537−ideslaveProcess fn Help = process fn Help

537+idemodeProcess fn Help = process fn Help

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

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

539− iPrintResult "changed directory to"

539+ iPrintResult "changed directory to"

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

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

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

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

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

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

543− iPrintResult "defined"

543+ iPrintResult "defined"

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

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

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

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

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

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

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

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

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

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

549−ideslaveProcess fn Universes = process fn Universes

549+idemodeProcess fn Universes = process fn Universes

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

550+idemodeProcess 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

564 iPrintResult ""

551 iPrintResult ""

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−ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

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

566− iPrintResult ""

566+ iPrintResult ""

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

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

568 iPrintResult ""

574 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

575+idemodeProcess fn Metavars = process fn Metavars

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

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

577− iPrintResult ""

577+ iPrintResult ""

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

578+idemodeProcess 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)

585 iPrintResult ""

579 iPrintResult ""

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

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

587− iPrintResult ""

581+ iPrintResult ""

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

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

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

583+ iPrintResult ""

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

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

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)

597 iPrintResult ""

585 iPrintResult ""

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−ideslaveProcess fn (Apropos pkg a) = do process fn (Apropos pkg a)

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

599− iPrintResult ""

599+ iPrintResult ""

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

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

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

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

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

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

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

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

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

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

605

606

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

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

1613 startServer port orig mods

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

1615 let idesock = IdemodeSocket `elem` opts

1616− when (idesl) $ ideslaveStart idesock orig inputs

1616+ when (idesl) $ idemodeStart idesock orig inputs

1617 ok <- noErrors

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

1619 where