Automatically detect console width

This can now be overridden with the :consolewidth command at the REPL or
in an init script.

CHANGELOG

@@ -24,6 +24,8 @@ New in 0.9.11:
   structurally smaller than "(x :: xs)"
 * assert_total internal function, which marks a subexpression as assumed to
   be total, e.g "assert_total (tail (x :: xs))".
+* Terminal width is automatically detected if Idris is compiled with curses
+  support. If curses is not available, automatic mode assumes 80 columns.
 
 Internal changes
 

custom.mk-alldeps

@@ -1,2 +1,2 @@
-CABALFLAGS += -f LLVM -f FFI
+CABALFLAGS += -f LLVM -f FFI -f curses
 

idris.cabal

@@ -370,6 +370,11 @@ Flag GMP
   Default:      False
   manual:       True
 
+Flag curses
+  Description:  Use Curses to get the screen width
+  Default:      False
+  manual:       True
+
 -- This flag determines whether to show Git hashes in version strings
 -- Defaults to True because Hackage is a source release
 Flag release
@@ -449,6 +454,7 @@ Library
 
                 , Pkg.Package
                 , Util.DynamicLinker
+                , Util.ScreenSize
 
   Other-modules:
                   Util.Pretty
@@ -529,6 +535,9 @@ Library
   if flag(GMP)
      build-depends: libffi
      cpp-options:   -DIDRIS_GMP
+  if flag(curses)
+     build-depends: hscurses
+     cpp-options:   -DCURSES
 
 Executable idris
   Main-is:        Main.hs

src/Idris/AbsSyntax.hs

@@ -36,6 +36,7 @@ import Control.Monad.Error (throwError, catchError)
 import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
 
 import Util.Pretty
+import Util.ScreenSize
 import Util.System
 
 getContext :: Idris Context
@@ -414,13 +415,24 @@ setWidth :: ConsoleWidth -> Idris ()
 setWidth w = do ist <- getIState
                 put ist { idris_consolewidth = w }
 
+renderWidth :: Idris Int
+renderWidth = do iw <- getWidth
+                 case iw of
+                   InfinitelyWide -> return 100000000
+                   ColsWide n -> return (max n 1)
+                   AutomaticWidth -> runIO getScreenWidth
+
+
 iRender :: Doc a -> Idris (SimpleDoc a)
 iRender d = do w <- getWidth
-               return $ case w of
-                          InfinitelyWide -> renderPretty 1.0 1000000000 d
-                          ColsWide n -> if n < 1
-                                          then renderPretty 1.0 1000000000 d
-                                          else renderPretty 0.5 n d
+               case w of
+                 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
+                 ColsWide n -> return $
+                               if n < 1
+                                 then renderPretty 1.0 1000000000 d
+                                 else renderPretty 0.8 n d
+                 AutomaticWidth -> do width <- runIO getScreenWidth
+                                      return $ renderPretty 0.8 width d
 
 ihPrintResult :: Handle -> String -> Idris ()
 ihPrintResult h s = do i <- getIState

src/Idris/AbsSyntaxTree.hs

@@ -85,7 +85,8 @@ data OutputMode = RawOutput | IdeSlave Integer deriving Show
 
 -- | How wide is the console?
 data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
-                  | ColsWide Int -- ^ Must be positive
+                  | ColsWide Int -- ^ Manually specified - must be positive
+                  | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
 
 -- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
 -- without typechecking).
@@ -219,7 +220,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
                    [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
                    [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
                    True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
-                   (ColsWide 80)
+                   AutomaticWidth
 
 -- | The monad for the main REPL - reading and processing files and updating
 -- global state (hence the IO inner monad).
@@ -283,6 +284,7 @@ data Command = Quit
              | ColourOn
              | ColourOff
              | ListErrorHandlers
+             | SetConsoleWidth ConsoleWidth
 
 data Opt = Filename String
          | Ver
@@ -329,6 +331,7 @@ data Opt = Filename String
          | OptLevel Word
          | Client String
          | ShowOrigErr
+         | AutoWidth -- ^ Automatically adjust terminal width
     deriving (Show, Eq)
 
 -- Parsed declarations

src/Idris/Completion.hs

@@ -54,7 +54,7 @@ tactics = map fst tacticArgs
 -- | Convert a name into a string usable for completion. Filters out names
 -- that users probably don't want to see.
 nameString :: Name -> Maybe String
-nameString (UN nm) 
+nameString (UN nm)
    | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing
 nameString (UN n)       = Just (str n)
 nameString (NS n _)     = nameString n
@@ -106,6 +106,10 @@ completeOption :: CompletionFunc Idris
 completeOption = completeWord Nothing " \t" completeOpt
     where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]
 
+completeConsoleWidth :: CompletionFunc Idris
+completeConsoleWidth = completeWord Nothing " \t" completeW
+    where completeW = return . completeWith ["auto", "infinite", "80", "120"]
+
 isWhitespace :: Char -> Bool
 isWhitespace = (flip elem) " \t\n"
 
@@ -152,6 +156,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
           completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
           completeArg ColourArg = completeColour (prev, next)
           completeArg NoArg = noCompletion (prev, next)
+          completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
           completeCmdName = return $ ("", completeWith commands cmd)
 
 -- | Complete REPL commands and defined identifiers

src/Idris/Help.hs

@@ -9,6 +9,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
             | ColourArg  -- ^ The command is the colour-setting command
             | NoArg -- ^ No completion (yet!?)
             | SpecialHeaderArg -- ^ do not use
+            | ConsoleWidthArg -- ^ The width of the console
 
 instance Show CmdArg where
     show ExprArg          = "<expr>"
@@ -20,6 +21,7 @@ instance Show CmdArg where
     show ColourArg        = "<option>"
     show NoArg            = ""
     show SpecialHeaderArg = "Arguments"
+    show ConsoleWidthArg  = "auto|infinite|<number>"
 
 help :: [([String], CmdArg, String)]
 help =
@@ -50,6 +52,7 @@ help =
     ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),
     ([":unset"], OptionArg, "Unset an option"),
     ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),
+    ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),
     ([":q",":quit"], NoArg, "Exit the Idris system")
   ]
 

src/Idris/REPL.hs

@@ -935,6 +935,8 @@ process h fn ListErrorHandlers =
        [] -> iPrintResult "No registered error handlers"
        handlers ->
            iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers
+process h fn (SetConsoleWidth w) = setWidth w
+
 
 classInfo :: ClassInfo -> Idris ()
 classInfo ci = do iputStrLn "Methods:\n"

src/Idris/REPLParser.hs

@@ -97,6 +97,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)
               <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))
               <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))
               <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)
+              <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))
               <|> do P.whiteSpace; do eof; return NOP
                              <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
 
@@ -107,6 +108,11 @@ pOption = do discard (P.symbol "errorcontext"); return ErrContext
       <|> do discard (P.symbol "showimplicits"); return ShowImpl
       <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
 
+pConsoleWidth :: P.IdrisParser ConsoleWidth
+pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
+            <|> do discard (P.symbol "infinite"); return InfinitelyWide
+            <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
+
 colours :: [(String, Maybe Color)]
 colours = [ ("black", Just Black)
           , ("red", Just Red)

src/Util/ScreenSize.hs

@@ -0,0 +1,21 @@
+{-# LANGUAGE CPP #-}
+module Util.ScreenSize where
+
+import Debug.Trace
+
+#ifndef CURSES
+
+getScreenWidth :: IO Int
+getScreenWidth = return 80
+
+#else
+
+import UI.HSCurses.Curses
+
+getScreenWidth :: IO Int
+getScreenWidth = do initScr
+                    refresh
+                    size <- scrSize
+                    endWin
+                    return (snd size)
+#endif