add html output highlighting
This commit is contained in:
parent
040a1862c3
commit
c48b7be559
3 changed files with 57 additions and 22 deletions
16
exe/Main.idr
16
exe/Main.idr
|
@ -27,13 +27,18 @@ die opts err = do
|
||||||
ignore $ fPutStr stderr $ render opts err
|
ignore $ fPutStr stderr $ render opts err
|
||||||
exitFailure
|
exitFailure
|
||||||
|
|
||||||
|
private
|
||||||
|
hlFor : HLType -> OutFile -> HL -> Highlight
|
||||||
|
hlFor Guess Console = highlightSGR
|
||||||
|
hlFor Guess _ = noHighlight
|
||||||
|
hlFor NoHL _ = noHighlight
|
||||||
|
hlFor Term _ = highlightSGR
|
||||||
|
hlFor Html _ = highlightHtml
|
||||||
|
|
||||||
private
|
private
|
||||||
runPretty : Options -> Eff Pretty a -> a
|
runPretty : Options -> Eff Pretty a -> a
|
||||||
runPretty opts act =
|
runPretty opts act =
|
||||||
let doColor = opts.color && opts.outFile == Console
|
runPrettyWith Outer opts.flavor (hlFor opts.hlType opts.outFile) 2 act
|
||||||
hl = if doColor then highlightSGR else noHighlight
|
|
||||||
in
|
|
||||||
runPrettyWith Outer opts.flavor hl 2 act
|
|
||||||
|
|
||||||
private
|
private
|
||||||
putErrLn : HasIO io => String -> io ()
|
putErrLn : HasIO io => String -> io ()
|
||||||
|
@ -133,7 +138,7 @@ private
|
||||||
outputStr : Lazy String -> Eff Compile ()
|
outputStr : Lazy String -> Eff Compile ()
|
||||||
outputStr str =
|
outputStr str =
|
||||||
case !(asksAt OPTS outFile) of
|
case !(asksAt OPTS outFile) of
|
||||||
None => pure ()
|
NoOut => pure ()
|
||||||
Console => putStr str
|
Console => putStr str
|
||||||
File f => do
|
File f => do
|
||||||
res <- withFile f WriteTruncate pure $ \h => fPutStr h str
|
res <- withFile f WriteTruncate pure $ \h => fPutStr h str
|
||||||
|
@ -187,6 +192,7 @@ oneMain [] = throw NoMain
|
||||||
oneMain [x] = pure x
|
oneMain [x] = pure x
|
||||||
oneMain mains = throw $ MultipleMains mains
|
oneMain mains = throw $ MultipleMains mains
|
||||||
|
|
||||||
|
|
||||||
private
|
private
|
||||||
processFile : String -> Eff Compile ()
|
processFile : String -> Eff Compile ()
|
||||||
processFile file = withEarlyStop $ do
|
processFile file = withEarlyStop $ do
|
||||||
|
|
|
@ -11,7 +11,7 @@ import Derive.Prelude
|
||||||
%language ElabReflection
|
%language ElabReflection
|
||||||
|
|
||||||
public export
|
public export
|
||||||
data OutFile = File String | Console | None
|
data OutFile = File String | Console | NoOut
|
||||||
%name OutFile f
|
%name OutFile f
|
||||||
%runElab derive "OutFile" [Eq, Ord, Show]
|
%runElab derive "OutFile" [Eq, Ord, Show]
|
||||||
|
|
||||||
|
@ -28,10 +28,15 @@ allPhases = %runElab do
|
||||||
cs <- getCons $ fst !(lookupName "Phase")
|
cs <- getCons $ fst !(lookupName "Phase")
|
||||||
traverse (check . var) cs
|
traverse (check . var) cs
|
||||||
|
|
||||||
|
||| "guess" is Term for a terminal and NoHL for a file
|
||||||
|
public export
|
||||||
|
data HLType = Guess | NoHL | Term | Html
|
||||||
|
%runElab derive "HLType" [Eq, Ord, Show]
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record Options where
|
record Options where
|
||||||
constructor MkOpts
|
constructor MkOpts
|
||||||
color : Bool
|
hlType : HLType
|
||||||
outFile : OutFile
|
outFile : OutFile
|
||||||
until : Maybe Phase
|
until : Maybe Phase
|
||||||
flavor : Pretty.Flavor
|
flavor : Pretty.Flavor
|
||||||
|
@ -49,7 +54,7 @@ defaultWidth = do
|
||||||
export
|
export
|
||||||
defaultOpts : IO Options
|
defaultOpts : IO Options
|
||||||
defaultOpts = pure $ MkOpts {
|
defaultOpts = pure $ MkOpts {
|
||||||
color = True,
|
hlType = Guess,
|
||||||
outFile = Console,
|
outFile = Console,
|
||||||
until = Nothing,
|
until = Nothing,
|
||||||
flavor = Unicode,
|
flavor = Unicode,
|
||||||
|
@ -66,7 +71,7 @@ data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
|
||||||
|
|
||||||
private
|
private
|
||||||
toOutFile : String -> OptAction
|
toOutFile : String -> OptAction
|
||||||
toOutFile "" = Ok {outFile := None}
|
toOutFile "" = Ok {outFile := NoOut}
|
||||||
toOutFile "-" = Ok {outFile := Console}
|
toOutFile "-" = Ok {outFile := Console}
|
||||||
toOutFile f = Ok {outFile := File f}
|
toOutFile f = Ok {outFile := File f}
|
||||||
|
|
||||||
|
@ -85,6 +90,14 @@ toWidth s = case parsePositive s of
|
||||||
Just n => Ok {width := n}
|
Just n => Ok {width := n}
|
||||||
Nothing => Err "invalid width: \{show s}"
|
Nothing => Err "invalid width: \{show s}"
|
||||||
|
|
||||||
|
private
|
||||||
|
toHLType : String -> OptAction
|
||||||
|
toHLType str = case toLower str of
|
||||||
|
"none" => Ok {hlType := NoHL}
|
||||||
|
"term" => Ok {hlType := Term}
|
||||||
|
"html" => Ok {hlType := Html}
|
||||||
|
_ => Err "unknown highlighting type \{str}\ntypes: term, html, none"
|
||||||
|
|
||||||
private
|
private
|
||||||
commonOptDescrs' : List (OptDescr OptAction)
|
commonOptDescrs' : List (OptDescr OptAction)
|
||||||
commonOptDescrs' = [
|
commonOptDescrs' = [
|
||||||
|
@ -105,10 +118,8 @@ extraOptDescrs = [
|
||||||
"use ascii syntax when printing",
|
"use ascii syntax when printing",
|
||||||
MkOpt [] ["width"] (ReqArg toWidth "<width>")
|
MkOpt [] ["width"] (ReqArg toWidth "<width>")
|
||||||
"max output width (defaults to terminal width)",
|
"max output width (defaults to terminal width)",
|
||||||
MkOpt [] ["color", "colour"] (NoArg $ Ok {color := True})
|
MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
|
||||||
"use colour output (default)",
|
"select highlighting type"
|
||||||
MkOpt [] ["no-color", "no-colour"] (NoArg $ Ok {color := False})
|
|
||||||
"don't use colour output"
|
|
||||||
]
|
]
|
||||||
|
|
||||||
private
|
private
|
||||||
|
@ -123,10 +134,10 @@ allOptDescrs = commonOptDescrs' ++ extraOptDescrs ++ helpOptDescrs
|
||||||
|
|
||||||
export
|
export
|
||||||
usageHeader : String
|
usageHeader : String
|
||||||
usageHeader = joinBy "\n" [
|
usageHeader = trim """
|
||||||
"quox [options] [file.quox ...]",
|
quox [options] [file.quox ...]
|
||||||
"rawr"
|
rawr
|
||||||
]
|
"""
|
||||||
|
|
||||||
export
|
export
|
||||||
usage : List (OptDescr _) -> IO a
|
usage : List (OptDescr _) -> IO a
|
||||||
|
|
|
@ -92,14 +92,32 @@ export %inline
|
||||||
highlightSGR : HL -> Highlight
|
highlightSGR : HL -> Highlight
|
||||||
highlightSGR h = MkHighlight (escapeSGR $ toSGR h) (escapeSGR [Reset])
|
highlightSGR h = MkHighlight (escapeSGR $ toSGR h) (escapeSGR [Reset])
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
toClass : HL -> String
|
||||||
|
toClass Delim = "dl"
|
||||||
|
toClass Free = "fr"
|
||||||
|
toClass TVar = "tv"
|
||||||
|
toClass TVarErr = "tv err"
|
||||||
|
toClass Dim = "dc"
|
||||||
|
toClass DVar = "dv"
|
||||||
|
toClass DVarErr = "dv err"
|
||||||
|
toClass Qty = "qt"
|
||||||
|
toClass Universe = "un"
|
||||||
|
toClass Syntax = "sy"
|
||||||
|
toClass Constant = "co"
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
highlightHtml : HL -> Highlight
|
||||||
|
highlightHtml h = MkHighlight #"<span class="\#{toClass h}">"# "</span>"
|
||||||
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
|
runPrettyHL : (HL -> Highlight) -> Eff Pretty a -> a
|
||||||
|
runPrettyHL f = runPrettyWith Outer Unicode f 2
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
runPretty : Eff Pretty a -> a
|
runPretty : Eff Pretty a -> a
|
||||||
runPretty = runPrettyWith Outer Unicode noHighlight 2
|
runPretty = runPrettyHL noHighlight
|
||||||
|
|
||||||
export %inline
|
|
||||||
runPrettyColor : Eff Pretty a -> a
|
|
||||||
runPrettyColor = runPrettyWith Outer Unicode highlightSGR 2
|
|
||||||
|
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
|
|
Loading…
Reference in a new issue