@@ -66,27 +66,27 @@ toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not impleme
6666eInfoNames :: ElabInfo -> [Name]
6767eInfoNames info = map fst (params info) ++ M.keys (inblock info)
6868
69−data IOption = IOption { opt_logLevel :: Int,
70− opt_typecase :: Bool,
71− opt_typeintype :: Bool,
72− opt_coverage :: Bool,
73− opt_showimp :: Bool, -- ^^ show implicits
74− opt_errContext :: Bool,
75− opt_repl :: Bool,
76− opt_verbose :: Bool,
77− opt_nobanner :: Bool,
78− opt_quiet :: Bool,
79− opt_codegen :: Codegen,
80− opt_outputTy :: OutputType,
81− opt_ibcsubdir :: FilePath,
82− opt_importdirs :: [FilePath],
83− opt_triple :: String,
84− opt_cpu :: String,
85− opt_cmdline :: [Opt], -- remember whole command line
86− opt_origerr :: Bool,
87− opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
88− opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
89− opt_optimise :: [Optimisation]
69+data IOption = IOption { opt_logLevel :: Int,
70+ opt_typecase :: Bool,
71+ opt_typeintype :: Bool,
72+ opt_coverage :: Bool,
73+ opt_showimp :: Bool, -- ^^ show implicits
74+ opt_errContext :: Bool,
75+ opt_repl :: Bool,
76+ opt_verbose :: Bool,
77+ opt_nobanner :: Bool,
78+ opt_quiet :: Bool,
79+ opt_codegen :: Codegen,
80+ opt_outputTy :: OutputType,
81+ opt_ibcsubdir :: FilePath,
82+ opt_importdirs :: [FilePath],
83+ opt_triple :: String,
84+ opt_cpu :: String,
85+ opt_cmdline :: [Opt], -- remember whole command line
86+ opt_origerr :: Bool,
87+ opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
88+ opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
89+ opt_optimise :: [Optimisation]
9090 }
9191 deriving (Show, Eq)
9292
@@ -151,6 +151,8 @@ data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
151151data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
152152 | ColsWide Int -- ^ Manually specified - must be positive
153153 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
154+ deriving (Show, Eq)
155+
154156
155157-- | The global state used in the Idris monad
156158data IState = IState {
@@ -463,6 +465,7 @@ data Opt = Filename String
463465 | ShowOrigErr
464466 | AutoWidth -- ^ Automatically adjust terminal width
465467 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
468+ | UseConsoleWidth ConsoleWidth
466469 deriving (Show, Eq)
467470
468471-- Parsed declarations