diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 81 |
1 files changed, 46 insertions, 35 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 67391f5567..fe86df0847 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,5 +1,4 @@ (************************************************************************) - (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) @@ -14,7 +13,6 @@ open Util open Pp open Printer -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration @@ -56,7 +54,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Universes"]; ["Printing";"Unfocused"]] -let is_known_option cmd = match cmd with +let is_known_option cmd = match Vernacprop.under_control cmd with | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> coqide_known_option o | _ -> false @@ -71,16 +69,20 @@ let ide_cmd_checks ~id (loc,ast) = if is_known_option ast then warn "Set this option from the IDE menu instead"; if is_navigation_vernac ast || is_undo ast then - warn "Use IDE navigation instead"; - if is_query ast then - warn "Query commands should not be inserted in scripts" + warn "Use IDE navigation instead" (** Interpretation (cf. [Ide_intf.interp]) *) +let ide_doc = ref None +let get_doc () = Option.get !ide_doc +let set_doc doc = ide_doc := Some doc + let add ((s,eid),(sid,verbose)) = + let doc = get_doc () in let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let loc_ast = Stm.parse_sentence sid pa in - let newid, rc = Stm.add ~ontop:sid verbose loc_ast in + let loc_ast = Stm.parse_sentence ~doc sid pa in + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in + set_doc doc; let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in ide_cmd_checks ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol @@ -95,9 +97,10 @@ let add ((s,eid),(sid,verbose)) = newid, (rc, "") let edit_at id = - match Stm.edit_at id with - | `NewTip -> CSig.Inl () - | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) + let doc = get_doc () in + match Stm.edit_at ~doc id with + | doc, `NewTip -> set_doc doc; CSig.Inl () + | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -110,12 +113,14 @@ let edit_at id = *) let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id ~route pa + let doc = get_doc () in + Stm.query ~at:id ~doc ~route pa let annotate phrase = + let doc = get_doc () in let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Stm.parse_sentence (Stm.get_current_state ()) pa + Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -197,7 +202,8 @@ let export_pre_goals pgs = } let goals () = - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; try let pfts = Proof_global.give_me_the_proof () in Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) @@ -205,9 +211,10 @@ let goals () = let evars () = try - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -217,7 +224,7 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in match all_goals with | [] -> None | g :: _ -> @@ -231,12 +238,17 @@ let hints () = (** Other API calls *) +let wait () = + let doc = get_doc () in + set_doc (Stm.wait ~doc) + let status force = (** We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) - Stm.finish (); - if force then Stm.join (); + set_doc (Stm.finish ~doc:(get_doc ())); + if force then + set_doc (Stm.join ~doc:(get_doc ())); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -253,7 +265,7 @@ let status force = Interface.status_path = path; Interface.status_proofname = proof; Interface.status_allproofs = allproofs; - Interface.status_proofnum = Stm.current_proof_depth (); + Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } let export_coq_object t = { @@ -357,22 +369,16 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized.") else begin - let init_sid = Stm.get_current_state () in + let init_sid = Stm.get_current_state ~doc:(get_doc ()) in initialized := true; match file with | None -> init_sid | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in - let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then begin - let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in - let loc_ast = Stm.parse_sentence init_sid pa in - Stm.add false ~ontop:init_sid loc_ast - end else init_sid, `NewTip in + let doc, initial_id, _ = + get_doc (), init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; - Stm.finish (); + set_doc (Stm.finish ~doc); initial_id end @@ -414,6 +420,7 @@ let eval_call c = Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; + Interface.wait = interruptible wait; Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; @@ -447,9 +454,13 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop () = +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args ~state = + let open Vernac.State in + set_doc state.doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in @@ -496,10 +507,10 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; - CoqworkmgrApi.(init Flags.High); + CoqworkmgrApi.(init High); args) let () = Coqtop.toploop_run := loop |