misc fixes and refactorings

src/Core/FC.idr

@@ -11,10 +11,11 @@ public export
 FileName : Type
 FileName = String
 
+||| A file context is a filename together with starting and ending positions
 public export
 data FC = MkFC FileName FilePos FilePos
         | EmptyFC
-        
+
 export
 file : FC -> FileName
 file (MkFC fn _ _) = fn
@@ -38,7 +39,7 @@ within (x, y) (MkFC _ start end)
    = (x, y) >= start && (x, y) <= end
 within _ _ = False
 
--- Return whether a given line is on the same line as the file context (assuming 
+-- Return whether a given line is on the same line as the file context (assuming
 -- we're in the right file)
 export
 onLine : Int -> FC -> Bool
@@ -58,8 +59,8 @@ toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
 
 export
 Show FC where
-  show loc = file loc ++ ":" ++ 
-             showPos (startPos loc) ++ "--" ++ 
+  show loc = file loc ++ ":" ++
+             showPos (startPos loc) ++ "--" ++
              showPos (endPos loc)
 
 

src/Idris/CommandLine.idr

@@ -101,7 +101,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Run the REPL with machine-readable syntax"),
 
            MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"]
-              (Just "Run the ide socket mode on default host and port (localhost:38398"),
+              (Just "Run the ide socket mode on default host and port (localhost:38398)"),
 
            MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
               (Just "Run the ide socket mode on given host and port"),

src/Idris/IDEMode/REPL.idr

@@ -31,6 +31,8 @@ import TTImp.Elab
 import TTImp.TTImp
 import TTImp.ProcessDecls
 
+import Utils.Hex
+
 import Control.Catchable
 import System
 import Idris.Socket
@@ -99,38 +101,12 @@ getNChars i (S k)
          xs <- getNChars i k
          pure (x :: xs)
 
-hex : Char -> Maybe Int
-hex '0' = Just 0
-hex '1' = Just 1
-hex '2' = Just 2
-hex '3' = Just 3
-hex '4' = Just 4
-hex '5' = Just 5
-hex '6' = Just 6
-hex '7' = Just 7
-hex '8' = Just 8
-hex '9' = Just 9
-hex 'a' = Just 10
-hex 'b' = Just 11
-hex 'c' = Just 12
-hex 'd' = Just 13
-hex 'e' = Just 14
-hex 'f' = Just 15
-hex _ = Nothing
-
-export
-toHex : Int -> List Char -> Maybe Int
-toHex _ [] = Just 0
-toHex m (d :: ds)
-    = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
-
-
 -- Read 6 characters. If they're a hex number, read that many characters.
 -- Otherwise, just read to newline
 getInput : File -> IO String
 getInput f
     = do x <- getNChars f 6
-         case toHex 1 (reverse x) of
+         case fromHexChars (reverse x) of
               Nothing =>
                 do rest <- getFLine f
                    pure (pack x ++ rest)

src/Idris/Package.idr

@@ -67,6 +67,7 @@ Show PkgDesc where
              maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
              maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
              maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
+             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
              maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
              maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
              maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg)

src/Utils/Hex.idr

@@ -31,3 +31,34 @@ asHex n = pack $ asHex' n []
     asHex' n hex with (n `divides` 16)
       asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex)
 
+export
+fromHexDigit : Char -> Maybe Int
+fromHexDigit '0' = Just 0
+fromHexDigit '1' = Just 1
+fromHexDigit '2' = Just 2
+fromHexDigit '3' = Just 3
+fromHexDigit '4' = Just 4
+fromHexDigit '5' = Just 5
+fromHexDigit '6' = Just 6
+fromHexDigit '7' = Just 7
+fromHexDigit '8' = Just 8
+fromHexDigit '9' = Just 9
+fromHexDigit 'a' = Just 10
+fromHexDigit 'b' = Just 11
+fromHexDigit 'c' = Just 12
+fromHexDigit 'd' = Just 13
+fromHexDigit 'e' = Just 14
+fromHexDigit 'f' = Just 15
+fromHexDigit _ = Nothing
+
+export
+fromHexChars : List Char -> Maybe Int
+fromHexChars = fromHexChars' 1
+  where
+    fromHexChars' : Int -> List Char -> Maybe Int
+    fromHexChars' _ [] = Just 0
+    fromHexChars' m (d :: ds) = pure $ !(fromHexDigit (toLower d)) * m + !(fromHexChars' (m*16) ds)
+
+export
+fromHex : String -> Maybe Int
+fromHex = fromHexChars . unpack