18e4b21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor change to display of metavariables

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.)

commit18e4b21071748a32d611adecfd751c8e6097ab3a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Oct 2015, 11:24 (11 years ago) parentb540068

2 files changed+12−10

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+4−4 src/Idris/REPL.hs+8−6

src/Idris/Core/Elaborate.hs+4−4

@@ -711,8 +711,8 @@ checkPiGoal n

711711 = do g <- goal

712712 case g of

713713 Bind _ (Pi _ _ _) _ -> return ()

714− _ -> do a <- getNameFrom (sMN 0 "pargTy")

715− b <- getNameFrom (sMN 0 "pretTy")

714+ _ -> do a <- getNameFrom (sMN 0 "__pargTy")

715+ b <- getNameFrom (sMN 0 "__pretTy")

716716 f <- getNameFrom (sMN 0 "pf")

717717 claim a RType

718718 claim b RType

@@ -725,8 +725,8 @@ checkPiGoal n

725725

726726simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

727727simple_app infer fun arg str =

728− do a <- getNameFrom (sMN 0 "argTy")

729− b <- getNameFrom (sMN 0 "retTy")

728+ do a <- getNameFrom (sMN 0 "__argTy")

729+ b <- getNameFrom (sMN 0 "__retTy")

730730 f <- getNameFrom (sMN 0 "f")

731731 s <- getNameFrom (sMN 0 "s")

732732 claim a RType

src/Idris/REPL.hs+8−6

@@ -942,12 +942,14 @@ process fn (Check (PRef _ _ n))

942942 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

943943 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

944944 putTy ppo ist i bnd (PPi _ n _ t sc)

945− = let current = text " " <>

946− (case n of

947− MN _ _ -> text "_"

948− UN nm | ('_':'_':_) <- str nm -> text "_"

949− _ -> bindingOf n False) <+>

950− colon <+> align (tPretty bnd ist t) <> line

945+ = let current = case n of

946+ MN _ _ -> text ""

947+ UN nm | ('_':'_':_) <- str nm -> text ""

948+ _ -> text " " <>

949+ bindingOf n False

950+ <+> colon

951+ <+> align (tPretty bnd ist t)

952+ <> line

951953 in

952954 current <> putTy ppo ist (i-1) ((n,False):bnd) sc

953955 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc