d75c5ba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4114 from joom/master

Fix LaTeX pretty printing of backslash, braces and percent

commitd75c5baf6770687469570dd57dcdbec8b9b30361 authorNiklas Larsson <metaniklas@gmail.com> dateWed 11 Oct 2017, 14:26 (9 years ago) parenta122109 897eaa8

5 files changed+21−5

compare with master

unifiedsplit

CHANGELOG.md+2 src/Idris/AbsSyntaxTree.hs+9−5 src/Idris/Core/TT.hs+1 src/Idris/IdeMode.hs+1 src/Idris/Output.hs+8

CHANGELOG.md+2

@@ -23,6 +23,8 @@

2323+ The --interface option now creates CommonJS modules on the node backend.

2424+ The C backend now pass arguments to the C compiler in the same order

2525 as they were given in the source files.

26++ Backslash, braces and percent symbols are now correctly pretty printed

27+ in LaTeX.

2628

2729# New in 1.1.1

2830

src/Idris/AbsSyntaxTree.hs+9−5

@@ -1697,6 +1697,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16971697 where

16981698 startPrec = 0

16991699 funcAppPrec = 10

1700+ lbrace = annotate (AnnSyntax "{") (text "{")

1701+ rbrace = annotate (AnnSyntax "}") (text "}")

1702+ percent = annotate (AnnSyntax "%") (text "%")

17001703

17011704 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

17021705 prettySe d p bnd (PQuote r) =

@@ -1709,7 +1712,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17091712 prettySe d p bnd (PLam fc n nfc ty sc) =

17101713 let (ns, sc') = getLamNames [n] sc in

17111714 depth d . bracket p startPrec . group . align . hang 2 $

1712− text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>

1715+ (annotate (AnnSyntax "\\") (text "\\"))

1716+ <> prettyBindingsOf ns False <+> text "=>" <$>

17131717 prettySe (decD d) startPrec ((n, False):bnd) sc'

17141718 where

17151719 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc

@@ -1749,7 +1753,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17491753

17501754 st =

17511755 case s of

1752− Static -> text "%static" <> space

1756+ Static -> percent <> text "static" <> space

17531757 _ -> empty

17541758 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)

17551759 | ppopt_impl ppo =

@@ -1769,7 +1773,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17691773

17701774 st =

17711775 case s of

1772− Static -> text "%static" <> space

1776+ Static -> percent <> text "static" <> space

17731777 _ -> empty

17741778 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =

17751779 depth d . bracket p startPrec $

@@ -1876,7 +1880,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18761880 , kwd "else" <+> prettySe (decD d) startPrec bnd f

18771881 ]

18781882 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm

1879− prettySe d p bnd (PResolveTC _) = kwd "%implementation"

1883+ prettySe d p bnd (PResolveTC _) = percent <> kwd "implementation"

18801884 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"

18811885 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

18821886 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

@@ -1981,7 +1985,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

19811985 end = if res then "}" else "}}"

19821986 prettySe d p bnd (PRunElab _ tm _) =

19831987 bracket p funcAppPrec . group . align . hang 2 $

1984− text "%runElab" <$>

1988+ (percent <> text "runElab") <$>

19851989 prettySe (decD d) funcAppPrec bnd tm

19861990 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

19871991 prettySe d p bnd _ = text "missing pretty-printer for term"

src/Idris/Core/TT.hs+1

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

224224 -- from that file.

225225 | AnnQuasiquote

226226 | AnnAntiquote

227+ | AnnSyntax String -- ^ type of syntax element: backslash or braces etc.

227228 deriving (Show, Eq, Generic)

228229

229230-- | Used for error reflection

src/Idris/IdeMode.hs+1

@@ -172,6 +172,7 @@ instance SExpable OutputAnnotation where

172172 maybeProps [("source-file", file)]

173173 toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]

174174 toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]

175+ toSExp (AnnSyntax c) = SexpList []

175176

176177encodeName :: Name -> String

177178encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

src/Idris/Output.hs+8

@@ -318,6 +318,7 @@ renderExternal fmt width doc

318318 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"

319319 decorate HTMLOutput AnnQuasiquote = id

320320 decorate HTMLOutput AnnAntiquote = id

321+ decorate HTMLOutput (AnnSyntax c) = \txt -> c

321322

322323 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

323324 latex "IdrisType"

@@ -349,6 +350,13 @@ renderExternal fmt width doc

349350 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")

350351 decorate LaTeXOutput AnnQuasiquote = id

351352 decorate LaTeXOutput AnnAntiquote = id

353+ decorate LaTeXOutput (AnnSyntax c) = \txt ->

354+ case c of

355+ "\\" -> "\\textbackslash"

356+ "{" -> "\\{"

357+ "}" -> "\\}"

358+ "%" -> "\\%"

359+ _ -> c

352360

353361 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

354362 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs