d75c5ba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4114 from joom/master

d75c5baNiklas Larsson9 years ago

CHANGELOG.md+2

compare with master

unifiedsplit

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

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

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

25 as they were given in the source files.

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

27+ in LaTeX.

27# New in 1.1.1

29# New in 1.1.1

src/Idris/AbsSyntaxTree.hs+9−5

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

1697 where

1698 startPrec = 0

1699 funcAppPrec = 10

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

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

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

1700

1703

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

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

1702 prettySe d p bnd (PQuote r) =

1705 prettySe d p bnd (PQuote r) =

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

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

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

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

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

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

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

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

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

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

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

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

1714 where

1718 where

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

1719 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

1749

1753

1750 st =

1754 st =

1751 case s of

1755 case s of

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

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

1753 _ -> empty

1757 _ -> empty

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

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

1755 | ppopt_impl ppo =

1759 | ppopt_impl ppo =

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

1769

1773

1770 st =

1774 st =

1771 case s of

1775 case s of

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

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

1773 _ -> empty

1777 _ -> empty

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

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

1775 depth d . bracket p startPrec $

1779 depth d . bracket p startPrec $

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

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

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

1877 ]

1881 ]

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

1882 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"

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

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

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

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

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

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

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

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

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

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

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

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

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

1984− text "%runElab" <$>

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

1985 prettySe (decD d) funcAppPrec bnd tm

1989 prettySe (decD d) funcAppPrec bnd tm

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

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

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

1991 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

224 -- from that file.

225 | AnnQuasiquote

226 | AnnAntiquote

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

227 deriving (Show, Eq, Generic)

228 deriving (Show, Eq, Generic)

228

229

229-- | Used for error reflection

230-- | Used for error reflection

src/Idris/IdeMode.hs+1

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

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

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

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

175+ toSExp (AnnSyntax c) = SexpList []

175

176

176encodeName :: Name -> String

177encodeName :: Name -> String

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

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

src/Idris/Output.hs+8

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

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

319 decorate HTMLOutput AnnQuasiquote = id

320 decorate HTMLOutput AnnAntiquote = id

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

321

322

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

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

323 latex "IdrisType"

324 latex "IdrisType"

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

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

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

350 decorate LaTeXOutput AnnQuasiquote = id

351 decorate LaTeXOutput AnnQuasiquote = id

351 decorate LaTeXOutput AnnAntiquote = id

352 decorate LaTeXOutput AnnAntiquote = id

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

354+ case c of

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

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

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

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

359+ _ -> c

352

360

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

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

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

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