diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 75 |
1 files changed, 22 insertions, 53 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0dfa03cca..4b95e983d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,6 +8,7 @@ (************************************************************************) open Vernacexpr +open Vernacprop open CErrors open Util open Pp @@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with | VernacUnsetOption o -> coqide_known_option o | _ -> false -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks (loc,ast) = @@ -86,16 +68,19 @@ let ide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning (strbrk "Set this option from the IDE menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning (strbrk "Use IDE navigation instead"); + Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); + if is_navigation_vernac ast || is_undo ast then + Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then - Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts") + Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence sid pa in + ide_cmd_checks loc_ast; + let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -122,12 +107,14 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = Stm.query ~at:id s; "" +let query (s,id) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Stm.query ~at:id pa; "" let annotate phrase = let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Vernac.parse_sentence (pa,None) + Stm.parse_sentence (Stm.get_current_state ()) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -370,43 +357,28 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized") else begin + let init_sid = Stm.get_current_state () in initialized := true; match file with - | None -> Stm.get_current_state () + | 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 - Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in + 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 if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; Stm.finish (); initial_id end -(* Retrocompatibility stuff *) +(* Retrocompatibility stuff, disabled since 8.7 *) let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - Stm.get_current_state (), CSig.Inl "" + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer @@ -494,9 +466,6 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; while not !quit do try let xml_query = Xml_parser.parse xml_ic in |