git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1550 from david-christiansen/pprint-command

Improvements to :pprint - constant highlighting and IDE support

commitf3ecd9073e3f81f6c48988c4f22e96ed4a22a5cc authorDavid Christiansen <david@davidchristiansen.dk> dateFri 26 Sep 2014, 09:29 (12 years ago) parent20b02c55194bf1
2 files changed+8−4
compare with master
unifiedsplit
src/Idris/Output.hs+5−2 src/Idris/REPL.hs+3−2
src/Idris/Output.hs+5−2
@@ -201,7 +201,9 @@ renderExternal fmt width doc
201201 decorate HTMLOutput (AnnName _ _ _ _) = id
202202 decorate HTMLOutput (AnnBoundName _ True) = tag "idris-bound idris-implicit" Nothing
203203 decorate HTMLOutput (AnnBoundName _ False) = tag "idris-bound" Nothing
204− decorate HTMLOutput (AnnConst _) = id -- TODO
204+ decorate HTMLOutput (AnnConst c) =
205+ tag (if constIsType c then "idris-type" else "idris-data")
206+ (Just $ constDocs c)
205207 decorate HTMLOutput (AnnData _ _) = tag "idris-data" Nothing
206208 decorate HTMLOutput (AnnType _ _) = tag "idris-type" Nothing
207209 decorate HTMLOutput AnnKeyword = tag "idris-keyword" Nothing
@@ -222,7 +224,8 @@ renderExternal fmt width doc
222224 decorate LaTeXOutput (AnnName _ _ _ _) = id
223225 decorate LaTeXOutput (AnnBoundName _ True) = latex "IdrisImplicit"
224226 decorate LaTeXOutput (AnnBoundName _ False) = latex "IdrisBound"
225− decorate LaTeXOutput (AnnConst _) = id -- TODO
227+ decorate LaTeXOutput (AnnConst c) =
228+ latex $ if constIsType c then "IdrisType" else "IdrisData"
226229 decorate LaTeXOutput (AnnData _ _) = latex "IdrisData"
227230 decorate LaTeXOutput (AnnType _ _) = latex "IdrisType"
228231 decorate LaTeXOutput AnnKeyword = latex "IdrisKeyword"
src/Idris/REPL.hs+3−2
@@ -575,6 +575,7 @@ ideslaveProcess fn (Apropos a) = do process fn (Apropos a)
575575ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)
576576ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)
577577ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)
578+ideslaveProcess fn (PPrint fmt n tm) = process fn (PPrint fmt n tm)
578579ideslaveProcess fn _ = iPrintError "command not recognized or not supported"
579580
580581
@@ -1189,7 +1190,7 @@ process fn (PrintDef n) =
11891190
11901191process fn (PPrint fmt width (PRef _ n))
11911192 = do outs <- pprintDef n
1192− iputStrLn =<< renderExternal fmt width (vsep outs)
1193+ iPrintResult =<< renderExternal fmt width (vsep outs)
11931194
11941195
11951196process fn (PPrint fmt width t)
@@ -1198,7 +1199,7 @@ process fn (PPrint fmt width t)
11981199 ist <- getIState
11991200 let ppo = ppOptionIst ist
12001201 ty' = normaliseC ctxt [] ty
1201− iputStrLn =<< renderExternal fmt width (pprintDelab ist tm)
1202+ iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
12021203
12031204
12041205showTotal :: Totality -> IState -> String