diff options
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 176 |
1 files changed, 124 insertions, 52 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index aecb317b..e1821921 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -1,16 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Protocol version of this file. This is the date of the last modification. *) (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20150913" +let protocol_version = "20170413" + +type msg_format = Richpp of int | Ppcmds +let msg_format = ref (Richpp 72) (** * Interface of calls to Coq by CoqIde *) @@ -92,10 +97,64 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) -let of_richpp x = Element ("richpp", [], [Richpp.repr x]) -let to_richpp xml = match xml with - | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x - | x -> raise Serialize.(Marshal_error("richpp",x)) +let to_routeid = function + | Element ("route_id",["val",i],[]) -> + let id = int_of_string i in id + | _ -> raise (Invalid_argument "to_route_id") + +let of_routeid i = Element ("route_id",["val",string_of_int i],[]) + +let of_box (ppb : Pp.block_type) = let open Pp in match ppb with + | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] + | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] + | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] + +let to_box = let open Pp in + do_match "ppbox" (fun s args -> match s with + | "hbox" -> Pp_hbox (to_int (singleton args)) + | "vbox" -> Pp_vbox (to_int (singleton args)) + | "hvbox" -> Pp_hvbox (to_int (singleton args)) + | "hovbox" -> Pp_hovbox (to_int (singleton args)) + | x -> raise (Marshal_error("*ppbox",PCData x)) + ) + +let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with + | Ppcmd_empty -> constructor "ppdoc" "empty" [] + | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] + | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] + | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] + | Ppcmd_print_break (i,j) + -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] + | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] + | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] + + +let rec to_pp xpp = let open Pp in + Pp.unrepr @@ + do_match "ppdoc" (fun s args -> match s with + | "empty" -> Ppcmd_empty + | "string" -> Ppcmd_string (to_string (singleton args)) + | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) + | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in + Ppcmd_box(bt,s) + | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in + Ppcmd_tag(tg,s) + | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in + Ppcmd_print_break(i, j) + | "newline" -> Ppcmd_force_newline + | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) + | x -> raise (Marshal_error("*ppdoc",PCData x)) + ) xpp + +let of_richpp x = Element ("richpp", [], [x]) + +(* Run-time Selectable *) +let of_pp (pp : Pp.t) = + match !msg_format with + | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) + | Ppcmds -> of_pp pp let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) @@ -104,7 +163,7 @@ let of_value f = function | None -> [] | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg]) + Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) let to_value f = function | Element ("value", attrs, l) -> @@ -120,7 +179,7 @@ let to_value f = function in let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in let id = to_stateid id in - let msg = to_richpp msg in + let msg = to_pp msg in Fail (id, loc, msg) else raise (Marshal_error("good or fail",PCData ans)) | x -> raise (Marshal_error("value",x)) @@ -147,15 +206,15 @@ let to_evar = function | x -> raise (Marshal_error("evar",x)) let of_goal g = - let hyp = of_list of_richpp g.goal_hyp in - let ccl = of_richpp g.goal_ccl in + let hyp = of_list of_pp g.goal_hyp in + let ccl = of_pp g.goal_ccl in let id = of_string g.goal_id in Element ("goal", [], [id; hyp; ccl]) let to_goal = function | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_richpp hyp in - let ccl = to_richpp ccl in - let id = to_string id in + let hyp = to_list to_pp hyp in + let ccl = to_pp ccl in + let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | x -> raise (Marshal_error("goal",x)) @@ -219,6 +278,7 @@ module ReifType : sig val coq_info_t : coq_info val_t val coq_object_t : 'a val_t -> 'a coq_object val_t val state_id_t : state_id val_t + val route_id_t : route_id val_t val search_cst_t : search_constraint val_t val of_value_type : 'a val_t -> 'a -> xml @@ -254,6 +314,7 @@ end = struct | Coq_info : coq_info val_t | Coq_object : 'a val_t -> 'a coq_object val_t | State_id : state_id val_t + | Route_id : route_id val_t | Search_cst : search_constraint val_t type value_type = Value_type : 'a val_t -> value_type @@ -279,6 +340,7 @@ end = struct let coq_info_t = Coq_info let coq_object_t x = Coq_object x let state_id_t = State_id + let route_id_t = Route_id let search_cst_t = Search_cst let of_value_type (ty : 'a val_t) : 'a -> xml = @@ -300,6 +362,7 @@ end = struct | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) | Union (t1,t2) -> (of_union (convert t1) (convert t2)) | State_id -> of_stateid + | Route_id -> of_routeid | Search_cst -> of_search_cst in convert ty @@ -323,6 +386,7 @@ end = struct | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) | Union (t1,t2) -> (to_union (convert t1) (convert t2)) | State_id -> to_stateid + | Route_id -> to_routeid | Search_cst -> to_search_cst in convert ty @@ -344,8 +408,8 @@ end = struct Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ - Richpp.raw_print goal ^ "]" in + "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ + Pp.string_of_ppcmds goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -400,6 +464,7 @@ end = struct | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id + | Route_id -> pr_int (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -425,6 +490,7 @@ end = struct | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" + | Route_id -> assert(true : route_id exists); "route_id" let print_type = function Value_type ty -> print_val_t ty @@ -456,7 +522,7 @@ open ReifType let add_sty_t : add_sty val_t = pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t string_t state_id_t +let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) let goals_sty_t : goals_sty val_t = unit_t let evars_sty_t : evars_sty val_t = unit_t let hints_sty_t : hints_sty val_t = unit_t @@ -467,6 +533,7 @@ let set_options_sty_t : set_options_sty val_t = list_t (pair_t (list_t string_t) option_value_t) let mkcases_sty_t : mkcases_sty val_t = string_t let quit_sty_t : quit_sty val_t = unit_t +let wait_sty_t : wait_sty val_t = unit_t let about_sty_t : about_sty val_t = unit_t let init_sty_t : init_sty val_t = option_t string_t let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t @@ -478,7 +545,7 @@ let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) let edit_at_rty_t : edit_at_rty val_t = union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = string_t +let query_rty_t : query_rty val_t = unit_t let goals_rty_t : goals_rty val_t = option_t goals_t let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) let hints_rty_t : hints_rty val_t = @@ -491,6 +558,7 @@ let get_options_rty_t : get_options_rty val_t = let set_options_rty_t : set_options_rty val_t = unit_t let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) let quit_rty_t : quit_rty val_t = unit_t +let wait_rty_t : wait_rty val_t = unit_t let about_rty_t : about_rty val_t = coq_info_t let init_rty_t : init_rty val_t = state_id_t let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) @@ -512,6 +580,7 @@ let calls = [| "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; "Quit", ($)quit_sty_t, ($)quit_rty_t; + "Wait", ($)wait_sty_t, ($)wait_rty_t; "About", ($)about_sty_t, ($)about_rty_t; "Init", ($)init_sty_t, ($)init_rty_t; "Interp", ($)interp_sty_t, ($)interp_rty_t; @@ -536,6 +605,8 @@ type 'a call = | About : about_sty -> about_rty call | Init : init_sty -> init_rty call | StopWorker : stop_worker_sty -> stop_worker_rty call + (* internal use (fake_ide) only, do not use *) + | Wait : wait_sty -> wait_rty call (* retrocompatibility *) | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call @@ -554,12 +625,13 @@ let id_of_call : type a. a call -> int = function | SetOptions _ -> 9 | MkCases _ -> 10 | Quit _ -> 11 - | About _ -> 12 - | Init _ -> 13 - | Interp _ -> 14 - | StopWorker _ -> 15 - | PrintAst _ -> 16 - | Annotate _ -> 17 + | Wait _ -> 12 + | About _ -> 13 + | Init _ -> 14 + | Interp _ -> 15 + | StopWorker _ -> 16 + | PrintAst _ -> 17 + | Annotate _ -> 18 let str_of_call c = pi1 calls.(id_of_call c) @@ -579,6 +651,7 @@ let mkcases x : mkcases_rty call = MkCases x let search x : search_rty call = Search x let quit x : quit_rty call = Quit x let init x : init_rty call = Init x +let wait x : wait_rty call = Wait x let interp x : interp_rty call = Interp x let stop_worker x : stop_worker_rty call = StopWorker x let print_ast x : print_ast_rty call = PrintAst x @@ -600,6 +673,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | SetOptions x -> mkGood (handler.set_options x) | MkCases x -> mkGood (handler.mkcases x) | Quit x -> mkGood (handler.quit x) + | Wait x -> mkGood (handler.wait x) | About x -> mkGood (handler.about x) | Init x -> mkGood (handler.init x) | Interp x -> mkGood (handler.interp x) @@ -624,6 +698,7 @@ let of_answer : type a. a call -> a value -> xml = function | SetOptions _ -> of_value (of_value_type set_options_rty_t) | MkCases _ -> of_value (of_value_type mkcases_rty_t ) | Quit _ -> of_value (of_value_type quit_rty_t ) + | Wait _ -> of_value (of_value_type wait_rty_t ) | About _ -> of_value (of_value_type about_rty_t ) | Init _ -> of_value (of_value_type init_rty_t ) | Interp _ -> of_value (of_value_type interp_rty_t ) @@ -631,6 +706,9 @@ let of_answer : type a. a call -> a value -> xml = function | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) +let of_answer msg_fmt = + msg_format := msg_fmt; of_answer + let to_answer : type a. a call -> xml -> a value = function | Add _ -> to_value (to_value_type add_rty_t ) | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) @@ -644,6 +722,7 @@ let to_answer : type a. a call -> xml -> a value = function | SetOptions _ -> to_value (to_value_type set_options_rty_t) | MkCases _ -> to_value (to_value_type mkcases_rty_t ) | Quit _ -> to_value (to_value_type quit_rty_t ) + | Wait _ -> to_value (to_value_type wait_rty_t ) | About _ -> to_value (to_value_type about_rty_t ) | Init _ -> to_value (to_value_type init_rty_t ) | Interp _ -> to_value (to_value_type interp_rty_t ) @@ -666,6 +745,7 @@ let of_call : type a. a call -> xml = fun q -> | SetOptions x -> mkCall (of_value_type set_options_sty_t x) | MkCases x -> mkCall (of_value_type mkcases_sty_t x) | Quit x -> mkCall (of_value_type quit_sty_t x) + | Wait x -> mkCall (of_value_type wait_sty_t x) | About x -> mkCall (of_value_type about_sty_t x) | Init x -> mkCall (of_value_type init_sty_t x) | Interp x -> mkCall (of_value_type interp_sty_t x) @@ -689,6 +769,7 @@ let to_call : xml -> unknown_call = | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a)) | "MkCases" -> Unknown (MkCases (mkCallArg mkcases_sty_t a)) | "Quit" -> Unknown (Quit (mkCallArg quit_sty_t a)) + | "Wait" -> Unknown (Wait (mkCallArg wait_sty_t a)) | "About" -> Unknown (About (mkCallArg about_sty_t a)) | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) @@ -701,10 +782,10 @@ let to_call : xml -> unknown_call = let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with | Add _ -> pr_value_gen (print add_rty_t ) value @@ -719,6 +800,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | SetOptions _ -> pr_value_gen (print set_options_rty_t) value | MkCases _ -> pr_value_gen (print mkcases_rty_t ) value | Quit _ -> pr_value_gen (print quit_rty_t ) value + | Wait _ -> pr_value_gen (print wait_rty_t ) value | About _ -> pr_value_gen (print about_rty_t ) value | Init _ -> pr_value_gen (print init_rty_t ) value | Interp _ -> pr_value_gen (print interp_rty_t ) value @@ -740,6 +822,7 @@ let pr_call : type a. a call -> string = fun call -> | SetOptions x -> return set_options_sty_t x | MkCases x -> return mkcases_sty_t x | Quit x -> return quit_sty_t x + | Wait x -> return wait_sty_t x | About x -> return about_sty_t x | Init x -> return init_sty_t x | Interp x -> return interp_sty_t x @@ -760,7 +843,7 @@ let document to_string_fmt = (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); + (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); document_type_encoding to_string_fmt (* Moved from feedback.mli : This is IDE specific and we don't want to @@ -787,20 +870,14 @@ let to_message_level = let of_message lvl loc msg = let lvl = of_message_level lvl in let xloc = of_option of_loc loc in - let content = of_richpp msg in + let content = of_pp msg in Xml_datatype.Element ("message", [], [lvl; xloc; content]) let to_message xml = match xml with | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) + Message(to_message_level lvl, to_option to_loc xloc, to_pp content) | x -> raise (Marshal_error("message",x)) -let is_message xml = - try begin match to_message xml with - | Message(l,c,m) -> Some (l,c,m) - | _ -> None - end with | Marshal_error _ -> None - let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom | "processed", _ -> Processed @@ -816,8 +893,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "workerstatus", [ns] -> let n, s = to_pair to_string to_string ns in WorkerStatus(n,s) - | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) + | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> @@ -849,10 +925,8 @@ let of_feedback_content = function | WorkerStatus(n,s) -> constructor "feedback_content" "workerstatus" [of_pair of_string of_string (n,s)] - | Goals (loc,s) -> - constructor "feedback_content" "goals" [of_loc loc;of_string s] | Custom (loc, name, x) -> - constructor "feedback_content" "custom" [of_loc loc; of_string name; x] + constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; @@ -863,23 +937,21 @@ let of_feedback_content = function of_string filename ] | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] -let of_edit_or_state_id = function - | Edit id -> ["object","edit"], of_edit_id id - | State id -> ["object","state"], of_stateid id +let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.id in + let obj, id = of_edit_or_state_id msg.span_id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) +let of_feedback msg_fmt = + msg_format := msg_fmt; of_feedback + let to_feedback xml = match xml with - | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { - id = Edit(to_edit_id id); - route = int_of_string route; - contents = to_feedback_content content } - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = State(to_stateid id); + | Element ("feedback", ["object","state";"route",route], [id;content]) -> { + doc_id = 0; + span_id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) |