Move serialization functions out of Stm

Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.

This should be quite safe to pull in. Test suite passes.

Related to #180

7 files changed, 21 insertions, 15 deletions

diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index 92301dc30e..c97c6d1cd7 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -1,2 +1,3 @@
 Xmlprotocol
+Texmacspp
 Ide_slave
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 59efc2d821..4b043661e0 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -393,6 +393,15 @@ 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"
+
 (** Grouping all call handlers together + error handling *)
 
 let eval_call xml_oc log c =
@@ -423,7 +432,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;
+    Interface.print_ast = print_ast;
     Interface.annotate = interruptible annotate;
   } in
   Xmlprotocol.abstract_eval_call handler c
diff --git a/stm/texmacspp.ml b/ide/texmacspp.ml
index d1d6de9ae8..d1d6de9ae8 100644
--- a/stm/texmacspp.ml
+++ b/ide/texmacspp.ml
diff --git a/stm/texmacspp.mli b/ide/texmacspp.mli
index 858847fb6a..858847fb6a 100644
--- a/stm/texmacspp.mli
+++ b/ide/texmacspp.mli
diff --git a/stm/stm.ml b/stm/stm.ml
index 28e749d5c8..e2acb10293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2314,18 +2314,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
     let e = Errors.push e in
     handle_failure e vcs tty
 
-let print_ast id =
-  try
-    match VCS.visit id with
-    | { step = `Cmd { cast = { loc; expr } } }
-    | { step = `Fork (({ loc; expr }, _, _, _), _) } 
-    | { step = `Qed ({ qast = { loc; expr } }, _) } ->
-        let xml = 
-          try Texmacspp.tmpp expr loc
-          with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
-        xml;
-    | _ -> Xml_datatype.PCData "ERROR"
-  with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+  match VCS.visit id with
+  | { step = `Cmd { cast = { loc; expr } } }
+  | { step = `Fork (({ loc; expr }, _, _, _), _) } 
+  | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+         Some (expr, loc)
+  | _ -> None
 
 let stop_worker n = Slaves.cancel_worker n
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 6519a62541..6ffe0beb44 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -76,7 +76,9 @@ val get_current_state : unit -> Stateid.t
 
 (* Misc *)
 val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a9..bd792b01f6 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
 Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
-Texmacspp
 Stm
 Vio_checking