diff options
Diffstat (limited to 'toplevel/ide_intf.ml')
| -rw-r--r-- | toplevel/ide_intf.ml | 43 |
1 files changed, 32 insertions, 11 deletions
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 9ba3d8b4..0df24c7a 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20120511" +let protocol_version = "20120710" (** * Interface of calls to Coq by CoqIde *) @@ -338,13 +338,25 @@ let to_call = function let of_status s = let of_so = of_option of_string in - Element ("status", [], [of_so s.status_path; of_so s.status_proofname]) + let of_sl = of_list of_string in + Element ("status", [], + [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_statenum; + of_int s.status_proofnum; + ] + ) let to_status = function -| Element ("status", [], [path; name]) -> +| Element ("status", [], [path; name; prfs; snum; pnum]) -> { - status_path = to_option to_string path; + status_path = to_list to_string path; status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_statenum = to_int snum; + status_proofnum = to_int pnum; } | _ -> raise Marshal_error @@ -370,14 +382,16 @@ let to_goal = function | _ -> raise Marshal_error let of_goals g = + let of_glist = of_list of_goal in let fg = of_list of_goal g.fg_goals in - let bg = of_list of_goal g.bg_goals in + let bg = of_list (of_pair of_glist of_glist) g.bg_goals in Element ("goals", [], [fg; bg]) let to_goals = function | Element ("goals", [], [fg; bg]) -> + let to_glist = to_list to_goal in let fg = to_list to_goal fg in - let bg = to_list to_goal bg in + let bg = to_list (to_pair to_glist to_glist) bg in { fg_goals = fg; bg_goals = bg; } | _ -> raise Marshal_error @@ -495,9 +509,9 @@ let pr_string s = "["^s^"]" let pr_bool b = if b then "true" else "false" let pr_status s = - let path = match s.status_path with - | None -> "no path; " - | Some p -> "path = " ^ p ^ "; " + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in let name = match s.status_proofname with | None -> "no proof;" @@ -512,7 +526,14 @@ let pr_mkcases l = let pr_goals_aux g = if g.fg_goals = [] then if g.bg_goals = [] then "Proof completed." - else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" (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 } = |