rename "Tag" highlight to "Constant"
This commit is contained in:
parent
2f8a2d2cd2
commit
3b9a339e5e
5 changed files with 29 additions and 29 deletions
|
@ -139,7 +139,7 @@ parameters {opts : LayoutOpts} (showContext : Bool)
|
|||
|
||||
prettyError (WrongFail str err loc) = pure $
|
||||
vsep [!(prettyLoc loc),
|
||||
"wrong error, expected to match", !(hl Tag $ text "\"\{str}\""),
|
||||
"wrong error, expected to match", !(hl Constant $ text "\"\{str}\""),
|
||||
"but got", !(prettyError err)]
|
||||
|
||||
prettyError (WrapParseError file err) =
|
||||
|
|
|
@ -41,7 +41,7 @@ data HL
|
|||
| Dim | DVar | DVarErr
|
||||
| Qty | Universe
|
||||
| Syntax
|
||||
| Tag
|
||||
| Constant
|
||||
%runElab derive "HL" [Eq, Ord, Show]
|
||||
|
||||
|
||||
|
@ -86,7 +86,7 @@ toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
|
|||
toSGR Qty = [SetForeground BrightMagenta]
|
||||
toSGR Universe = [SetForeground BrightRed]
|
||||
toSGR Syntax = [SetForeground BrightCyan]
|
||||
toSGR Tag = [SetForeground BrightRed]
|
||||
toSGR Constant = [SetForeground BrightRed]
|
||||
|
||||
export %inline
|
||||
highlightSGR : HL -> Highlight
|
||||
|
@ -272,8 +272,8 @@ typecaseD = hl Syntax $ text "type-case"
|
|||
ofD = hl Syntax $ text "of"
|
||||
returnD = hl Syntax $ text "return"
|
||||
dotD = hl Delim $ text "."
|
||||
zeroD = hl Syntax $ text "zero"
|
||||
succD = hl Syntax $ text "succ"
|
||||
zeroD = hl Constant $ text "zero"
|
||||
succD = hl Constant $ text "succ"
|
||||
coeD = hl Syntax $ text "coe"
|
||||
compD = hl Syntax $ text "comp"
|
||||
undD = hl Syntax $ text "_"
|
||||
|
@ -330,13 +330,13 @@ prettyLoc (L (YesLoc file b)) =
|
|||
|
||||
export
|
||||
prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts)
|
||||
prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag
|
||||
prettyTag tag = hl Constant $ text $ "'" ++ quoteTag tag
|
||||
|
||||
export
|
||||
prettyStrLit : {opts : _} -> String -> Eff Pretty (Doc opts)
|
||||
prettyStrLit s =
|
||||
let s = concatMap esc1 $ unpack s in
|
||||
hl Syntax $ hcat ["\"", text s, "\""]
|
||||
hl Constant $ hcat ["\"", text s, "\""]
|
||||
where
|
||||
esc1 : Char -> String
|
||||
esc1 '"' = "\""; esc1 '\\' = "\\"
|
||||
|
|
|
@ -287,7 +287,7 @@ prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts)
|
|||
prettyEnum cases =
|
||||
tightBraces =<<
|
||||
fillSeparateTight !commaD <$>
|
||||
traverse (hl Tag . Doc.text . quoteTag) cases
|
||||
traverse (hl Constant . Doc.text . quoteTag) cases
|
||||
|
||||
private
|
||||
prettyCaseRet : {opts : _} ->
|
||||
|
|
|
@ -363,9 +363,9 @@ prettySexp (L (x :: xs)) = do
|
|||
parens $ ifMultiline
|
||||
(hsep $ d :: ds)
|
||||
(hsep [d, vsep ds] <|> vsep (d :: map (indent 2) ds))
|
||||
prettySexp (Q (V x)) = hl Tag $ "'" <+> prettyId' x
|
||||
prettySexp (Q x) = pure $ hcat [!(hl Tag "'"), !(prettySexp x)]
|
||||
prettySexp (N n) = hl Tag $ pshow n
|
||||
prettySexp (Q (V x)) = hl Constant $ "'" <+> prettyId' x
|
||||
prettySexp (Q x) = pure $ hcat [!(hl Constant "'"), !(prettySexp x)]
|
||||
prettySexp (N n) = hl Constant $ pshow n
|
||||
prettySexp (S s) = prettyStrLit $ escape s
|
||||
prettySexp (Lambda xs e) = prettyLambda "lambda" xs e
|
||||
prettySexp (LambdaC xs e) = prettyLambda "lambda%" xs e
|
||||
|
|
|
@ -226,7 +226,7 @@ prettyTerm xs (CaseEnum tag cases _) =
|
|||
prettyCase xs prettyTag tag $
|
||||
map (\(t, rhs) => MkPrettyCaseArm t [] rhs) $ toList cases
|
||||
prettyTerm xs (Absurd _) = hl Syntax "absurd"
|
||||
prettyTerm xs (Nat n _) = hl Tag $ pshow n
|
||||
prettyTerm xs (Nat n _) = hl Constant $ pshow n
|
||||
prettyTerm xs (Succ nat _) = prettyApp xs !succD [< nat]
|
||||
prettyTerm xs (CaseNat nat zer suc _) =
|
||||
prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
|
||||
|
|
Loading…
Reference in a new issue