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 92301dc30..c97c6d1cd 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 59efc2d82..4b043661e 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 d1d6de9ae..d1d6de9ae 100644
--- a/stm/texmacspp.ml
+++ b/ide/texmacspp.ml
diff --git a/stm/texmacspp.mli b/ide/texmacspp.mli
index 858847fb6..858847fb6 100644
--- a/stm/texmacspp.mli
+++ b/ide/texmacspp.mli
diff --git a/stm/stm.ml b/stm/stm.ml
index 28e749d5c..e2acb1029 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 6519a6254..6ffe0beb4 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 92b3a869a..bd792b01f 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
 Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
-Texmacspp
 Stm
 Vio_checking