663c401 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−1

compare with master

unifiedsplit

@@ -816,7 +816,9 @@ targetCPU = do i <- getIState

816

817verbose :: Idris Bool

818verbose = do i <- getIState

819+ -- Quietness overrides verbosity

820+ return (not (opt_quiet (idris_options i)) &&

819− return (opt_verbose (idris_options i))

821+ opt_verbose (idris_options i))

820

822

821setVerbose :: Bool -> Idris ()

823setVerbose :: Bool -> Idris ()

822setVerbose t = do i <- getIState

824setVerbose t = do i <- getIState

test/delab001/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./delab001.idr

2foo : Nat -> String

1foo : Nat -> String

3foo n = case n of

2foo n = case n of

4 0 => "z"

3 0 => "z"

test/docs001/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./docs001.idr

2Type class C

1Type class C

3 class

2 class

4

3

test/docs002/expected+3−5

@@ -1,11 +1,9 @@

1−Type checking ./docs002.idr

2−*docs002> T1 : Type

1+T1 : Type

3 Some documentation

2 Some documentation

4

3

5−*docs002> T2 : Type

4+T2 : Type

6 Some other documentation

5 Some other documentation

7

6

8−*docs002> T3 : Int

7+T3 : Int

9 Some provided postulate

8 Some provided postulate

10

9

11−*docs002> Bye bye

test/docs002/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --consolewidth 80 --nobanner --nocolor docs002.idr < input

2+idris --consolewidth 80 --nobanner --nocolor --quiet docs002.idr < input

3rm *.ibc

test/docs003/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./docs003.idr

2Type class Functor

1Type class Functor

3 Functors

2 Functors

4

3

test/ffi001/expected−1

@@ -1,2 +1 @@

1−Type checking ./test022.idr

20.9995736030415051

10.9995736030415051

test/ffi003/expected−1

@@ -1,2 +1 @@

1−Type checking ./test024.idr

2testtest

1testtest

test/idrisdoc001/expected−2

@@ -1,5 +1,3 @@

1−Type checking ./TestEmpty.idr

2−Type checking ./TestPrivate.idr

3Warning: Ignoring empty or non-existing namespace 'TestEmpty'

1Warning: Ignoring empty or non-existing namespace 'TestEmpty'

4Warning: Ignoring empty or non-existing namespace 'TestPrivate'

2Warning: Ignoring empty or non-existing namespace 'TestPrivate'

5No namespaces to generate documentation for

3No namespaces to generate documentation for

test/idrisdoc001/run+1−1

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

2# Tests that no documentation is built for empty and/or private-only namespaces

3idris --mkdoc test_empty.ipkg

4−rm -rf *.ibc *_doc

4+rm -rf *.ibc *_doc

test/idrisdoc001/test_empty.ipkg+2

@@ -1,4 +1,6 @@

1package test_empty

2

3+opts = "--quiet"

4+

3modules = TestEmpty, TestPrivate

5modules = TestEmpty, TestPrivate

4

6

test/idrisdoc002/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestFunctions.idr

2Functions are documented

1Functions are documented

test/idrisdoc002/test_functions.ipkg+2

@@ -1,4 +1,6 @@

1package test_functions

2

3+opts = "--quiet"

4+

3modules = TestFunctions

5modules = TestFunctions

4

6

test/idrisdoc003/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestDatatypes.idr

2Data types are documented

1Data types are documented

test/idrisdoc003/test_datatypes.ipkg+2

@@ -1,4 +1,6 @@

1package test_datatypes

2

3+opts = "--quiet"

4+

3modules = TestDatatypes

5modules = TestDatatypes

4

6

test/idrisdoc004/expected−1

@@ -1,2 +1 @@

1−Type checking ./TestTypeclasses.idr

2Typeclasses are documented

1Typeclasses are documented

test/idrisdoc004/test_typeclasses.ipkg+2

@@ -1,4 +1,6 @@

1package test_typeclasses

2

3+opts = "--quiet"

4+

3modules = TestTypeclasses

5modules = TestTypeclasses

4

6

test/idrisdoc005/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./TestTracing.idr

2TestTracing: Check

1TestTracing: Check

3Prelude.Bool: Check

2Prelude.Bool: Check

test/idrisdoc005/test_tracing.ipkg+2

@@ -1,4 +1,6 @@

1package test_tracing

2

3+opts = "--quiet"

4+

3modules = TestTracing

5modules = TestTracing

4

6

test/idrisdoc006/expected−2

@@ -1,6 +1,4 @@

1−Type checking ./A/fully/Qualified/NAME.idr

2IdrisDoc file written

1IdrisDoc file written

3−Type checking ./B.idr

4A.fully.Qualified.NAME.html

2A.fully.Qualified.NAME.html

5B.html

3B.html

6A.fully.Qualified.NAME is in the index

4A.fully.Qualified.NAME is in the index

test/idrisdoc006/package_a.ipkg+2

@@ -1,4 +1,6 @@

1package test_merge

2

3+opts = "--quiet"

4+

3modules = A.fully.Qualified.NAME

5modules = A.fully.Qualified.NAME

4

6

test/idrisdoc006/package_b.ipkg+2

@@ -1,4 +1,6 @@

1package test_merge

2

3+opts = "--quiet"

4+

3modules = B

5modules = B

4

6

test/idrisdoc007/package.ipkg+2

@@ -1,4 +1,6 @@

1package do_not_delete

2

3+opts = "--quiet"

4+

3modules = A

5modules = A

4

6

test/idrisdoc008/expected−2

@@ -1,4 +1,2 @@

1−Type checking ./Abstract.idr

2−Type checking ./Visible.idr

3Abstract members are documented

1Abstract members are documented

4Public members are documented

2Public members are documented

test/idrisdoc008/visibility.ipkg+2

@@ -1,4 +1,6 @@

1package visibility

2

3+opts = "--quiet"

4+

3modules = Abstract, Visible

5modules = Abstract, Visible

4

6

test/idrisdoc009/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./Test.idr

2Data type Test : Type

1Data type Test : Type

3 Docs for datatype Test.

2 Docs for datatype Test.

4

3

test/interactive001/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./test032.idr

2isElem x [] = ?isElem_rhs_1

1isElem x [] = ?isElem_rhs_1

3isElem x (y :: xs) = ?isElem_rhs_3

2isElem x (y :: xs) = ?isElem_rhs_3

4

3

test/interactive002/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./interactive002.idr

2Nat

1Nat

3Nat

2Nat

4Nat

3Nat

test/interactive003/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./interactive003.idr

2ys

1ys

3x :: app xs ys

2x :: app xs ys

4[]

3[]

test/interactive004/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./interactive004.idr

2plus ?foo_rhs2 ?foo_rhs3

1plus ?foo_rhs2 ?foo_rhs3

3append k m ?append_rhs2 ?append_rhs3

2append k m ?append_rhs2 ?append_rhs3

test/interactive005/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./interactive005.idr

23 : Nat

13 : Nat

3Hello, World

2Hello, World

4main : IO ()

3main : IO ()

test/interactive006/expected−1

@@ -1,2 +1 @@

1−Type checking ./interactive006.idr

2plus ?foo_rhs2 ?foo_rhs3

1plus ?foo_rhs2 ?foo_rhs3

test/proof009/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./proof009.idr

2

1

3

2

4---------- Goal: ----------

3---------- Goal: ----------

test/reg039/expected−1

@@ -1,2 +1 @@

1−Type checking ./reg039.idr

2[3, 2, 1]

1[3, 2, 1]

test/reg041/expected−1

@@ -1,3 +1,2 @@

1−Type checking ./ott.idr

2?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

1?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

3Z

2Z

test/totality007/expected−1

@@ -1,4 +1,3 @@

1−Type checking ./Totality.idr

2Totality.idr:4:1:

1Totality.idr:4:1:

3Totality.foo is not total as there are missing cases

2Totality.foo is not total as there are missing cases

4Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

3Totality.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

2

3-- totality007

4-- Test that the package builder doesn't allow totality errors in a build

5−opts = "--consolewidth 80"

5+opts = "--quiet --consolewidth 80"

6sourcedir = src

7modules = Totality