git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2430 from david-christiansen/parser-highlights
768437cDavid Christiansen
src/Idris/Elab/Term.hs+3−7
compare with master
unifiedsplit
@@ -409,7 +409,7 @@ elab ist info emode opts fn tm
409-- pexp l, pexp r]))
409-- pexp l, pexp r]))
410-- True
410-- True
411
411
412− elab' ina _ (PDPair fc p l@(PRef _ n) t r)
412+ elab' ina _ (PDPair fc p l@(PRef nfc n) t r)
413 = case t of
413 = case t of
414 Placeholder ->
414 Placeholder ->
415 do hnf_compute
415 do hnf_compute
@@ -418,13 +418,9 @@ elab ist info emode opts fn tm
418 TType _ -> asType
418 TType _ -> asType
419 _ -> asValue
419 _ -> asValue
420 _ -> asType
420 _ -> 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)
422 [pexp t,
422 [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)])
428 asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)
424 asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)
429 [pimp (sMN 0 "a") t False,
425 [pimp (sMN 0 "a") t False,
430 pimp (sMN 0 "P") Placeholder True,
426 pimp (sMN 0 "P") Placeholder True,
src/Idris/ParseExpr.hs+2−2
@@ -403,13 +403,13 @@ bracketed' open syn =
403 do (FC f start (l, c)) <- getFC
403 do (FC f start (l, c)) <- getFC
404 lchar ')'
404 lchar ')'
405 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
405 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 ':';
407 lty <- expr syn
407 lty <- expr syn
408 reservedOp "**"
408 reservedOp "**"
409 fc <- getFC
409 fc <- getFC
410 r <- expr syn
410 r <- expr syn
411 lchar ')'
411 lchar ')'
412− return (PDPair fc TypeOrTerm (PRef fc ln) lty r))
412+ return (PDPair fc TypeOrTerm (PRef lnfc ln) lty r))
413 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
413 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
414 -- No prefix operators! (bit of a hack here...)
414 -- No prefix operators! (bit of a hack here...)
415 if (o == "-" || o == "!")
415 if (o == "-" || o == "!")