From a0846af5fa60b3cb48a261b90660fc2f9a896d18 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Mon, 20 Sep 2021 15:19:52 +0100 Subject: [PATCH] [ decor ] highlighting comments too Even though the `Comment` aspect is not (currently) supported in the IDEMode, this is crucial to get proper highlighting in Katla's LaTeX & HTML backends. --- src/Core/Binary.idr | 2 +- src/Core/Metadata.idr | 5 ++++ src/Parser/Lexer/Source.idr | 46 +++++++++++++++++++++++------- src/Parser/Source.idr | 8 ++++-- tests/ideMode/ideMode005/expected7 | 2 ++ tests/ideMode/ideMode005/expected8 | 1 + 6 files changed, 49 insertions(+), 15 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 0b1d72458..958c2c053 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -33,7 +33,7 @@ import public Libraries.Utils.Binary ||| (Increment this when changing anything in the data format) export ttcVersion : Int -ttcVersion = 63 +ttcVersion = 64 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 4931665a0..71e777e6f 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -21,6 +21,7 @@ import Libraries.Utils.Binary public export data Decoration : Type where + Comment : Decoration Typ : Decoration Function : Decoration Data : Decoration @@ -54,6 +55,7 @@ SemanticDecorations = List ASemanticDecoration public export Eq Decoration where + Comment == Comment = True Typ == Typ = True Function == Function = True Data == Data = True @@ -69,6 +71,7 @@ Eq Decoration where -- break the IDE mode. public export Show Decoration where + show Comment = "comment" show Typ = "type" show Function = "function" show Data = "data" @@ -87,6 +90,7 @@ TTC Decoration where toBuf b Namespace = tag 5 toBuf b Postulate = tag 6 toBuf b Module = tag 7 + toBuf b Comment = tag 8 fromBuf b = case !getTag of 0 => pure Typ @@ -97,6 +101,7 @@ TTC Decoration where 5 => pure Namespace 6 => pure Postulate 7 => pure Module + 8 => pure Comment _ => corrupt "Decoration" public export diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 2458c9567..badaffc29 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -2,6 +2,7 @@ module Parser.Lexer.Source import public Parser.Lexer.Common +import Data.Either import Data.List1 import Data.List import Data.Maybe @@ -41,6 +42,8 @@ data Token | DotSepIdent Namespace String -- ident.ident | DotIdent String -- .ident | Symbol String + -- Whitespace + | Space -- Comments | Comment | DocComment String @@ -70,6 +73,8 @@ Show Token where show (DotSepIdent ns n) = "namespaced identifier " ++ show ns ++ "." ++ show n show (DotIdent x) = "dot+identifier " ++ x show (Symbol x) = "symbol " ++ x + -- Whitespace + show Space = "whitespace" -- Comments show Comment = "comment" show (DocComment c) = "doc comment: \"" ++ c ++ "\"" @@ -99,6 +104,8 @@ Pretty Token where pretty (DotSepIdent ns n) = reflow "namespaced identifier" <++> pretty ns <+> dot <+> pretty n pretty (DotIdent x) = pretty "dot+identifier" <++> pretty x pretty (Symbol x) = pretty "symbol" <++> pretty x + -- Whitespace + pretty Space = pretty "space" -- Comments pretty Comment = pretty "comment" pretty (DocComment c) = reflow "doc comment:" <++> dquotes (pretty c) @@ -351,7 +358,7 @@ mutual <|> match namespacedIdent parseNamespace <|> match identNormal parseIdent <|> match pragma (\x => Pragma (assert_total $ strTail x)) - <|> match space (const Comment) + <|> match space (const Space) <|> match validSymbol Symbol <|> match symbol Unrecognised where @@ -377,20 +384,37 @@ mutual export lexTo : Lexer -> - String -> Either (StopReason, Int, Int, String) (List (WithBounds Token)) + String -> + Either (StopReason, Int, Int, String) + ( List (WithBounds ()) -- bounds of comments + , List (WithBounds Token)) -- tokens lexTo reject str = case lexTo reject rawTokens str of - -- Add the EndInput token so that we'll have a line and column - -- number to read when storing spans in the file - (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++ - [MkBounded EndInput False (MkBounds l c l c)]) + (toks, (EndInput, l, c, _)) => + -- Add the EndInput token so that we'll have a line and column + -- number to read when storing spans in the file + let end = [MkBounded EndInput False (MkBounds l c l c)] in + Right $ map (++ end) + $ partitionEithers + $ map spotComment + $ filter isNotSpace toks (_, fail) => Left fail where - notComment : WithBounds Token -> Bool - notComment t = case t.val of - Comment => False - _ => True + + isNotSpace : WithBounds Token -> Bool + isNotSpace t = case t.val of + Space => False + _ => True + + spotComment : WithBounds Token -> + Either (WithBounds ()) (WithBounds Token) + spotComment t = case t.val of + Comment => Left (() <$ t) + _ => Right t export -lex : String -> Either (StopReason, Int, Int, String) (List (WithBounds Token)) +lex : String -> + Either (StopReason, Int, Int, String) + ( List (WithBounds ()) -- bounds of comments + , List (WithBounds Token)) -- tokens lex = lexTo (pred $ const False) diff --git a/src/Parser/Source.idr b/src/Parser/Source.idr index d9e829a0e..6da5b5270 100644 --- a/src/Parser/Source.idr +++ b/src/Parser/Source.idr @@ -20,13 +20,15 @@ runParserTo : {e : _} -> String -> Grammar SemanticDecorations Token e ty -> Either Error (List Warning, SemanticDecorations, ty) runParserTo origin lit reject str p - = do str <- mapFst (fromLitError origin) $ unlit lit str - toks <- mapFst (fromLexError origin) $ lexTo reject str + = do str <- mapFst (fromLitError origin) $ unlit lit str + (cs, toks) <- mapFst (fromLexError origin) $ lexTo reject str (decs, ws, (parsed, _)) <- mapFst (fromParsingErrors origin) $ parseWith p toks + let cs : SemanticDecorations + = cs <&> \ c => ((origin, start c, end c), Comment, Nothing) let ws = ws <&> \ (mb, warn) => let mkFC = \ b => MkFC origin (startBounds b) (endBounds b) in ParserWarning (maybe EmptyFC mkFC mb) warn - Right (ws, decs, parsed) + Right (ws, cs ++ decs, parsed) export runParser : {e : _} -> diff --git a/tests/ideMode/ideMode005/expected7 b/tests/ideMode/ideMode005/expected7 index 1dea3d824..6b69a83c3 100644 --- a/tests/ideMode/ideMode005/expected7 +++ b/tests/ideMode/ideMode005/expected7 @@ -81,6 +81,7 @@ 0000c6(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 15 8) (:end 15 8)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) 000073(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 15 10) (:end 15 11)) ((:decor :keyword)))))) 1) 0000c9(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 15 13) (:end 15 14)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) +000072(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 16 8) (:end 16 17)) ((:decor :comment)))))) 1) 000072(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 17 8) (:end 17 10)) ((:decor :keyword)))))) 1) 0000d8(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 17 12) (:end 17 15)) ((:name "True") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) 000073(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 17 17) (:end 17 17)) ((:decor :keyword)))))) 1) @@ -90,6 +91,7 @@ 0000d9(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 18 12) (:end 18 16)) ((:name "False") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) 000073(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 18 18) (:end 18 19)) ((:decor :keyword)))))) 1) 0000d7(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 18 21) (:end 18 22)) ((:name "Nil") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) +000072(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 19 8) (:end 19 16)) ((:decor :comment)))))) 1) 0000d7(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 20 8) (:end 20 11)) ((:name "True") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) 000073(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 20 13) (:end 20 14)) ((:decor :keyword)))))) 1) 0000e0(:output (:ok (:highlight-source ((((:filename "Case.idr") (:start 20 16) (:end 20 19)) ((:name "pure") (:namespace "Prelude.Interfaces") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) diff --git a/tests/ideMode/ideMode005/expected8 b/tests/ideMode/ideMode005/expected8 index b7dcc78b9..6f7155569 100644 --- a/tests/ideMode/ideMode005/expected8 +++ b/tests/ideMode/ideMode005/expected8 @@ -47,6 +47,7 @@ 00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 25) (:end 13 25)) ((:decor :keyword)))))) 1) 0000e1(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 27) (:end 13 27)) ((:name ".") (:namespace "Prelude.Basics") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) 0000e5(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 13 29) (:end 13 35)) ((:name "bigMono") (:namespace "RecordUpdate") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1) +00007a(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 15 1) (:end 15 23)) ((:decor :comment)))))) 1) 000079(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 1) (:end 16 6)) ((:decor :keyword)))))) 1) 000077(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 8) (:end 16 11)) ((:decor :type)))))) 1) 00007b(:output (:ok (:highlight-source ((((:filename "RecordUpdate.idr") (:start 16 13) (:end 16 17)) ((:decor :keyword)))))) 1)