diff options
| -rw-r--r-- | ide/coqidetop.mllib | 1 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 11 | ||||
| -rw-r--r-- | ide/texmacspp.ml (renamed from stm/texmacspp.ml) | 0 | ||||
| -rw-r--r-- | ide/texmacspp.mli (renamed from stm/texmacspp.mli) | 0 | ||||
| -rw-r--r-- | stm/stm.ml | 19 | ||||
| -rw-r--r-- | stm/stm.mli | 4 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 |
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 |