diff options
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d337a911d8..7445ce5ca0 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20140312" +let protocol_version = "20150913" (** * Interface of calls to Coq by CoqIde *) @@ -90,7 +90,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 = Stateid.to_xml id in - Element ("value", ["val", "fail"] @ loc, [id;PCData msg]) + Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg]) let to_value f = function | Element ("value", attrs, l) -> let ans = massoc "val" attrs in @@ -103,8 +103,9 @@ let to_value f = function Some (loc_s, loc_e) with Marshal_error | Failure _ -> None in - let id = Stateid.of_xml (List.hd l) in - let msg = raw_string (List.tl l) in + let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in + let id = Stateid.of_xml id in + let msg = Richpp.to_richpp msg in Fail (id, loc, msg) else raise Marshal_error | _ -> raise Marshal_error @@ -131,14 +132,14 @@ let to_evar = function | _ -> raise Marshal_error let of_goal g = - let hyp = of_list of_string g.goal_hyp in - let ccl = of_string g.goal_ccl in + let hyp = of_list Richpp.of_richpp g.goal_hyp in + let ccl = Richpp.of_richpp 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_string hyp in - let ccl = to_string ccl in + let hyp = to_list Richpp.to_richpp hyp in + let ccl = Richpp.to_richpp ccl in let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | _ -> raise Marshal_error @@ -318,10 +319,9 @@ end = struct (List.length lg + List.length rg) pr_focus l in Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else - let pr_menu s = s in let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ - pr_menu goal ^ "]" in + "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ + Richpp.raw_print goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -672,10 +672,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^" ["^str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value call value = match call with | Add _ -> pr_value_gen (print add_rty_t ) (Obj.magic value) @@ -731,7 +731,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),"error message")))); + (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); document_type_encoding to_string_fmt (* vim: set foldmethod=marker: *) |