074e10b · Idris-dev · git.iko.soy

idris.cabal+29

compare with master

unifiedsplit

@@ -319,6 +319,35 @@ Extra-source-files:

319 test/ffi005/run

320 test/ffi005/expected

321

322+ test/idrisdoc001/run

323+ test/idrisdoc001/expected

324+ test/idrisdoc001/*.idr

325+ test/idrisdoc001/*.ipkg

326+ test/idrisdoc002/run

327+ test/idrisdoc002/expected

328+ test/idrisdoc002/*.idr

329+ test/idrisdoc002/*.ipkg

330+ test/idrisdoc003/run

331+ test/idrisdoc003/expected

332+ test/idrisdoc003/*.idr

333+ test/idrisdoc003/*.ipkg

334+ test/idrisdoc004/run

335+ test/idrisdoc004/expected

336+ test/idrisdoc004/*.idr

337+ test/idrisdoc004/*.ipkg

338+ test/idrisdoc005/run

339+ test/idrisdoc005/expected

340+ test/idrisdoc005/*.idr

341+ test/idrisdoc005/*.ipkg

342+ test/idrisdoc006/run

343+ test/idrisdoc006/expected

344+ test/idrisdoc006/*.idr

345+ test/idrisdoc006/*.ipkg

346+ test/idrisdoc007/run

347+ test/idrisdoc007/expected

348+ test/idrisdoc007/*.idr

349+ test/idrisdoc007/*.ipkg

350+

322 test/interactive001/run

351 test/interactive001/run

323 test/interactive001/input

352 test/interactive001/input

324 test/interactive001/*.idr

353 test/interactive001/*.idr

src/Idris/IdrisDoc.hs+1−1

@@ -637,7 +637,7 @@ readDocInfo dir =

637 where reader h = let converter = text2DocInfo . E.decodeUtf8

638 in converter `fmap` BS.hGetContents h

639 onlyValid out ns s = do s' <- s

640− let end = (genRelNsPath ns "html")

640+ let end = "docs" </> (genRelNsPath ns "html")

641 exists <- doesFileExist $ out </> end

642 if exists then return $ S.insert ns s'

643 else s

test/README+1

@@ -5,6 +5,7 @@ dsl: Embedded DSLs and features to support DSL development

5effects: Effects package

6error: Error messages and error reflection

7ffi: FFI calls, including type providers

8+idrisdoc: Documentation tool functionality

8interactive: Interactive editing, proof search

9interactive: Interactive editing, proof search

9io: IO monad

10io: IO monad

10literate: .lidr files; literate programming

11literate: .lidr files; literate programming

test/idrisdoc001/TestEmpty.idrnew file+1

@@ -0,0 +1 @@

1+module TestEmpty

test/idrisdoc001/expectednew file+3

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

1+Type checking ./TestEmpty.idr

2+Warning: Ignoring empty or non-existing namespace 'TestEmpty'

3+No namespaces to generate documentation for

test/idrisdoc001/runnew file+4

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

1+#!/usr/bin/env bash

2+# Tests that no documentation is built for empty namespaces

3+idris --mkdoc test_empty.ipkg

4+rm -rf *.ibc *_doc

test/idrisdoc001/test_empty.ipkgnew file+4

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

1+package test_empty

2+

3+modules = TestEmpty

4+

test/idrisdoc002/TestFunctions.idrnew file+5

@@ -0,0 +1,5 @@

1+module TestFunctions

2+

3+||| Test function

4+test : ()

5+test = ()

test/idrisdoc002/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestFunctions.idr

2+Functions are documented

test/idrisdoc002/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+# Tests that documentation is generated for functions

3+idris --mkdoc test_functions.ipkg

4+[ -d test_functions_doc ] && echo "Functions are documented"

5+rm -rf *.ibc *_doc

test/idrisdoc002/test_functions.ipkgnew file+4

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

1+package test_functions

2+

3+modules = TestFunctions

4+

test/idrisdoc003/TestDatatypes.idrnew file+6

@@ -0,0 +1,6 @@

1+module TestDatatypes

2+

3+||| This is another test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc003/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestDatatypes.idr

2+Data types are documented

test/idrisdoc003/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+# Tests that documentation is generated for data types

3+idris --mkdoc test_datatypes.ipkg

4+[ -d test_datatypes_doc ] && echo "Data types are documented"

5+rm -rf *.ibc *_doc

test/idrisdoc003/test_datatypes.ipkgnew file+4

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

1+package test_datatypes

2+

3+modules = TestDatatypes

4+

test/idrisdoc004/TestTypeclasses.idrnew file+8

@@ -0,0 +1,8 @@

1+module TestTypeclasses

2+

3+||| This is a test

4+|||

5+||| @ a Test arg

6+class Test a where

7+ ||| Test function

8+ test : a -> Int

test/idrisdoc004/expectednew file+2

@@ -0,0 +1,2 @@

1+Type checking ./TestTypeclasses.idr

2+Typeclasses are documented

test/idrisdoc004/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+# Tests that documentation is generated for type classes

3+idris --mkdoc test_typeclasses.ipkg

4+[ -d test_typeclasses_doc ] && echo "Typeclasses are documented"

5+rm -rf *.ibc *_doc

test/idrisdoc004/test_typeclasses.ipkgnew file+4

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

1+package test_typeclasses

2+

3+modules = TestTypeclasses

4+

test/idrisdoc005/TestTracing.idrnew file+4

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

1+module TestTracing

2+

3+test : Bool

4+test = True

test/idrisdoc005/expectednew file+3

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

1+Type checking ./TestTracing.idr

2+TestTracing: Check

3+Prelude.Bool: Check

test/idrisdoc005/runnew file+6

@@ -0,0 +1,6 @@

1+#!/usr/bin/env bash

2+# Tests that references to other namespaces are traced

3+idris --mkdoc test_tracing.ipkg

4+[ -f test_tracing_doc/docs/TestTracing.html ] && echo "TestTracing: Check"

5+[ -f test_tracing_doc/docs/Prelude.Bool.html ] && echo "Prelude.Bool: Check"

6+rm -rf *.ibc *_doc

test/idrisdoc005/test_tracing.ipkgnew file+4

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

1+package test_tracing

2+

3+modules = TestTracing

4+

test/idrisdoc006/A.idrnew file+6

@@ -0,0 +1,6 @@

1+module A

2+

3+||| This is another test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc006/B.idrnew file+5

@@ -0,0 +1,5 @@

1+module B

2+

3+||| Test function

4+test : ()

5+test = ()

test/idrisdoc006/expectednew file+6

@@ -0,0 +1,6 @@

1+Type checking ./A.idr

2+Type checking ./B.idr

3+A: Check

4+B: Check

5+A

6+B

test/idrisdoc006/package_a.ipkgnew file+4

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

1+package test_merge

2+

3+modules = A

4+

test/idrisdoc006/package_b.ipkgnew file+4

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

1+package test_merge

2+

3+modules = B

4+

test/idrisdoc006/runnew file+8

@@ -0,0 +1,8 @@

1+#!/usr/bin/env bash

2+# Tests that documentation properly is merged with existing

3+idris --mkdoc package_a.ipkg

4+idris --mkdoc package_b.ipkg

5+[ -f test_merge_doc/docs/A.html ] && echo "A: Check"

6+[ -f test_merge_doc/docs/B.html ] && echo "B: Check"

7+cat test_merge_doc/IdrisDoc

8+rm -rf *.ibc *_doc

test/idrisdoc007/A.idrnew file+6

@@ -0,0 +1,6 @@

1+module A

2+

3+||| This is a test

4+data Test : Type where

5+ ||| Test constructor

6+ ATest : Test

test/idrisdoc007/expectednew file+1

@@ -0,0 +1 @@

1+Exit status (expects 1): 1

test/idrisdoc007/package.ipkgnew file+4

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

1+package do_not_delete

2+

3+modules = A

4+

test/idrisdoc007/runnew file+6

@@ -0,0 +1,6 @@

1+#!/usr/bin/env bash

2+# Tests that documentation only is written when safe

3+mkdir do_not_delete_doc

4+idris --mkdoc package.ipkg > nowhere

5+echo Exit status $expects 1$: $?

6+rm -rf do_not_delete_doc *.ibc nowhere