git.iko.soy/Idris-dev
on master help sign in
Move IDE protocol docs
27ccd9aDavid Raymond Christiansen
docs/index.rst+1−8
compare with master
unifiedsplit
@@ -104,6 +104,7 @@ Language Reference
104 reference/uniqueness-types
104 reference/uniqueness-types
105 reference/ffi
105 reference/ffi
106 reference/erasure
106 reference/erasure
107+ reference/ide-protocol
107
108
108.. _guides:
109.. _guides:
109
110
@@ -116,11 +117,3 @@ Short Guides
116
117
117 guides/type-providers-ffi
118 guides/type-providers-ffi
118
119
119−############################
120−Implementation Documentation
121−############################
122−
123−.. toctree::
124− :maxdepth: 1
125−
126− ide/protocol
docs/ide/protocol.rst → docs/reference/ide-protocol.rstrenamed+1−1
@@ -1,5 +1,5 @@
1********************
1********************
2−Idris's IDE Protocol
2+The IDE Protocol
3********************
3********************
4
4
5The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.
5The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.