From 6a412da0f2681ede8f2753666bb9098e7ac8bfd2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 May 2017 02:55:28 +0200
Subject: [ide] Disable `print_ast` call.

So far this part of the system has shown little utility other than
having developers put time to fix it every time they change something
in the system.

I have never seen this functionality used in the wild, and a large
part of the vernac was marked TODO. Given that we have automatic
methods to provide this functionality these days (PPX), we remove
Texmacspp.
---
 ide/ide_slave.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 56ada9d132..dbca959eae 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -388,14 +388,8 @@ let interp ((_raw, verbose), s) =
 
 let quit = ref false
 
-(** Serializes the output of Stm.get_ast  *)
-let print_ast id =
-  match Stm.get_ast id with
-  | Some (expr, loc) -> begin
-      try  Texmacspp.tmpp expr loc
-      with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
-    end
-  | None     -> Xml_datatype.PCData "ERROR"
+(** Disabled *)
+let print_ast id = Xml_datatype.PCData "ERROR"
 
 (** Grouping all call handlers together + error handling *)
 
-- 
cgit v1.2.3