git.iko.soy/Idris-dev
on master help sign in
Support '!' at REPL
e4343cbEdwin Brady
src/Idris/AbsSyntaxTree.hs+4−4
compare with master
unifiedsplit
@@ -960,7 +960,7 @@ prettyImp impl = prettySe 10
960 prettySe p (PApp _ (PRef _ f) [])
960 prettySe p (PApp _ (PRef _ f) [])
961 | not impl = pretty f
961 | not impl = pretty f
962 prettySe p (PAppBind _ (PRef _ f) [])
962 prettySe p (PAppBind _ (PRef _ f) [])
963− | not impl = pretty f <+> text "!"
963+ | not impl = text "!" <+> pretty f
964 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
964 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
965 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
965 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
966 let [l, r] = getExps args in
966 let [l, r] = getExps args in
@@ -1147,7 +1147,7 @@ showImp ist impl colour tm = se 10 [] tm where
1147 se p bnd (PApp _ hd@(PRef _ f) [])
1147 se p bnd (PApp _ hd@(PRef _ f) [])
1148 | not impl = se p bnd hd
1148 | not impl = se p bnd hd
1149 se p bnd (PAppBind _ hd@(PRef _ f) [])
1149 se p bnd (PAppBind _ hd@(PRef _ f) [])
1150− | not impl = se p bnd hd ++ "!"
1150+ | not impl = "!" ++ se p bnd hd
1151 se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)
1151 se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)
1152 | length (getExps args) == 2 && not impl && not (isAlpha f)
1152 | length (getExps args) == 2 && not impl && not (isAlpha f)
1153 = let [l, r] = getExps args in
1153 = let [l, r] = getExps args in
@@ -1158,8 +1158,8 @@ showImp ist impl colour tm = se 10 [] tm where
1158 else concatMap (seArg bnd) args
1158 else concatMap (seArg bnd) args
1159 se p bnd (PAppBind _ f as)
1159 se p bnd (PAppBind _ f as)
1160 = let args = getExps as in
1160 = let args = getExps as in
1161− bracket p 1 $ se 1 bnd f ++ "!" ++ if impl then concatMap (sArg bnd) as
1161+ "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1162− else concatMap (seArg bnd) args
1162+ else concatMap (seArg bnd) args)
1163 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1163 se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1164 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1164 where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1165 se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1165 se p bnd (PHidden tm) = "." ++ se 0 bnd tm
src/Idris/ParseExpr.hs+1−1
@@ -48,7 +48,7 @@ fullExpr :: SyntaxInfo -> IdrisParser PTerm
48fullExpr syn = do x <- expr syn
48fullExpr syn = do x <- expr syn
49 eof
49 eof
50 i <- get
50 i <- get
51− return $ desugar syn i x
51+ return $ debindApp syn (desugar syn i x)
52
52
53
53
54{- |Parses an expression
54{- |Parses an expression