ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Minor change to display of metavariables

Browse Source 
Displaying things with machine generated names is really just noise, and
potentially confusing since they're inaccessible and typically an
artefact of the elaboration process, so hide them.

(If this turns out to be differently confusing, we'll have to consider
an option to display them. Maybe we should do that anyway.)
This commit is contained in:
Edwin Brady 2015-10-01 11:24:00 +01:00
parent b54006872f
commit 18e4b21071
2 changed files with 12 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Idris/Core/Elaborate.hs
View File

@ -711,8 +711,8 @@ checkPiGoal n
= do g <- goal = do g <- goal
case g of case g of
Bind _ (Pi _ _ _) _ -> return () Bind _ (Pi _ _ _) _ -> return ()
_ -> do a <- getNameFrom (sMN 0 "pargTy") _ -> do a <- getNameFrom (sMN 0 "__pargTy")
b <- getNameFrom (sMN 0 "pretTy") b <- getNameFrom (sMN 0 "__pretTy")
f <- getNameFrom (sMN 0 "pf") f <- getNameFrom (sMN 0 "pf")
claim a RType claim a RType
claim b RType claim b RType
@ -725,8 +725,8 @@ checkPiGoal n
simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
simple_app infer fun arg str = simple_app infer fun arg str =
do a <- getNameFrom (sMN 0 "argTy") do a <- getNameFrom (sMN 0 "__argTy")
b <- getNameFrom (sMN 0 "retTy") b <- getNameFrom (sMN 0 "__retTy")
f <- getNameFrom (sMN 0 "f") f <- getNameFrom (sMN 0 "f")
s <- getNameFrom (sMN 0 "s") s <- getNameFrom (sMN 0 "s")
claim a RType claim a RType

14
src/Idris/REPL.hs
View File

@ -942,12 +942,14 @@ process fn (Check (PRef _ _ n))
putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
putTy ppo ist i bnd (PPi _ n _ t sc) putTy ppo ist i bnd (PPi _ n _ t sc)
= let current = text " " <> = let current = case n of
(case n of MN _ _ -> text ""
MN _ _ -> text "_" UN nm | ('_':'_':_) <- str nm -> text ""
UN nm | ('_':'_':_) <- str nm -> text "_" _ -> text " " <>
_ -> bindingOf n False) <+> bindingOf n False
colon <+> align (tPretty bnd ist t) <> line <+> colon
<+> align (tPretty bnd ist t)
<> line
in in
current <> putTy ppo ist (i-1) ((n,False):bnd) sc current <> putTy ppo ist (i-1) ((n,False):bnd) sc
putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc