CoqIDE: new message to print AST

4 files changed, 25 insertions, 1 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 61c60c02f..e99956738 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
 
diff --git a/ide/interface.mli b/ide/interface.mli
index 4dca41a88..43f728a1d 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -209,6 +209,8 @@ type interp_rty = state_id * (string,string) Util.union
 type stop_worker_sty = string
 type stop_worker_rty = unit
 
+type print_ast_sty = state_id
+type print_ast_rty = Xml_datatype.xml
 
 type handler = {
   add         : add_sty         -> add_rty;
@@ -224,6 +226,7 @@ type handler = {
   mkcases     : mkcases_sty     -> mkcases_rty;
   about       : about_sty       -> about_rty;
   stop_worker : stop_worker_sty -> stop_worker_rty;
+  print_ast   : print_ast_sty   -> print_ast_rty;
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 3c312d374..cd20d7a5c 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -187,6 +187,7 @@ module ReifType : sig
   val string_t       : string val_t
   val int_t          : int val_t
   val bool_t         : bool val_t
+  val xml_t          : Xml_datatype.xml val_t
   
   val option_t       : 'a val_t -> 'a option val_t
   val list_t         : 'a val_t -> 'a list val_t
@@ -217,7 +218,7 @@ module ReifType : sig
 end = struct
 
   type value_type =
-    | Unit | String | Int | Bool
+    | Unit | String | Int | Bool | Xml
 
     | Option of value_type
     | List of value_type
@@ -237,6 +238,7 @@ end = struct
   let string_t       = String
   let int_t          = Int
   let bool_t         = Bool
+  let xml_t          = Xml
 
   let option_t x     = Option x
   let list_t x       = List x
@@ -257,6 +259,7 @@ end = struct
     let rec convert ty : 'a -> xml = match ty with
       | Unit          -> Obj.magic of_unit
       | Bool          -> Obj.magic of_bool
+      | Xml           -> Obj.magic (fun x -> x)
       | String        -> Obj.magic of_string
       | Int           -> Obj.magic of_int
       | State         -> Obj.magic of_status
@@ -279,6 +282,7 @@ end = struct
     let rec convert ty : xml -> 'a = match ty with
       | Unit          -> Obj.magic to_unit
       | Bool          -> Obj.magic to_bool
+      | Xml           -> Obj.magic (fun x -> x)
       | String        -> Obj.magic to_string
       | Int           -> Obj.magic to_int
       | State         -> Obj.magic to_status
@@ -353,6 +357,7 @@ end = struct
   | Unit          -> Obj.magic pr_unit
   | Bool          -> Obj.magic pr_bool
   | String        -> Obj.magic pr_string
+  | Xml           -> Obj.magic Xml_printer.to_string_fmt
   | Int           -> Obj.magic pr_int
   | State         -> Obj.magic pr_status
   | Option_state  -> Obj.magic pr_option_state
@@ -375,6 +380,7 @@ end = struct
   | Unit          -> "unit"
   | Bool          -> "bool"
   | String        -> "string"
+  | Xml           -> "xml"
   | Int           -> "int"
   | State         -> assert(true : status exists); "Interface.status"
   | Option_state  -> assert(true : option_state exists); "Interface.option_state"
@@ -435,6 +441,7 @@ let about_sty_t : about_sty val_t = unit_t
 let init_sty_t : init_sty val_t = option_t string_t
 let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
 let stop_worker_sty_t : stop_worker_sty val_t = string_t
+let print_ast_sty_t : print_ast_sty val_t = state_id_t
 
 let add_rty_t : add_rty val_t =
   pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -457,6 +464,7 @@ let about_rty_t : about_rty val_t = coq_info_t
 let init_rty_t : init_rty val_t = state_id_t
 let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t)
 let stop_worker_rty_t : stop_worker_rty val_t = unit_t
+let print_ast_rty_t : print_ast_rty val_t = xml_t
 
 let ($) x = erase x
 let calls = [|  
@@ -476,6 +484,7 @@ let calls = [|
   "Init",       ($)init_sty_t,        ($)init_rty_t;
   "Interp",     ($)interp_sty_t,      ($)interp_rty_t;
   "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
+  "PrintAst",   ($)print_ast_sty_t,   ($)print_ast_rty_t;
 |]
 
 type 'a call =
@@ -496,6 +505,7 @@ type 'a call =
   | StopWorker of stop_worker_sty
   (* retrocompatibility *)
   | Interp     of interp_sty
+  | PrintAst   of print_ast_sty
 
 let id_of_call = function
   | Add _        -> 0
@@ -514,6 +524,7 @@ let id_of_call = function
   | Init _       -> 13
   | Interp _     -> 14
   | StopWorker _ -> 15
+  | PrintAst _   -> 16
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
@@ -535,6 +546,7 @@ let quit x        : quit_rty call        = Quit x
 let init x        : init_rty call        = Init x
 let interp x      : interp_rty call      = Interp x
 let stop_worker x : stop_worker_rty call = StopWorker x
+let print_ast   x : print_ast_rty call   = PrintAst x
 
 let abstract_eval_call handler (c : 'a call) : 'a value =
   let mkGood x : 'a value = Good (Obj.magic x) in
@@ -556,6 +568,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
     | Init x       -> mkGood (handler.init x)
     | Interp x     -> mkGood (handler.interp x)
     | StopWorker x -> mkGood (handler.stop_worker x)
+    | PrintAst x   -> mkGood (handler.print_ast x)
   with any ->
     Fail (handler.handle_exn any)
 
@@ -577,6 +590,7 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with
   | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
   | Interp _     -> of_value (of_value_type interp_rty_t     ) (Obj.magic v)
   | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v)
+  | PrintAst _   -> of_value (of_value_type print_ast_rty_t  ) (Obj.magic v)
 
 let to_answer (q : 'a call) (x : xml) : 'a value = match q with
   | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
@@ -595,6 +609,7 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with
   | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
   | Interp _     -> Obj.magic (to_value (to_value_type interp_rty_t     ) x)
   | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x)
+  | PrintAst _   -> Obj.magic (to_value (to_value_type print_ast_rty_t  ) x)
 
 let of_call (q : 'a call) : xml =
   let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -615,6 +630,7 @@ let of_call (q : 'a call) : xml =
   | Init x       -> mkCall (of_value_type init_sty_t        x)
   | Interp x     -> mkCall (of_value_type interp_sty_t      x)
   | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
+  | PrintAst x   -> mkCall (of_value_type print_ast_sty_t   x)
 
 let to_call : xml -> unknown call =
   do_match "call" (fun s a ->
@@ -636,6 +652,7 @@ let to_call : xml -> unknown call =
     | "Init"       -> Init       (mkCallArg init_sty_t        a)
     | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
     | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
+    | "PrintAst"   -> PrintAst   (mkCallArg print_ast_sty_t   a)
     | _ -> raise Marshal_error)
 
 (** Debug printing *)
@@ -664,6 +681,7 @@ let pr_full_value call value = match call with
   | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
   | Interp _     -> pr_value_gen (print interp_rty_t     ) (Obj.magic value)
   | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value)
+  | PrintAst _   -> pr_value_gen (print print_ast_rty_t  ) (Obj.magic value)
 let pr_call call = match call with
   | Add x        -> str_of_call call ^ " " ^ print add_sty_t         x
   | Edit_at x    -> str_of_call call ^ " " ^ print edit_at_sty_t     x
@@ -681,6 +699,7 @@ let pr_call call = match call with
   | Init x       -> str_of_call call ^ " " ^ print init_sty_t        x
   | Interp x     -> str_of_call call ^ " " ^ print interp_sty_t      x
   | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
+  | PrintAst x   -> str_of_call call ^ " " ^ print print_ast_sty_t   x
 
 let document to_string_fmt =
   Printf.printf "=== Available calls ===\n\n";
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 42defce85..145c88abb 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -31,6 +31,7 @@ val init        : init_sty        -> init_rty call
 val stop_worker : stop_worker_sty -> stop_worker_rty call
 (* retrocompatibility *)
 val interp      : interp_sty      -> interp_rty call
+val print_ast      : print_ast_sty      -> print_ast_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value