diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index ac70fed96..ea325ce02 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -26,21 +26,23 @@ compileToJS : Ref Ctxt Defs -> compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"] htmlHeader : String -htmlHeader = concat $ the (List String) $ - [ "\n" - , " \n" - , " \n" - , " \n" - , " \n" - , " \n" - , " \n" - , "" - ] +htmlFooter = """ + + + + + """ addHeaderAndFooter : String -> String -> String addHeaderAndFooter outfile es = diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5b12cc11a..f73ea3e9b 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -989,29 +989,35 @@ header : {auto c : Ref Ctxt Defs} -> {auto h : Ref HeaderFiles (SortedSet String)} -> Core () header = do - let initLines = [ "#include " - , "/* " ++ (generatedString "RefC") ++" */"] + let initLines = """ + #include + /* \{ generatedString "RefC" } */ + + """ let headerFiles = Libraries.Data.SortedSet.toList !(get HeaderFiles) let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles fns <- get FunctionDefinitions - update OutfileText (appendL (initLines ++ headerLines ++ ["\n// function definitions"] ++ fns)) + update OutfileText (appendL ([initLines] ++ headerLines ++ ["\n// function definitions"] ++ fns)) footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText Output} -> {auto h : Ref HeaderFiles (SortedSet String)} -> Core () footer = do - emit EmptyFC "" - emit EmptyFC " // main function" - emit EmptyFC "int main(int argc, char *argv[])" - emit EmptyFC "{" - if contains "idris_support.h" !(get HeaderFiles) - then emit EmptyFC " idris2_setArgs(argc, argv);" - else pure () - emit EmptyFC " Value *mainExprVal = __mainExpression_0();" - emit EmptyFC " trampoline(mainExprVal);" - emit EmptyFC " return 0; // bye bye" - emit EmptyFC "}" + emit EmptyFC """ + + // main function + int main(int argc, char *argv[]) + { + \{ ifThenElse (contains "idris_support.h" !(get HeaderFiles)) + "idris2_setArgs(argc, argv);" + "" + } + Value *mainExprVal = __mainExpression_0(); + trampoline(mainExprVal); + return 0; // bye bye + } + """ export executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 4ea9922d5..f974f0566 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -87,28 +87,33 @@ schHeader : String -> List String -> Bool -> String schHeader chez libs whole = (if os /= "windows" then "#!" ++ chez ++ (if whole then " --program\n\n" else " --script\n\n") - else "") ++ - "; " ++ (generatedString "Chez") ++ "\n" ++ - "(import (chezscheme))\n" ++ - "(case (machine-type)\n" ++ - " [(i3fb ti3fb a6fb ta6fb) #f]\n" ++ - " [(i3le ti3le a6le ta6le tarm64le) (load-shared-object \"libc.so.6\")]\n" ++ - " [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object \"libc.dylib\")]\n" ++ - " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++ - " [else (load-shared-object \"libc.so\")])\n\n" ++ - showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++ - if whole - then "(let ()\n" - else "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))\n" + else "") ++ """ + ;; \{ generatedString "Chez" } + (import (chezscheme)) + (case (machine-type) + [(i3fb ti3fb a6fb ta6fb) #f] + [(i3le ti3le a6le ta6le tarm64le) (load-shared-object "libc.so.6")] + [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object "libc.dylib")] + [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")] + [else (load-shared-object "libc.so")]) + + \{ showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) } + + \{ ifThenElse whole + "(let ()" + "(source-directories (cons (getenv \"IDRIS2_INC_SRC\") (source-directories)))" + } + + """ schFooter : Bool -> Bool -> String -schFooter prof whole - = "(collect 4)\n(blodwen-run-finalisers)\n" ++ - (if prof - then "(profile-dump-html)" - else "") ++ - (if whole - then ")\n" else "\n") +schFooter prof whole = """ + + (collect 4) + (blodwen-run-finalisers) + \{ ifThenElse prof "(profile-dump-html)" "" } + \{ ifThenElse whole ")" "" } + """ showChezChar : Char -> String -> String showChezChar '\\' = ("\\\\" ++) @@ -385,49 +390,56 @@ getFgnCall version (n, fc, d) = schFgnDef fc n d version export startChezPreamble : String -startChezPreamble = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Chez") - , "" - , "set -e # exit on any error" - , "" - , "if [ \"$(uname)\" = Darwin ]; then" - , " DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")" - , "else" - , " DIR=$(dirname \"$(readlink -f -- \"$0\")\")" - , "fi" - , "" -- so that the preamble ends with a newline - ] +startChezPreamble = """ + #!/bin/sh + # \{ generatedString "Chez" } + + set -e # exit on any error + + if [ "$(uname)" = Darwin ]; then + DIR=$(zsh -c 'printf %s "$0:A:h"' "$0") + else + DIR=$(dirname "$(readlink -f -- "$0")") + fi + + """ startChez : String -> String -> String -startChez appdir target = startChezPreamble ++ unlines - [ "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$LD_LIBRARY_PATH\"" - , "export DYLD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$DYLD_LIBRARY_PATH\"" - , "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\"" - , "\"$DIR/" ++ target ++ "\" \"$@\"" - ] +startChez appdir target = startChezPreamble ++ """ + export LD_LIBRARY_PATH="$DIR/\{ appdir }:$LD_LIBRARY_PATH" + export DYLD_LIBRARY_PATH="$DIR/\{ appdir }:$DYLD_LIBRARY_PATH" + export IDRIS2_INC_SRC="$DIR/\{ appdir }" + + "$DIR/\{ target }" "$@" + """ startChezCmd : String -> String -> String -> String -> String -startChezCmd chez appdir target progType = unlines - [ "@echo off" - , "set APPDIR=%~dp0" - , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%" - , "set IDRIS2_INC_SRC=%APPDIR%" ++ appdir - , "\"" ++ chez ++ "\" " ++ progType ++ " \"%APPDIR%" ++ target ++ "\" %*" - ] +startChezCmd chez appdir target progType = """ + @echo off + + rem \{ generatedString "Chez" } + + set APPDIR=%~dp0 + set PATH=%APPDIR%\{ appdir };%PATH% + set IDRIS2_INC_SRC=%APPDIR%\{ appdir } + + "\{ chez }" \{ progType } "%APPDIR%\{ target }" %* + """ startChezWinSh : String -> String -> String -> String -> String -startChezWinSh chez appdir target progType = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Chez") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\"" - , "export IDRIS2_INC_SRC=\"$DIR/" ++ appdir ++ "\"" - , "\"" ++ chez ++ "\" " ++ progType ++ " \"$DIR/" ++ target ++ "\" \"$@\"" - ] +startChezWinSh chez appdir target progType = """ + #!/bin/sh + # \{ generatedString "Chez" } + + set -e # exit on any error + + DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") + PATH="$DIR/\{ appdir }:$PATH" + + export IDRIS2_INC_SRC="$DIR/\{ appdir }" + + "\{ chez }" \{ progType } "$DIR/\{ target }" "$@" + """ ||| Compile a TT expression to Chez Scheme compileToSS : Ref Ctxt Defs -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index a78a120e1..455b2ac87 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -39,59 +39,67 @@ import Libraries.Utils.String %default covering schHeader : List String -> List String -> String -schHeader libs compilationUnits = unlines - [ "(import (chezscheme) (support) " - ++ unwords ["(" ++ cu ++ ")" | cu <- compilationUnits] - ++ ")" - , "(case (machine-type)" - , " [(i3le ti3le a6le ta6le tarm64le) (load-shared-object \"libc.so.6\")]" - , " [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object \"libc.dylib\")]" - , " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" - , " (load-shared-object \"ws2_32.dll\")]" - , " [else (load-shared-object \"libc.so\")]" - , unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] - , ")" - ] +schHeader libs compilationUnits = """ + (import (chezscheme) (support) + \{ unwords ["(" ++ cu ++ ")" | cu <- compilationUnits] }) + (case (machine-type) + [(i3le ti3le a6le ta6le tarm64le) (load-shared-object "libc.so.6")] + [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object "libc.dylib")] + [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")] + [else (load-shared-object "libc.so")] + \{ unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs] }) + + """ schFooter : String -schFooter = "(collect 4)\n(blodwen-run-finalisers)\n" +schFooter = """ + + (collect 4) + (blodwen-run-finalisers) + """ startChez : String -> String -> String -> String -startChez chez appDirSh targetSh = Chez.startChezPreamble ++ unlines - [ "export LD_LIBRARY_PATH=\"$DIR/" ++ appDirSh ++ ":$LD_LIBRARY_PATH\"" - , "export DYLD_LIBRARY_PATH=\"$DIR/" ++ appDirSh ++ ":$DYLD_LIBRARY_PATH\"" - , "\"" ++ chez ++ "\" -q " - ++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" " - ++ "--program \"$DIR/" ++ targetSh ++ "\" " - ++ "\"$@\"" - ] +startChez chez appDirSh targetSh = Chez.startChezPreamble ++ """ + export LD_LIBRARY_PATH="$DIR/\{ appDirSh }:$LD_LIBRARY_PATH" + export DYLD_LIBRARY_PATH="$DIR/\{ appDirSh }:$DYLD_LIBRARY_PATH" + + "\{ chez }" -q \ + --libdirs "$DIR/\{ appDirSh }" \ + --program "$DIR/\{ targetSh }" \ + "$@" + """ startChezCmd : String -> String -> String -> String -startChezCmd chez appDirSh targetSh = unlines - [ "@echo off" - , "set APPDIR=%~dp0" - , "set PATH=%APPDIR%" ++ appDirSh ++ ";%PATH%" - , "\"" ++ chez ++ "\" -q " - ++ "--libdirs \"%APPDIR%" ++ appDirSh ++ "\" " - ++ "--program \"%APPDIR%" ++ targetSh ++ "\" " - ++ "%*" - ] +startChezCmd chez appDirSh targetSh = """ + @echo off + + rem \{ generatedString "ChezSep" } + + set APPDIR=%~dp0 + set PATH=%APPDIR%\{ appDirSh };%PATH% + + "\{ chez }" -q \ + --libdirs "%APPDIR%\{ appDirSh }" \ + --program "%APPDIR%\{ targetSh }" \ + %* + """ startChezWinSh : String -> String -> String -> String -startChezWinSh chez appDirSh targetSh = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Chez") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appDirSh ++ ":$PATH\"" - , "\"" ++ chez ++ "\" --program \"$DIR/" ++ targetSh ++ "\" \"$@\"" - , "\"" ++ chez ++ "\" -q " - ++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" " - ++ "--program \"$DIR/" ++ targetSh ++ "\" " - ++ "\"$@\"" - ] +startChezWinSh chez appDirSh targetSh = """ + #!/bin/sh + # \{ generatedString "ChezSep" } + + set -e # exit on any error + + DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") + PATH="$DIR/\{ appDirSh }:$PATH" + + "\{ chez }" --program "$DIR/\{ targetSh }" "$@" + "\{ chez }" -q \ + --libdirs "$DIR/\{ appDirSh }" \ + --program "$DIR/\{ targetSh }" \ + "$@" + """ -- TODO: parallelise this compileChezLibraries : (chez : String) -> (libDir : String) -> (ssFiles : List String) -> Core () diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 691112a57..acc8a20d7 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -49,14 +49,16 @@ findGSCBackend = Just e => " -cc " ++ e schHeader : String -schHeader = - "; " ++ (generatedString "Gambit") ++ "\n" ++ - "(declare (block)\n" ++ - "(inlining-limit 450)\n" ++ - "(standard-bindings)\n" ++ - "(extended-bindings)\n" ++ - "(not safe)\n" ++ - "(optimize-dead-definitions))\n" +schHeader = """ + ;; \{ generatedString "Gambit" } + (declare (block) + (inlining-limit 450) + (standard-bindings) + (extended-bindings) + (not safe) + (optimize-dead-definitions)) + + """ showGambitChar : Char -> String -> String showGambitChar '\\' = ("\\\\" ++) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index fdb49288b..3f6fe798c 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -42,24 +42,29 @@ findRacoExe = pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe" schHeader : Bool -> String -> String -schHeader prof libs - = "#lang racket/base\n" ++ - "; " ++ (generatedString "Racket") ++ "\n" ++ - "(require racket/async-channel)\n" ++ -- for asynchronous channels - "(require racket/future)\n" ++ -- for parallelism/concurrency - "(require racket/math)\n" ++ -- for math ops - "(require racket/system)\n" ++ -- for system - "(require rnrs/bytevectors-6)\n" ++ -- for buffers - "(require rnrs/io/ports-6)\n" ++ -- for files - "(require srfi/19)\n" ++ -- for file handling and data - "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C - (if prof then "(require profile)\n" else "") ++ - "(require racket/flonum)\n" ++ -- for float-typed transcendental functions - libs ++ - "(let ()\n" +schHeader prof libs = """ + #lang racket/base + ;; \{ generatedString "Racket" } + (require racket/async-channel) ; for asynchronous channels + (require racket/future) ; for parallelism/concurrency + (require racket/math) ; for math ops + (require racket/system) ; for system + (require rnrs/bytevectors-6) ; for buffers + (require rnrs/io/ports-6) ; for files + (require srfi/19) ; for file handling and data + (require ffi/unsafe ffi/unsafe/define) ; for calling C + \{ ifThenElse prof "(require profile)" "" } + (require racket/flonum) ; for float-typed transcendental functions + \{ libs } + (let () + + """ schFooter : String -schFooter = ") (collect-garbage)" +schFooter = """ + ) + (collect-garbage) + """ showRacketChar : Char -> String -> String showRacketChar '\\' = ("\\\\" ++) @@ -330,42 +335,48 @@ getFgnCall : {auto f : Ref Done (List String) } -> getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d startRacket : String -> String -> String -> String -startRacket racket appdir target = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Racket") - , "" - , "set -e # exit on any error" - , "" - , "if [ \"$(uname)\" = Darwin ]; then" - , " DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")" - , "else" - , " DIR=$(dirname \"$(readlink -f -- \"$0\")\")" - , "fi" - , "" - , "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$LD_LIBRARY_PATH\"" - , "export DYLD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$DYLD_LIBRARY_PATH\"" - , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\"" - ] +startRacket racket appdir target = """ + #!/bin/sh + # \{ generatedString "Racket" } + + set -e # exit on any error + + if [ "$(uname)" = Darwin ]; then + DIR=$(zsh -c 'printf %s "$0:A:h"' "$0") + else + DIR=$(dirname "$(readlink -f -- "$0")") + fi + + export LD_LIBRARY_PATH="$DIR/\{ appdir }:$LD_LIBRARY_PATH" + export DYLD_LIBRARY_PATH="$DIR/\{ appdir }:$DYLD_LIBRARY_PATH" + + \{ racket } "$DIR/\{ target }" "$@" + """ startRacketCmd : String -> String -> String -> String -startRacketCmd racket appdir target = unlines - [ "@echo off" - , "set APPDIR=%~dp0" - , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%" - , racket ++ "\"%APPDIR%" ++ target ++ "\" %*" - ] +startRacketCmd racket appdir target = """ + @echo off + + rem \{ generatedString "Racket" } + + set APPDIR=%~dp0 + set PATH=%APPDIR%\{ appdir };%PATH% + + \{ racket } "%APPDIR%\{ target }" %* + """ startRacketWinSh : String -> String -> String -> String -startRacketWinSh racket appdir target = unlines - [ "#!/bin/sh" - , "# " ++ (generatedString "Racket") - , "" - , "set -e # exit on any error" - , "" - , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")" - , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\"" - , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\"" - ] +startRacketWinSh racket appdir target = """ + #!/bin/sh + # \{ generatedString "Racket" } + + set -e # exit on any error + + DIR=$(dirname "$(readlink -f -- "$0" || cygpath -a -- "$0")") + PATH="$DIR/\{ appdir }:$PATH" + + \{ racket } "$DIR/\{ target }" "$@" + """ compileToRKT : Ref Ctxt Defs -> String -> ClosedTerm -> (outfile : String) -> Core () diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 63e7073d7..882e3799e 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -141,18 +141,19 @@ record Metadata where covering Show Metadata where show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap - fname semanticHighlighting semanticAliases semanticDefaults) - = "Metadata:\n" ++ - " lhsApps: " ++ show apps ++ "\n" ++ - " names: " ++ show names ++ "\n" ++ - " type declarations: " ++ show tydecls ++ "\n" ++ - " current LHS: " ++ show currentLHS ++ "\n" ++ - " holes: " ++ show holeLHS ++ "\n" ++ - " nameLocMap: " ++ show nameLocMap ++ "\n" ++ - " sourceIdent: " ++ show fname ++ - " semanticHighlighting: " ++ show semanticHighlighting ++ - " semanticAliases: " ++ show semanticAliases ++ - " semanticDefaults: " ++ show semanticDefaults + fname semanticHighlighting semanticAliases semanticDefaults) = """ + Metadata: + lhsApps: \{ show apps } + names: \{ show names } + type declarations: \{ show tydecls } + current LHS: \{ show currentLHS } + holes: \{ show holeLHS } + nameLocMap: \{ show nameLocMap } + sourceIdent: \{ show fname } + semanticHighlighting: \{ show semanticHighlighting } + semanticAliases: \{ show semanticAliases } + semanticDefaults: \{ show semanticDefaults } + """ export initMetadata : OriginDesc -> Metadata diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 44a24beb9..046015879 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -40,17 +40,18 @@ outputDirWithDefault d = fromMaybe (build_dir d "exec") (output_dir d) public export toString : Dirs -> String -toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = - unlines [ "+ Working Directory :: " ++ show wdir - , "+ Source Directory :: " ++ show sdir - , "+ Build Directory :: " ++ show bdir - , "+ Local Depend Directory :: " ++ show ldir - , "+ Output Directory :: " ++ show (outputDirWithDefault d) - , "+ Installation Prefix :: " ++ show dfix - , "+ Extra Directories :: " ++ show edirs - , "+ Package Directories :: " ++ show pdirs - , "+ CG Library Directories :: " ++ show ldirs - , "+ Data Directories :: " ++ show ddirs] +toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) = """ + + Working Directory :: \{ show wdir } + + Source Directory :: \{ show sdir } + + Build Directory :: \{ show bdir } + + Local Depend Directory :: \{ show ldir } + + Output Directory :: \{ show $ outputDirWithDefault d } + + Installation Prefix :: \{ show dfix } + + Extra Directories :: \{ show edirs } + + Package Directories :: \{ show pdirs } + + CG Library Directories :: \{ show ldirs } + + Data Directories :: \{ show ddirs } + """ public export data CG = Chez diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 20f98719b..5edb0ae7a 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -402,13 +402,15 @@ versionMsg = "Idris 2, version " ++ show version export usage : String -usage = versionMsg ++ "\n" ++ - "Usage: idris2 [options] [input file]\n\n" ++ - "Available options:\n" ++ - optsUsage ++ - "\n" ++ - "Environment variables:\n" ++ - envsUsage +usage = """ + \{ versionMsg } + Usage: idris2 [options] [input file] + + Available options: + \{ optsUsage } + Environment variables: + \{ envsUsage } + """ checkNat : Integer -> Maybe Nat checkNat n = toMaybe (n >= 0) (integerToNat n) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 7b525ca7f..14b26b425 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -132,13 +132,15 @@ tryTTM (c :: cs) = tryTTM cs banner : String -banner = " ____ __ _ ___ \n" ++ - " / _/___/ /____(_)____ |__ \\ \n" ++ - " / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++ - " _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++ - " /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++ - "\n" ++ - "Welcome to Idris 2. Enjoy yourself!" +banner = #""" + ____ __ _ ___ + / _/___/ /____(_)____ |__ \ + / // __ / ___/ / ___/ __/ / Version \#{ showVersion True version } + _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org + /___/\__,_/_/ /_/____/ /____/ Type :? for help + + Welcome to Idris 2. Enjoy yourself! + """# checkVerbose : List CLOpt -> Bool checkVerbose [] = False diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 4a78301d5..6e99ea526 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -248,16 +248,15 @@ opts x _ = pure $ if (x `elem` optionFlags) -- bash autocompletion script using the given function name completionScript : (fun : String) -> String -completionScript fun = - let fun' = "_" ++ fun - in unlines [ fun' ++ "()" - , "{" - , " ED=$([ -z $2 ] && echo \"--\" || echo $2)" - , " COMPREPLY=($(idris2 --bash-completion $ED $3))" - , "}" - , "" - , "complete -F " ++ fun' ++ " -o default idris2" - ] +completionScript fun = let fun' = "_" ++ fun in """ + \{ fun' }() + { + ED=$([ -z $2 ] && echo "--" || echo $2) + COMPREPLY=($(idris2 --bash-completion $ED $3)) + } + + complete -F \{ fun' } -o default idris2 + """ -------------------------------------------------------------------------------- -- Processing Options