bbee4af · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #852 from david-christiansen/ideslave-really-no-curses

Don't use Curses to look for console width in IDESlave + properly serialize and deserialize the new with-expressions from IBCs

commitbbee4af9c73e9ae390b384ad4f7238eeade85aac authorEdwin Brady <edwin.brady@gmail.com> dateWed 5 Feb 2014, 10:59 (13 years ago) parentc15b21b 649b340

2 files changed+15−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−2 src/Idris/IBC.hs+8−1

src/Idris/AbsSyntax.hs+7−2

@@ -425,14 +425,19 @@ renderWidth = do iw <- getWidth

425425

426426iRender :: Doc a -> Idris (SimpleDoc a)

427427iRender d = do w <- getWidth

428+ ist <- getIState

429+ let ideSlave = case idris_outputmode ist of

430+ IdeSlave _ -> True

431+ _ -> False

428432 case w of

429433 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

430434 ColsWide n -> return $

431435 if n < 1

432436 then renderPretty 1.0 1000000000 d

433437 else renderPretty 0.8 n d

434− AutomaticWidth -> do width <- runIO getScreenWidth

435− return $ renderPretty 0.8 width d

438+ AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

439+ | otherwise -> do width <- runIO getScreenWidth

440+ return $ renderPretty 0.8 width d

436441

437442ihPrintResult :: Handle -> String -> Idris ()

438443ihPrintResult h s = do i <- getIState

src/Idris/IBC.hs+8−1

@@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 58

29+ibcVersion = 59

3030

3131

3232data IBCFile = IBCFile { ver :: Word8,

@@ -1650,6 +1650,10 @@ instance Binary PTerm where

16501650 put x1

16511651 PNoImplicits x1 -> do putWord8 36

16521652 put x1

1653+ PDisamb x1 x2 -> do putWord8 37

1654+ put x1

1655+ put x2

1656+

16531657 get

16541658 = do i <- getWord8

16551659 case i of

@@ -1759,6 +1763,9 @@ instance Binary PTerm where

17591763 return (PUnifyLog x1)

17601764 36 -> do x1 <- get

17611765 return (PNoImplicits x1)

1766+ 37 -> do x1 <- get

1767+ x2 <- get

1768+ return (PDisamb x1 x2)

17621769 _ -> error "Corrupted binary data for PTerm"

17631770

17641771instance (Binary t) => Binary (PTactic' t) where