@@ -100,7 +100,7 @@ the program is compiled to the executable \texttt{hello}.
100100
101101\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102102Idris version \version{}
103−-------------------
103+--------------------
104104
105105 Command Arguments Purpose
106106
@@ -111,19 +111,26 @@ Idris version \version{}
111111 :total <name> Check the totality of a name
112112 :r :reload Reload current file
113113 :l :load <filename> Load a new file
114+ :cd <filename> Change working directory
114115 :m :module <module> Import an extra module
115116 :e :edit Edit current file using $EDITOR or $VISUAL
116− :m :metavars Show remaining proof obligations (metavariables)
117− :p :prove <name> Prove a metavariable
117+ :m :metavars <metavar> Show remaining proof obligations (metavariables)
118+ :p :prove <metavar> Prove a metavariable
118119 :a :addproof <name> Add proof to source file
119120 :rmproof <name> Remove proof from proof stack
120121 :showproof <name> Show proof
121122 :proofs Show available proofs
123+ :x <expr> Execute IO actions resulting from an expression
124+ using the interpreter
122125 :c :compile <filename> Compile to an executable <filename>
126+ :js :javascript <filename> Compile to JavaScript <filename>
123127 :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
124130 :? :h :help Display this help text
125131 :set <option> Set an option (errorcontext, showimplicits)
126132 :unset <option> Unset an option
133+ :colour :color <option> Turn REPL colours on or off; set a specific colour
127134 :q :quit Exit the Idris system
128135\end{SaveVerbatim}
129136\codefigs{cmds}{Interactive environment commands}