diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /toplevel/ide_intf.ml | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'toplevel/ide_intf.ml')
-rw-r--r-- | toplevel/ide_intf.ml | 120 |
1 files changed, 117 insertions, 3 deletions
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index fc8ffa25..9ba3d8b4 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -6,6 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Protocol version of this file. This is the date of the last modification. *) + +(** WARNING: TO BE UPDATED WHEN MODIFIED! *) + +let protocol_version = "20120511" + (** * Interface of calls to Coq by CoqIde *) open Xml_parser @@ -22,10 +28,32 @@ type 'a call = | Evars | Hints | Status + | Search of search_flags | GetOptions | SetOptions of (option_name * option_value) list | InLoadPath of string | MkCases of string + | Quit + | About + +(** The structure that coqtop should implement *) + +type handler = { + interp : raw * verbose * string -> string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + search : search_flags -> search_answer list; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + quit : unit -> unit; + about : unit -> coq_info; + handle_exn : exn -> location * string; +} (** The actual calls *) @@ -35,10 +63,12 @@ let goals : goals option call = Goal let evars : evar list option call = Evars let hints : (hint list * hint) option call = Hints let status : status call = Status +let search flags : search_answer list call = Search flags let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s let mkcases s : string list list call = MkCases s +let quit : unit call = Quit (** * Coq answers to CoqIde *) @@ -51,10 +81,13 @@ let abstract_eval_call handler c = | Evars -> Obj.magic (handler.evars () : evar list option) | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) | Status -> Obj.magic (handler.status () : status) + | Search flags -> Obj.magic (handler.search flags : search_answer list) | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) | SetOptions opts -> Obj.magic (handler.set_options opts : unit) | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) | MkCases s -> Obj.magic (handler.mkcases s : string list list) + | Quit -> Obj.magic (handler.quit () : unit) + | About -> Obj.magic (handler.about () : coq_info) in Good res with e -> let (l, str) = handler.handle_exn e in @@ -178,6 +211,44 @@ let to_option_state = function } | _ -> raise Marshal_error +let of_search_constraint = function +| Name_Pattern s -> + constructor "search_constraint" "name_pattern" [of_string s] +| Type_Pattern s -> + constructor "search_constraint" "type_pattern" [of_string s] +| SubType_Pattern s -> + constructor "search_constraint" "subtype_pattern" [of_string s] +| In_Module m -> + constructor "search_constraint" "in_module" [of_list of_string m] +| Include_Blacklist -> + constructor "search_constraint" "include_blacklist" [] + +let to_search_constraint xml = do_match xml "search_constraint" + (fun s args -> match s with + | "name_pattern" -> Name_Pattern (to_string (singleton args)) + | "type_pattern" -> Type_Pattern (to_string (singleton args)) + | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) + | "in_module" -> In_Module (to_list to_string (singleton args)) + | "include_blacklist" -> Include_Blacklist + | _ -> raise Marshal_error) + +let of_search_answer ans = + let path = of_list of_string ans.search_answer_full_path in + let name = of_string ans.search_answer_base_name in + let tpe = of_string ans.search_answer_type in + Element ("search_answer", [], [path; name; tpe]) + +let to_search_answer = function +| Element ("search_answer", [], [path; name; tpe]) -> + let path = to_list to_string path in + let name = to_string name in + let tpe = to_string tpe in { + search_answer_full_path = path; + search_answer_base_name = name; + search_answer_type = tpe; + } +| _ -> raise Marshal_error + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (loc, msg) -> @@ -218,6 +289,9 @@ let of_call = function Element ("call", ["val", "hints"], []) | Status -> Element ("call", ["val", "status"], []) +| Search flags -> + let args = List.map (of_pair of_search_constraint of_bool) flags in + Element ("call", ["val", "search"], args) | GetOptions -> Element ("call", ["val", "getoptions"], []) | SetOptions opts -> @@ -227,6 +301,10 @@ let of_call = function Element ("call", ["val", "inloadpath"], [PCData file]) | MkCases ind -> Element ("call", ["val", "mkcases"], [PCData ind]) +| Quit -> + Element ("call", ["val", "quit"], []) +| About -> + Element ("call", ["val", "about"], []) let to_call = function | Element ("call", attrs, l) -> @@ -242,6 +320,9 @@ let to_call = function | "goal" -> Goal | "evars" -> Evars | "status" -> Status + | "search" -> + let args = List.map (to_pair to_search_constraint to_bool) l in + Search args | "getoptions" -> GetOptions | "setoptions" -> let args = List.map (to_pair (to_list to_string) to_option_value) l in @@ -249,6 +330,8 @@ let to_call = function | "inloadpath" -> InLoadPath (raw_string l) | "mkcases" -> MkCases (raw_string l) | "hints" -> Hints + | "quit" -> Quit + | "about" -> About | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -275,13 +358,15 @@ let to_evar = function let of_goal g = let hyp = of_list of_string g.goal_hyp in let ccl = of_string g.goal_ccl in - Element ("goal", [], [hyp; ccl]) + let id = of_string g.goal_id in + Element ("goal", [], [id; hyp; ccl]) let to_goal = function -| Element ("goal", [], [hyp; ccl]) -> +| Element ("goal", [], [id; hyp; ccl]) -> let hyp = to_list to_string hyp in let ccl = to_string ccl in - { goal_hyp = hyp; goal_ccl = ccl } + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | _ -> raise Marshal_error let of_goals g = @@ -296,6 +381,23 @@ let to_goals = function { fg_goals = fg; bg_goals = bg; } | _ -> raise Marshal_error +let of_coq_info info = + let version = of_string info.coqtop_version in + let protocol = of_string info.protocol_version in + let release = of_string info.release_date in + let compile = of_string info.compile_date in + Element ("coq_info", [], [version; protocol; release; compile]) + +let to_coq_info = function +| Element ("coq_info", [], [version; protocol; release; compile]) -> + { + coqtop_version = to_string version; + protocol_version = to_string protocol; + release_date = to_string release; + compile_date = to_string compile; + } +| _ -> raise Marshal_error + let of_hints = let of_hint = of_list (of_pair of_string of_string) in of_option (of_pair (of_list of_hint) of_hint) @@ -308,10 +410,13 @@ let of_answer (q : 'a call) (r : 'a value) = | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) | Status -> Obj.magic (of_status : status -> xml) + | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml) | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) + | Quit -> Obj.magic (fun _ -> Element ("unit", [], [])) + | About -> Obj.magic (of_coq_info : coq_info -> xml) in of_value convert r @@ -331,6 +436,8 @@ let to_answer xml = | "evar" -> Obj.magic (to_evar elt : evar) | "option_value" -> Obj.magic (to_option_value elt : option_value) | "option_state" -> Obj.magic (to_option_state elt : option_state) + | "coq_info" -> Obj.magic (to_coq_info elt : coq_info) + | "search_answer" -> Obj.magic (to_search_answer elt : search_answer) | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -370,10 +477,13 @@ let pr_call = function | Evars -> "EVARS" | Hints -> "HINTS" | Status -> "STATUS" + | Search _ -> "SEARCH" | GetOptions -> "GETOPTIONS" | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" | InLoadPath s -> "INLOADPATH "^s | MkCases s -> "MKCASES "^s + | Quit -> "QUIT" + | About -> "ABOUT" let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v @@ -428,7 +538,11 @@ let pr_full_value call value = | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) | Hints -> pr_value value | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | Search _ -> pr_value value | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) | SetOptions _ -> pr_value value | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) + | Quit -> pr_value value + | About -> pr_value value + |