diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index e6f4a17..a26100b 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -249,7 +249,7 @@ prettyDBind = hl DVar . prettyBind' export %inline typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, -stringD, eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, +stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD, ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD : {opts : LayoutOpts} -> Eff Pretty (Doc opts) typeD = hl Syntax . text =<< ifUnicode "★" "Type" @@ -267,6 +267,7 @@ eqD = hl Syntax $ text "Eq" colonD = hl Delim $ text ":" commaD = hl Delim $ text "," semiD = hl Delim $ text ";" +atD = hl Delim $ text "@" caseD = hl Syntax $ text "case" typecaseD = hl Syntax $ text "type-case" ofD = hl Syntax $ text "of" diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index cc1784d..ae2b565 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -201,8 +201,7 @@ prettyTArg dnames tnames s = private prettyDArg : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts) -prettyDArg dnames p = - map (text "@" <+>) $ withPrec Arg $ prettyDim dnames p +prettyDArg dnames p = [|atD <+> withPrec Arg (prettyDim dnames p)|] private splitApps : Elim d n -> (Elim d n, List (Either (Dim d) (Term d n)))