From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- ide/ide_slave.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide/ide_slave.ml') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bf86db08f..7f30a4acc 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -390,8 +390,8 @@ 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 + | Some (loc, expr) -> begin + try Texmacspp.tmpp ~loc expr with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) end | None -> Xml_datatype.PCData "ERROR" -- cgit v1.2.3