aboutsummaryrefslogtreecommitdiff
path: root/ide/ide_slave.ml
diff options
context:
space:
mode:
authorEnrico Tassi2014-09-24 17:25:27 +0200
committerEnrico Tassi2014-09-29 21:54:31 +0200
commitec49447d078da25959d617ae23e55a668fdd1646 (patch)
treefa36169808ba6bcd886f9fa6e333a569e218717c /ide/ide_slave.ml
parent7eeda1b1ffd93311965aa431ea64f0fb38e3b34d (diff)
CoqIDE: new message to print AST
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r--ide/ide_slave.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 61c60c02f2..e99956738a 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -375,6 +375,7 @@ let eval_call xml_oc log c =
Interface.interp = interruptible interp;
Interface.handle_exn = handle_exn;
Interface.stop_worker = Stm.stop_worker;
+ Interface.print_ast = Stm.print_ast;
} in
Xmlprotocol.abstract_eval_call handler c