Johann Rudloff
9591b147a4
[ cleanup ] Remove unused helper function
2021-04-29 13:41:34 +02:00
Johann Rudloff
f656b97928
[ refactor ] Move all HTML-related code out of the Idris.Package module
2021-04-29 11:56:47 +02:00
Johann Rudloff
8012736e83
[ fix ] Add new module to the ipkg file
2021-04-29 11:29:37 +02:00
Johann Rudloff
0b9831e3c5
[ refactor ] Move HTML docs specific code into its own module
2021-04-29 10:47:31 +02:00
Johann Rudloff
af26a73504
[ cleanup ] Most reAnnotate calls in Idris.REPL can be skipped
...
Since we have the locally overloaded `prettyTerm`, we can move most
functions in the `REPL` module back to `IdrisAnn`, reducing the overall
size of the PR.
2021-04-29 10:11:58 +02:00
Johann Rudloff
4e937246b7
[ cleanup ] Remove some (now) unused Doc annotations, restore original colors
2021-04-29 10:07:13 +02:00
Johann Rudloff
8550de29bb
Use Data.Strings instead of Data.String for compatibility with previous release
2021-04-28 20:05:51 +02:00
Johann Rudloff
fd0690dc08
Add parentheses around operator names in HTML docs
2021-04-28 18:46:20 +02:00
Johann Rudloff
1ac28921df
Merge remote-tracking branch 'origin/master' into mkdoc-rework
2021-04-28 18:45:24 +02:00
Johann Rudloff
906a353e0a
Finish mkdocs rework
2021-04-28 18:28:23 +02:00
Johann Rudloff
c1dd237679
Introduce IdrisSyntax annotation type
2021-04-28 16:38:45 +02:00
Giuseppe Lomurno
cab4403357
Typo in findInTree
2021-04-28 15:24:11 +01:00
G. Allais
96a2809f62
[ fix #1169 ] primitive types are not NTCon ( #1340 )
2021-04-28 09:33:27 +01:00
Stefan Höck
bbea929cf3
[ refactor ] Cleanup integral primops ( #1211 )
2021-04-28 09:32:46 +01:00
G. Allais
d32daaf36a
[ fix ] properly handle Namespace blocks for DocStrings ( #1342 )
2021-04-28 09:31:01 +01:00
Johann Rudloff
17af0230ef
Update doc generation so it compiles with latest Idris master
2021-04-28 09:38:11 +02:00
Guillaume ALLAIS
4224c58651
[ fix ] print infix operators with parens
...
I noticed that e.g. List's (::) was not printed correctly in `:doc`
so here's a fix.
2021-04-27 14:12:48 +01:00
Jonathan Chan
72e45d959e
[ REPL ] Added commands :ti and :opts ( #1241 )
...
:ti does the same thing as :t, but shows the type as if showimplicits
were set. The value of REPLOpt.ShowImplicits is unchanged.
:opts shows the current values of the options that can be set or unset
with :set/:unset. (This already existed in REPLCmd.GetOpts, idk why it
just wasn't in Parser.parserCommandsForHelp.)
Also fixed the spacing of the help message.
2021-04-27 10:27:50 +01:00
Johann Rudloff
b0ede0f2b1
Get rid of multi-line strings to fix build from previous version
2021-04-26 23:02:28 +02:00
Johann Rudloff
3dd5878e22
[ wip ] Improve HTML docs with better annotations
2021-04-26 23:02:25 +02:00
Johann Rudloff
a012e64ef2
Add Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML to idris2api's modules list
2021-04-26 22:59:23 +02:00
Johann Rudloff
e5a1898692
Fix tests for commit: Transition :doc command to use PrettyPrint instead of plain strings
2021-04-26 22:59:06 +02:00
Johann Rudloff
b978816b53
[lazy rebase] Update makeDocs for new getDocsForName implementation ((Doc IdrisAnn) instead of String)
2021-04-26 22:55:48 +02:00
Johann Rudloff
0b9c435aa7
Begin refactoring: extract HTML generation to separate module
2021-04-26 22:48:24 +02:00
Johann Rudloff
ae9da0e8ce
Reformat docs CSS file to comply with code style guide (and make the linter happy)
2021-04-26 22:48:24 +02:00
Johann Rudloff
e8ca7c85e3
Update to accomodate for latest Idris2 changes
2021-04-26 22:48:24 +02:00
Johann Rudloff
295b7638af
Initial implementation to get links working
...
The process is a bit hacky, but I could not find an easier way.
During desugaring we set the "fullNamespace" option, so that namespaces
are not lost. When the (pretty printed) Doc is rendered to HTML, the
namespaces are used to generate the link destination, but are removed
before generating the "user-visible" string (the text inside the "<a>"
tag).
2021-04-26 22:48:24 +02:00
Johann Rudloff
13cba46188
Show types, show names inside module without namespace
2021-04-26 22:48:21 +02:00
Johann Rudloff
68a5f1f1b7
Copy styles.css from support into generated docs/ folder
2021-04-26 22:45:14 +02:00
Johann Rudloff
1a025131e3
Exact namespace comparison to avoid duplicated entries for re-exported names
2021-04-26 22:44:03 +02:00
Johann Rudloff
1de8b4497c
HTML-Escape full documentation body
2021-04-26 22:44:03 +02:00
Johann Rudloff
3baab8abea
First draft version of --mkdoc CLI switch
2021-04-26 22:44:00 +02:00
Tung Alissa
881a5e7fbc
[ fix #1328 ] print infix functions enclosed in grave accents ( #1331 )
2021-04-25 18:56:08 +01:00
stefan-hoeck
0858c26dcf
[ refactor ] renamed value to runConst
2021-04-25 10:41:36 +01:00
stefan-hoeck
7863636490
[ new ] add Contravariant interface
2021-04-25 10:41:36 +01:00
stefan-hoeck
047fdb50dd
[ new ] missing Identity implementations
2021-04-25 10:41:36 +01:00
stefan-hoeck
cb7add2eca
[ new ] add Const applicative functor
2021-04-25 10:41:36 +01:00
Guardian Spirit
15bd6823d2
Add identity cast ( #1332 )
2021-04-25 09:22:01 +01:00
Ruslan Feizerakhmanov
70158b9dd1
REPL commands: load-package & fuzzy-search ( #1318 )
...
REPL commands: load-package & fuzzy-search
Move REPL-related code over to its own namespace
2021-04-25 09:13:55 +01:00
Johann Rudloff
489b85aae5
PrettyPrint: Fix SimpleDocTree.fromStream dropping parts of documents
...
When flattening the `SimpleDocTree` created from a `SimpleDocStream`, the
first part of a concatenated doc was sometimes dropped, depending on the
result of the recursive call to `flatten`.
2021-04-25 09:10:22 +01:00
André Videla
9f39ad6ba8
Implement new parameters syntax
...
Previously, parameter block reused the same syntax as in Idris1:
```
parameters (v1 : t1, … , vn : tn)
```
Unfortunately this syntax presents some issues:
- It does not allow to declare implicit parameters
- It does not allow to specify which multiplicity to use
- It is inconsistent with the syntax used for named arguments elsewhere
in the language.
This change fixes those three problems by borrowing the syntax for
declaring type parameters in records:
```
parameters (v1 : t2) (v2 : t2) … (vn : tn)
```
It also enables other features like multiple declarations of arguments
with the same type:
```
parameters (v1, v2 : Type)
```
2021-04-23 19:02:48 +01:00
André Videla
908550c05f
merge multiplicity parser
2021-04-23 19:02:48 +01:00
Ohad Kammar
9a445f57e6
[base] Minor: change the order of terms in the IntegerView ( #1327 )
2021-04-23 14:52:44 +01:00
Denis Buzdalov
583442b359
[ contrib ] Arithmetic on Fin ( #830 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-04-23 12:05:13 +01:00
arty
48dc732788
[ base ] Not (a == b) implies not a == b ( #1315 )
2021-04-22 13:16:26 +01:00
Zoe Stafford
c75b3f7f14
Add Agda-like builtins ( #1253 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-04-22 13:08:32 +01:00
stefan-hoeck
181b26b250
[ fix ] broken unicode parsing in JSON
2021-04-22 10:59:14 +01:00
claymager
d6583048d8
Fixes for processPackage ( #1304 )
2021-04-21 10:15:39 +01:00
Tung Alissa
1bf46bc458
[ REPL ] Improving :doc (fixity, totality, colours) ( #1316 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-04-21 09:39:18 +01:00
Robert Wright
8e08e96201
Replace RefC putStrLn usages with log
2021-04-19 16:04:41 +01:00
