924f791 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Highlighting for infix operators

commit924f7913e18795b8e070ccbb634000ad88a991bc authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 10 May 2015, 20:06 (11 years ago) parentc8ae141

4 files changed+26−11

compare with master

unifiedsplit

src/Idris/Core/TT.hs+3−2 src/Idris/Elab/Term.hs+6−1 src/Idris/ParseHelpers.hs+10−2 src/Idris/ParseOps.hs+7−6

src/Idris/Core/TT.hs+3−2

@@ -123,10 +123,10 @@ instance Show FC where

123123 show (FileFC f) = f

124124

125125-- | Output annotation for pretty-printed name - decides colour

126−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput

126+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving Show

127127

128128-- | Text formatting output

129−data TextFormatting = BoldText | ItalicText | UnderlineText

129+data TextFormatting = BoldText | ItalicText | UnderlineText deriving Show

130130

131131-- | Output annotations for pretty-printing

132132data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -142,6 +142,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

142142 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term

143143 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific

144144 | AnnErr Err

145+ deriving Show

145146

146147-- | Used for error reflection

147148data ErrorReportPart = TextPart String

src/Idris/Elab/Term.hs+6−1

@@ -704,6 +704,11 @@ elab ist info emode opts fn tm

704704 let (ns', eargs) = unzip $

705705 sortBy cmpArg (zip ns args)

706706 ulog <- getUnifyLog

707+

708+ annot <- findHighlight f

709+ highlightSource ffc annot

710+ trace ("highlighting " ++ show f ++ " at " ++ show ffc ++ " as " ++ show annot) $ return ()

711+

707712 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

708713 [] fc False f

709714 (zip ns' (unmatchableArgs ++ repeat False))

@@ -1277,7 +1282,7 @@ elab ist info emode opts fn tm

12771282 elabArgs ist ina failed fc retry f [] force _ = return ()

12781283 elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)

12791284 = do hs <- get_holes

1280− if holeName `elem` hs then

1285+ if holeName `elem` hs then

12811286 do focus holeName

12821287 case t of

12831288 Placeholder -> do movelast holeName

src/Idris/ParseHelpers.hs+10−2

@@ -278,6 +278,12 @@ reservedOp name = token $ try $

278278 do string name

279279 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

280280

281+reservedOpFC :: MonadicParsing m => String -> m FC

282+reservedOpFC name = token $ try $ do (FC f (l, c) _) <- getFC

283+ string name

284+ notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

285+ return (FC f (l, c) (l, c + length name))

286+

281287-- | Parses an identifier as a token

282288identifier :: (MonadicParsing m) => m (String, FC)

283289identifier = try(do (i, fc) <-

@@ -303,14 +309,16 @@ maybeWithNS parser ascend bad = do

303309 (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))

304310 return (mkName (x, xs), fc)

305311 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

306− parserNoNS parser = do (x, fc) <- parser; return (x, "", fc)

312+ parserNoNS parser = do startFC <- getFC

313+ (x, nameFC) <- parser

314+ return (x, "", spanFC startFC nameFC)

307315 parserNS :: MonadicParsing m => m (String, FC) -> String -> m (String, String, FC)

308316 parserNS parser ns = do startFC <- getFC

309317 xs <- string ns

310318 lchar '.'; (x, nameFC) <- parser

311319 return (x, xs, spanFC startFC nameFC)

312320 parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

313− parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

321+ parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

314322

315323-- | Parses a name

316324name :: IdrisParser (Name, FC)

src/Idris/ParseOps.hs+7−6

@@ -47,7 +47,7 @@ table fixes

4747 flatten t = t

4848

4949

50−-- | Calculates table for fixtiy declarations

50+-- | Calculates table for fixity declarations

5151toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

5252toTable fs = map (map toBin)

5353 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

@@ -61,9 +61,8 @@ toTable fs = map (map toBin)

6161

6262-- | Binary operator

6363binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm

64−binary name f = Infix (do fc <- getFC

65− indentPropHolds gtProp

66− reservedOp name

64+binary name f = Infix (do indentPropHolds gtProp

65+ fc <- reservedOpFC name

6766 indentPropHolds gtProp

6867 return (f fc))

6968

@@ -106,8 +105,10 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

106105 op <- lchar '(' *> reservedOp "=" <* lchar ')'

107106 return (eqTy, FC f (l, c) (l, c+3)))

108107 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

109− op <- lchar '(' *> operator <* lchar ')'

110− return (op, (FC f (l, c) (l, c+1)))) False []

108+ op <- lchar '(' *> operator

109+ (FC _ _ (l', c')) <- getFC

110+ lchar ')'

111+ return (op, (FC f (l, c) (l', c' + 1)))) False []

111112

112113{- | Parses a function (either normal name or operator)

113114