diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 16 | ||||
| -rw-r--r-- | toplevel/ide_blob.ml | 25 | ||||
| -rw-r--r-- | toplevel/ide_blob.mli | 3 |
3 files changed, 37 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 74c4ff3db8..440d362807 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -150,6 +150,7 @@ let usage () = let warning s = msg_warning (str s) +let ide_slave = ref false let ide_args = ref [] let parse_args arglist = @@ -287,6 +288,8 @@ let parse_args arglist = | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem + | "-ideslave" :: rem -> ide_slave := true; parse rem + | s :: rem -> ide_args := s :: !ide_args; parse rem @@ -308,6 +311,12 @@ let init arglist = begin try parse_args arglist; + if !ide_args <> [] then usage (); + if !ide_slave then begin + Flags.make_silent true; + Pfedit.set_undo (Some 5000); + Ide_blob.init_stdout () + end; if_verbose print_header (); init_load_path (); inputstate (); @@ -342,13 +351,14 @@ let init_ide arglist = Flags.make_silent true; Pfedit.set_undo (Some 5000); Ide_blob.init_stdout (); - init arglist; List.rev !ide_args let start () = init_toplevel (List.tl (Array.to_list Sys.argv)); - if !ide_args <> [] then usage (); - Toplevel.loop(); + if !ide_slave then + Ide_blob.loop () + else + Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index a312b0037b..899cee1e46 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -403,7 +403,9 @@ let concl_next_tac sigma concl = ]) let current_goals () = - let pfts = Pfedit.get_pftreestate () in + let pfts = + Proof_global.give_me_the_proof () + in let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in if all_goals = [] then begin @@ -524,12 +526,14 @@ type 'a call = type 'a value = | Good of 'a - | Fail of exn + | Fail of (Util.loc * Pp.std_ppcmds) let eval_call c = + let null_formatter = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in let filter_compat_exn = function | Vernac.DuringCommandInterp (loc,inner) | Vernacexpr.DuringSyntaxChecking (loc,inner) -> inner + | Vernacexpr.Quit -> raise Vernacexpr.Quit | e -> e in try Good (match c with @@ -541,7 +545,11 @@ let eval_call c = | Cur_goals -> Obj.magic (current_goals ()) | Cur_status -> Obj.magic (current_status ()) | Cases s -> Obj.magic (make_cases s)) - with e -> Fail (filter_compat_exn e) + with e -> + let (l,pp) = explain_exn (filter_compat_exn e) in + (* force evaluation of format stream *) + Pp.msg_with null_formatter pp; + Fail (l,pp) let is_in_loadpath s : bool call = In_loadpath s @@ -568,3 +576,14 @@ let make_cases s : string list list call = Cases s (* End of wrappers *) + +let loop () = + try + while true do + let q = (Safe_marshal.receive: in_channel -> 'a call) stdin in + let r = eval_call q in + Safe_marshal.send stdout r + done + with + | Vernacexpr.Quit -> exit 0 + | _ -> exit 1 diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index c74d67f2ce..561821b563 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -23,7 +23,7 @@ type 'a call type 'a value = | Good of 'a - | Fail of exn + | Fail of (Util.loc * Pp.std_ppcmds) val eval_call : 'a call -> 'a value @@ -43,3 +43,4 @@ val current_goals : goals call val read_stdout : string call +val loop : unit -> unit |