@@ -100,7 +100,7 @@ the program is compiled to the executable \texttt{hello}.
101\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
101\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102Idris version \version{}
102Idris version \version{}
103−-------------------
103+--------------------
105 Command Arguments Purpose
105 Command Arguments Purpose
@@ -111,19 +111,26 @@ Idris version \version{}
111 :total <name> Check the totality of a name
111 :total <name> Check the totality of a name
112 :r :reload Reload current file
112 :r :reload Reload current file
113 :l :load <filename> Load a new file
113 :l :load <filename> Load a new file
114+ :cd <filename> Change working directory
114 :m :module <module> Import an extra module
115 :m :module <module> Import an extra module
115 :e :edit Edit current file using $EDITOR or $VISUAL
116 :e :edit Edit current file using $EDITOR or $VISUAL
116− :m :metavars Show remaining proof obligations (metavariables)
117+ :m :metavars <metavar> Show remaining proof obligations (metavariables)
117− :p :prove <name> Prove a metavariable
118+ :p :prove <metavar> Prove a metavariable
118 :a :addproof <name> Add proof to source file
119 :a :addproof <name> Add proof to source file
119 :rmproof <name> Remove proof from proof stack
120 :rmproof <name> Remove proof from proof stack
120 :showproof <name> Show proof
121 :showproof <name> Show proof
121 :proofs Show available proofs
122 :proofs Show available proofs
123+ :x <expr> Execute IO actions resulting from an expression
124+ using the interpreter
122 :c :compile <filename> Compile to an executable <filename>
125 :c :compile <filename> Compile to an executable <filename>
126+ :js :javascript <filename> Compile to JavaScript <filename>
123 :exec :execute Compile to an executable and run
127 :exec :execute Compile to an executable and run
128+ :dynamic <filename> Dynamically load a C library (similar to %dynamic)
129+ :dynamic List dynamically loaded C libraries
124 :? :h :help Display this help text
130 :? :h :help Display this help text
125 :set <option> Set an option (errorcontext, showimplicits)
131 :set <option> Set an option (errorcontext, showimplicits)
126 :unset <option> Unset an option
132 :unset <option> Unset an option
133+ :colour :color <option> Turn REPL colours on or off; set a specific colour
127 :q :quit Exit the Idris system
134 :q :quit Exit the Idris system
128\end{SaveVerbatim}
135\end{SaveVerbatim}
129\codefigs{cmds}{Interactive environment commands}
136\codefigs{cmds}{Interactive environment commands}