Merge pull request #2094 from david-christiansen/no-type-checking-message-quiet
Make --quiet imply non-verbosity
commit663c401154fb4f43f8bdb861abee006299f07f81
authorDavid Christiansen <david@davidchristiansen.dk>
dateWed 1 Apr 2015, 19:02 (12 years ago)
parentcb6f6466c4553c
src/Idris/AbsSyntax.hs+3−1
@@ -816,7 +816,9 @@ targetCPU = do i <- getIState
816816
817817verbose :: Idris Bool
818818verbose = do i <- getIState
819− return (opt_verbose (idris_options i))
819+ -- Quietness overrides verbosity
820+ return (not (opt_quiet (idris_options i)) &&
821+ opt_verbose (idris_options i))
820822
821823setVerbose :: Bool -> Idris ()
822824setVerbose t = do i <- getIState
test/delab001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./delab001.idr
21foo : Nat -> String
32foo n = case n of
43 0 => "z"
test/docs001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./docs001.idr
21Type class C
32 class
43
test/docs002/expected+3−5
@@ -1,11 +1,9 @@
1−Type checking ./docs002.idr
2−*docs002> T1 : Type
1+T1 : Type
32 Some documentation
43
5−*docs002> T2 : Type
4+T2 : Type
65 Some other documentation
76
8−*docs002> T3 : Int
7+T3 : Int
98 Some provided postulate
109
11−*docs002> Bye bye
test/docs002/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris --consolewidth 80 --nobanner --nocolor docs002.idr < input
2+idris --consolewidth 80 --nobanner --nocolor --quiet docs002.idr < input
33rm *.ibc
test/docs003/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./docs003.idr
21Type class Functor
32 Functors
43
test/ffi001/expected−1
@@ -1,2 +1 @@
1−Type checking ./test022.idr
210.9995736030415051
test/ffi003/expected−1
@@ -1,2 +1 @@
1−Type checking ./test024.idr
21testtest
test/idrisdoc001/expected−2
@@ -1,5 +1,3 @@
1−Type checking ./TestEmpty.idr
2−Type checking ./TestPrivate.idr
31Warning: Ignoring empty or non-existing namespace 'TestEmpty'
42Warning: Ignoring empty or non-existing namespace 'TestPrivate'
53No namespaces to generate documentation for
test/idrisdoc001/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
22# Tests that no documentation is built for empty and/or private-only namespaces
33idris --mkdoc test_empty.ipkg
4−rm -rf *.ibc *_doc
4+rm -rf *.ibc *_doc
test/idrisdoc001/test_empty.ipkg+2
@@ -1,4 +1,6 @@
11package test_empty
22
3+opts = "--quiet"
4+
35modules = TestEmpty, TestPrivate
46
test/idrisdoc002/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestFunctions.idr
21Functions are documented
test/idrisdoc002/test_functions.ipkg+2
@@ -1,4 +1,6 @@
11package test_functions
22
3+opts = "--quiet"
4+
35modules = TestFunctions
46
test/idrisdoc003/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestDatatypes.idr
21Data types are documented
test/idrisdoc003/test_datatypes.ipkg+2
@@ -1,4 +1,6 @@
11package test_datatypes
22
3+opts = "--quiet"
4+
35modules = TestDatatypes
46
test/idrisdoc004/expected−1
@@ -1,2 +1 @@
1−Type checking ./TestTypeclasses.idr
21Typeclasses are documented
test/idrisdoc004/test_typeclasses.ipkg+2
@@ -1,4 +1,6 @@
11package test_typeclasses
22
3+opts = "--quiet"
4+
35modules = TestTypeclasses
46
test/idrisdoc005/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./TestTracing.idr
21TestTracing: Check
32Prelude.Bool: Check
test/idrisdoc005/test_tracing.ipkg+2
@@ -1,4 +1,6 @@
11package test_tracing
22
3+opts = "--quiet"
4+
35modules = TestTracing
46
test/idrisdoc006/expected−2
@@ -1,6 +1,4 @@
1−Type checking ./A/fully/Qualified/NAME.idr
21IdrisDoc file written
3−Type checking ./B.idr
42A.fully.Qualified.NAME.html
53B.html
64A.fully.Qualified.NAME is in the index
test/idrisdoc006/package_a.ipkg+2
@@ -1,4 +1,6 @@
11package test_merge
22
3+opts = "--quiet"
4+
35modules = A.fully.Qualified.NAME
46
test/idrisdoc006/package_b.ipkg+2
@@ -1,4 +1,6 @@
11package test_merge
22
3+opts = "--quiet"
4+
35modules = B
46
test/idrisdoc007/package.ipkg+2
@@ -1,4 +1,6 @@
11package do_not_delete
22
3+opts = "--quiet"
4+
35modules = A
46
test/idrisdoc008/expected−2
@@ -1,4 +1,2 @@
1−Type checking ./Abstract.idr
2−Type checking ./Visible.idr
31Abstract members are documented
42Public members are documented
test/idrisdoc008/visibility.ipkg+2
@@ -1,4 +1,6 @@
11package visibility
22
3+opts = "--quiet"
4+
35modules = Abstract, Visible
46
test/idrisdoc009/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./Test.idr
21Data type Test : Type
32 Docs for datatype Test.
43
test/interactive001/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./test032.idr
21isElem x [] = ?isElem_rhs_1
32isElem x (y :: xs) = ?isElem_rhs_3
43
test/interactive002/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive002.idr
21Nat
32Nat
43Nat
test/interactive003/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive003.idr
21ys
32x :: app xs ys
43[]
test/interactive004/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./interactive004.idr
21plus ?foo_rhs2 ?foo_rhs3
32append k m ?append_rhs2 ?append_rhs3
test/interactive005/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./interactive005.idr
213 : Nat
32Hello, World
43main : IO ()
test/interactive006/expected−1
@@ -1,2 +1 @@
1−Type checking ./interactive006.idr
21plus ?foo_rhs2 ?foo_rhs3
test/proof009/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./proof009.idr
21
32
43---------- Goal: ----------
test/reg039/expected−1
@@ -1,2 +1 @@
1−Type checking ./reg039.idr
21[3, 2, 1]
test/reg041/expected−1
@@ -1,3 +1,2 @@
1−Type checking ./ott.idr
21?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)
32Z
test/totality007/expected−1
@@ -1,4 +1,3 @@
1−Type checking ./Totality.idr
21Totality.idr:4:1:
32Totality.foo is not total as there are missing cases
43Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases
test/totality007/totality.ipkg+1−1
@@ -2,6 +2,6 @@ package totality
22
33-- totality007
44-- Test that the package builder doesn't allow totality errors in a build
5−opts = "--consolewidth 80"
5+opts = "--quiet --consolewidth 80"
66sourcedir = src
77modules = Totality