git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2430 from david-christiansen/parser-highlights

Highlight name in dependent pair type as binder

commit768437c7c8c4ef239e810f26f1915b5065d3f8ee authorDavid Christiansen <david@davidchristiansen.dk> dateFri 10 Jul 2015, 20:14 (11 years ago) parentc2bf84ffb600d4
2 files changed+5−9
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+3−7 src/Idris/ParseExpr.hs+2−2
src/Idris/Elab/Term.hs+3−7
@@ -409,7 +409,7 @@ elab ist info emode opts fn tm
409409-- pexp l, pexp r]))
410410-- True
411411
412− elab' ina _ (PDPair fc p l@(PRef _ n) t r)
412+ elab' ina _ (PDPair fc p l@(PRef nfc n) t r)
413413 = case t of
414414 Placeholder ->
415415 do hnf_compute
@@ -418,13 +418,9 @@ elab ist info emode opts fn tm
418418 TType _ -> asType
419419 _ -> asValue
420420 _ -> asType
421− where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
421+ where asType = elab' ina (Just fc) (PApp fc (PRef NoFC sigmaTy)
422422 [pexp t,
423−
424− -- TODO: save the FC from the dependent pair
425− -- syntax and put it on this lambda for interactive
426− -- semantic highlighting support. NoFC for now.
427− pexp (PLam fc n NoFC Placeholder r)])
423+ pexp (PLam fc n nfc Placeholder r)])
428424 asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)
429425 [pimp (sMN 0 "a") t False,
430426 pimp (sMN 0 "P") Placeholder True,
src/Idris/ParseExpr.hs+2−2
@@ -403,13 +403,13 @@ bracketed' open syn =
403403 do (FC f start (l, c)) <- getFC
404404 lchar ')'
405405 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
406− <|> try (do ln <- fst <$> name; lchar ':';
406+ <|> try (do (ln, lnfc) <- name; lchar ':';
407407 lty <- expr syn
408408 reservedOp "**"
409409 fc <- getFC
410410 r <- expr syn
411411 lchar ')'
412− return (PDPair fc TypeOrTerm (PRef fc ln) lty r))
412+ return (PDPair fc TypeOrTerm (PRef lnfc ln) lty r))
413413 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
414414 -- No prefix operators! (bit of a hack here...)
415415 if (o == "-" || o == "!")