@@ -124,7 +124,7 @@ data IState = IState {
124 idris_calledgraph :: Ctxt [Name],
124 idris_calledgraph :: Ctxt [Name],
125 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
125 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
126 idris_tyinfodata :: Ctxt TIData,
126 idris_tyinfodata :: Ctxt TIData,
127− idris_totcheck :: [(FC, Name)], -- names to check totality on
127+ idris_totcheck :: [(FC, Name)], -- names to check totality on
128 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
128 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
129 idris_options :: IOption,
129 idris_options :: IOption,
130 idris_name :: Int,
130 idris_name :: Int,
@@ -298,7 +298,7 @@ data Command = Quit
298 | AddMissing Bool Int Name
298 | AddMissing Bool Int Name
299 | MakeWith Bool Int Name
299 | MakeWith Bool Int Name
300 | DoProofSearch Bool -- ^ update
300 | DoProofSearch Bool -- ^ update
301− Bool -- ^ recursive (i.e. do arguments too)
301+ Bool -- ^ recursive (i.e. do arguments too)
302 Int Name [Name]
302 Int Name [Name]
303 | SetOpt Opt
303 | SetOpt Opt
304 | UnsetOpt Opt
304 | UnsetOpt Opt
@@ -440,7 +440,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying
440 | Implicit -- implicit coercion
440 | Implicit -- implicit coercion
441 | CExport String -- export, with a C name
441 | CExport String -- export, with a C name
442 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
442 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
443− | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
443+ | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
444 | Reflection -- a reflecting function, compile-time only
444 | Reflection -- a reflecting function, compile-time only
445 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
445 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
446 deriving (Show, Eq)
446 deriving (Show, Eq)
@@ -843,10 +843,10 @@ deriving instance NFData ClassInfo
843-- Type inference data
843-- Type inference data
845data TIData = TIPartial -- ^ a function with a partially defined type
845data TIData = TIPartial -- ^ a function with a partially defined type
846− | TISolution [Term] -- ^ possible solutions to a metavariable in a type
846+ | TISolution [Term] -- ^ possible solutions to a metavariable in a type
847 deriving Show
847 deriving Show
849−data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
849+data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
850 detaggable :: Bool }
850 detaggable :: Bool }
851 deriving Show
851 deriving Show
@@ -1384,7 +1384,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im
1384 where strName (UN n) = T.unpack n
1384 where strName (UN n) = T.unpack n
1385 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1385 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1386 | otherwise = strName n
1386 | otherwise = strName n
1387− strName (MN i s) = T.unpack s
1387+ strName (MN i s) = T.unpack s
1388 strName other = show other
1388 strName other = show other