From 0692216822e1fd9001f15178c5cb9dd91c9fbc74 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Sep 2011 16:47:16 +0000 Subject: Ide_intf: slight reorganisation of the IDE api - merge raw_interp with interp (with one more flag) - merge read_stdout with interp, which now return a string - shorter command names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/command_windows.ml | 10 +++------- ide/coq.ml | 19 +++++++++---------- ide/coq.mli | 13 ++++++------- ide/coqide.ml | 31 ++++++++++++------------------- 4 files changed, 30 insertions(+), 43 deletions(-) (limited to 'ide') diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 739435df4..0d0894213 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -102,15 +102,11 @@ object(self) in try result#buffer#set_text - (match Coq.raw_interp coqtop phrase with + (match Coq.interp coqtop ~raw:true phrase with | Ide_intf.Fail (l,str) -> ("Error while interpreting "^phrase^":\n"^str) - | Ide_intf.Good () -> - match Coq.read_stdout coqtop with - | Ide_intf.Fail (l,str) -> - ("Error while fetching "^phrase^"results:\n"^str) - | Ide_intf.Good results -> - ("Result for command " ^ phrase ^ ":\n" ^ results)) + | Ide_intf.Good results -> + ("Result for command " ^ phrase ^ ":\n" ^ results)) with e -> let s = Printexc.to_string e in assert (Glib.Utf8.validate s); diff --git a/ide/coq.ml b/ide/coq.ml index dbb0d8ac3..a5b2d38ab 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -199,13 +199,12 @@ let eval_call coqtop (c:'a Ide_intf.call) = flush coqtop.cin; (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout -let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s)) -let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s) -let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout +let interp coqtop ?(raw=false) ?(verbose=true) s = + eval_call coqtop (Ide_intf.interp (raw,verbose,s)) let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) -let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s) -let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s) -let current_status coqtop = eval_call coqtop Ide_intf.current_status +let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) +let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) +let status coqtop = eval_call coqtop Ide_intf.status module PrintOpt = struct @@ -227,8 +226,8 @@ struct List.fold_left (fun acc cmd -> let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in - match raw_interp coqtop str with - | Ide_intf.Good () -> acc + match interp coqtop ~raw:true ~verbose:false str with + | Ide_intf.Good _ -> acc | Ide_intf.Fail (l,errstr) -> Ide_intf.Fail (l,"Could not eval \""^str^"\": "^errstr) ) (Ide_intf.Good ()) @@ -242,8 +241,8 @@ struct state_hack (Ide_intf.Good ()) end -let current_goals coqtop = +let goals coqtop = match PrintOpt.enforce_hack coqtop with - | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals + | Ide_intf.Good () -> eval_call coqtop Ide_intf.goals | Ide_intf.Fail str -> Ide_intf.Fail str diff --git a/ide/coq.mli b/ide/coq.mli index 04155ac40..685bfcac3 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -45,14 +45,13 @@ val interrupter : (int -> unit) ref (** * Calls to Coqtop, cf [Ide_intf] for more details *) -val interp : coqtop -> bool -> string -> unit Ide_intf.value -val raw_interp : coqtop -> string -> unit Ide_intf.value -val read_stdout : coqtop -> string Ide_intf.value +val interp : + coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value val rewind : coqtop -> int -> unit Ide_intf.value -val is_in_loadpath : coqtop -> string -> bool Ide_intf.value -val make_cases : coqtop -> string -> string list list Ide_intf.value -val current_status : coqtop -> string Ide_intf.value -val current_goals : coqtop -> Ide_intf.goals Ide_intf.value +val status : coqtop -> string Ide_intf.value +val goals : coqtop -> Ide_intf.goals Ide_intf.value +val inloadpath : coqtop -> string -> bool Ide_intf.value +val mkcases : coqtop -> string -> string list list Ide_intf.value (** A specialized version of [raw_interp] dedicated to set/unset options. *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 0f5321486..7a714b1d0 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -829,7 +829,7 @@ object(self) else (fun _ _ -> ()) in try - match Coq.current_goals !mycoqtop with + match Coq.goals !mycoqtop with | Ide_intf.Fail (l,str) -> self#set_message ("Error in coqtop :\n"^str) | Ide_intf.Good goals -> @@ -842,7 +842,7 @@ object(self) method show_goals = self#show_goals_full - method private send_to_coq ct verbosely phrase show_output show_error localize = + method private send_to_coq ct verbose phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in let display_error (loc,s) = @@ -873,16 +873,11 @@ object(self) prerr_endline "Send_to_coq starting now"; (* It's important here to work with [ct] and not [!mycoqtop], otherwise we could miss a restart of coqtop and continue sending it orders. *) - match Coq.interp ct verbosely phrase with + match Coq.interp ct ~verbose phrase with | Ide_intf.Fail (l,str) -> sync display_error (l,str); None - | Ide_intf.Good () -> - match Coq.read_stdout ct with - | Ide_intf.Fail (l,str) -> sync display_error (l,str); None - | Ide_intf.Good msg -> - sync display_output msg; - (** TODO: Restore someday the access to Decl_mode.get_damon_flag, - and also detect the use of admit, and then return Unsafe *) - Some Safe + | Ide_intf.Good msg -> sync display_output msg; Some Safe + (* TODO: Restore someday the access to Decl_mode.get_damon_flag, + and also detect the use of admit, and then return Unsafe *) with | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *) raise RestartCoqtop @@ -1253,24 +1248,22 @@ object(self) (input_view#event#connect#key_press ~callback:self#active_keypress_handler); prerr_endline "CONNECTED active : "; print_id (match act_id with Some x -> x | None -> assert false); - match - filename - with + match filename with | None -> () | Some f -> let dir = Filename.dirname f in let ct = !mycoqtop in - match Coq.is_in_loadpath ct dir with + match Coq.inloadpath ct dir with | Ide_intf.Fail (_,str) -> self#set_message ("Could not determine lodpath, this might lead to problems:\n"^str) | Ide_intf.Good true -> () | Ide_intf.Good false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - match Coq.interp ct false cmd with + match Coq.interp ct cmd with | Ide_intf.Fail (l,str) -> self#set_message ("Couln't add loadpath:\n"^str) - | Ide_intf.Good () -> () + | Ide_intf.Good _ -> () end method private electric_paren tag = @@ -2180,7 +2173,7 @@ let main files = ignore (f av); pop_info (); push_info - (match Coq.current_status !(current.toplvl) with + (match Coq.status !(current.toplvl) with | Ide_intf.Fail (l,str) -> "Oops, problem while fetching coq status." | Ide_intf.Good str -> str) @@ -2195,7 +2188,7 @@ let main files = let w = get_current_word () in let cur_ct = !(session_notebook#current_term.toplvl) in try - match Coq.make_cases cur_ct w with + match Coq.mkcases cur_ct w with | Ide_intf.Fail _ -> raise Not_found | Ide_intf.Good cases -> let print_branch c l = -- cgit v1.2.3