From 1d4bbefe5fe19306ab415e537863763a0a74134a Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 23 Aug 2020 16:09:10 -0700 Subject: Add an XML message for "Show Proof Diffs" Add menu item that uses this --- ide/coqide/coq.ml | 4 ++++ ide/coqide/coq.mli | 5 +++++ ide/coqide/coqOps.ml | 22 ++++++++++++++++++++++ ide/coqide/coqOps.mli | 2 +- ide/coqide/coqide.ml | 33 ++++++++++++++++++++++++++++++--- ide/coqide/coqide_ui.ml | 1 + ide/coqide/fake_ide.ml | 30 +++++++++++++++++------------- ide/coqide/idetop.ml | 19 +++++++++++++++++-- ide/coqide/protocol/interface.ml | 5 +++++ ide/coqide/protocol/xmlprotocol.ml | 31 ++++++++++++++++++++++++++++--- ide/coqide/protocol/xmlprotocol.mli | 1 + 11 files changed, 131 insertions(+), 22 deletions(-) (limited to 'ide') diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 57cdccce6d..6e5d57c9a5 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -512,6 +512,7 @@ let hints x = eval_call (Xmlprotocol.hints x) let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let proof_diff x = eval_call (Xmlprotocol.proof_diff x) let break_coqtop coqtop workers = if coqtop.status = Busy then @@ -578,6 +579,9 @@ struct let set (type a) (opt : a t) (v : a) = Hashtbl.replace current_state (opt_name opt) (opt_data opt v) + let get (type a) (opt : a t) = + Hashtbl.find current_state (opt_name opt) + let reset () = let init_descr d = List.iter (fun o -> set o d.init) d.opts in List.iter init_descr bool_items; diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli index 82df36c91c..aaaf14e4d0 100644 --- a/ide/coqide/coq.mli +++ b/ide/coqide/coq.mli @@ -127,6 +127,7 @@ val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query val search : Interface.search_sty -> Interface.search_rty query val init : Interface.init_sty -> Interface.init_rty query +val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query @@ -144,6 +145,10 @@ sig val set : 'a t -> 'a -> unit + val get : 'a t -> Interface.option_value + + val diff : string t + val printing_unfocused: unit -> bool (** [enforce] transmits to coq the current option values. diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml index 29ea3ce9ea..97076745a3 100644 --- a/ide/coqide/coqOps.ml +++ b/ide/coqide/coqOps.ml @@ -142,6 +142,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -361,6 +362,27 @@ object(self) let query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next + method proof_diff where ~next : unit Coq.task = + (* todo: would be nice to ignore comments, too *) + let rec back iter = + if iter#is_start then iter + else + let c = iter#char in + if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char) + else if c = int_of_char '.' then iter#backward_char + else iter in + + let where = back (buffer#get_iter_at_mark where) in + let until _ start stop = + (buffer#get_iter_at_mark stop)#compare where >= 0 && + (buffer#get_iter_at_mark start)#compare where <= 0 in + let state_id = fst @@ self#find_id until in + let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with + | StringValue diffs -> diffs + | _ -> "off") in + let proof_diff = Coq.proof_diff (diff_opt, state_id) in + Coq.bind proof_diff next + method private still_valid { edit_id = id } = try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true with Not_found -> false diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli index 3a4678ae9c..84911a6aa8 100644 --- a/ide/coqide/coqOps.mli +++ b/ide/coqide/coqOps.mli @@ -20,6 +20,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -30,7 +31,6 @@ object method get_errors : (int * string) list method get_slaves_status : int * int * string CString.Map.t - method handle_failure : handle_exn_rty -> unit task method destroy : unit -> unit diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index b66da11e7b..f9e6e74372 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -747,6 +747,24 @@ let coq_icon () = let dir = List.find chk (Minilib.coqide_data_dirs ()) in Filename.concat dir name +let show_proof_diff where sn = + sn.messages#default_route#clear; + Coq.try_grab sn.coqtop (sn.coqops#proof_diff where + ~next:(function + | Interface.Fail (_, _, err) -> + let err = if (Pp.string_of_ppcmds err) <> "No proofs to diff." then err else + Pp.str "Put the cursor over proven lines for \"Show Proof\" diffs" + in + let err = Ideutils.validate err in + sn.messages#default_route#add err; + Coq.return () + | Interface.Good diff -> + sn.messages#default_route#add diff; + Coq.return ())) + ignore + +let show_proof_diffs _ = cb_on_current_term (show_proof_diff `INSERT) () + let about _ = let dialog = GWindow.about_dialog () in let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in @@ -1103,6 +1121,8 @@ let build_ui () = radio "Set diff" 1 ~label:"Show diffs: only _added"; radio "Set removed diff" 2 ~label:"Show diffs: added and _removed"; ]; + item "Show Proof Diffs" ~label:"_Show Proof (with diffs, if set)" ~accel:(modifier_for_display#get ^ "S") + ~callback:MiscMenu.show_proof_diffs; ]; toggle_items view_menu Coq.PrintOpt.bool_items; @@ -1352,6 +1372,11 @@ let main files = this default coqtop path *) let read_coqide_args argv = + let set_debug () = + Minilib.debug := true; + Flags.debug := true; + Exninfo.record_backtrace true + in let rec filter_coqtop coqtop project_files bindings_files out = function |"-unicode-bindings" :: sfilenames :: args -> let filenames = Str.split (Str.regexp ",") sfilenames in @@ -1371,10 +1396,12 @@ let read_coqide_args argv = |"-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1 |"-debug"::args -> - Minilib.debug := true; - Flags.debug := true; - Exninfo.record_backtrace true; + set_debug (); filter_coqtop coqtop project_files bindings_files ("-debug"::out) args + |"-xml-debug"::args -> + set_debug (); + Flags.xml_debug := true; + filter_coqtop coqtop project_files bindings_files ("-xml-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files bindings_files out args diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index e9ff1bbba1..6540fc6fca 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -89,6 +89,7 @@ let init () = \n \ \n \ \n \ +\n \ \n \ \n \ \n \ diff --git a/ide/coqide/fake_ide.ml b/ide/coqide/fake_ide.ml index e1736a5fe0..034f5b4e2a 100644 --- a/ide/coqide/fake_ide.ml +++ b/ide/coqide/fake_ide.ml @@ -136,7 +136,7 @@ module Parser = struct (* {{{ *) match g with | Item (s,_) -> Printf.sprintf "%s" (clean s) | Opt g -> Printf.sprintf "[%s]" (print g) - | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Alt gs -> Printf.sprintf "( %s )" (String.concat "\n| " (List.map print gs)) | Seq gs -> String.concat " " (List.map print gs) let rec print_toklist = function @@ -253,6 +253,9 @@ let eval_print l coq = after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> eval_call (query (0,(phrase,tip_id()))) coq + | [ Tok(_,"PDIFF"); Tok(_,id) ] -> + let to_id, _ = get_id id in + eval_call (proof_diff ("on",to_id)) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in eval_call (query (0,(phrase, to_id))) coq @@ -282,6 +285,7 @@ let grammar = ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase] ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "PDIFF"); Item eat_id ] ; Seq [Item (eat_rex "WAIT")] ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] @@ -295,12 +299,11 @@ let grammar = let read_command inc = Parser.parse grammar inc let usage () = - error (Printf.sprintf - "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ - Usage: %s (file|-) []\n\ - Input syntax is the following:\n%s\n" - (Filename.basename Sys.argv.(0)) - (Parser.print grammar)) + prerr_endline (Printf.sprintf "Usage: %s ( file | - ) [ \"\" ]\n\ + Input syntax is:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)); + exit 1 module Coqide = Spawn.Sync () @@ -308,14 +311,15 @@ let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"] in let idetop_name = System.get_toplevel_path "coqidetop" in - let coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> Array.of_list def_args, f - | [| _; f; ct |] -> - let ct = Str.split (Str.regexp " ") ct in - Array.of_list (def_args @ ct), f + let input_file, args = match Sys.argv with + | [| _; f |] -> f, [] + | [| _; f; args |] -> + let args = Str.split (Str.regexp " ") args in + f, args | _ -> usage () in + let def_coqtop_args = ["--xml_format=Ppcmds"] in + let coqtop_args = Array.of_list(def_coqtop_args @ args) in let inc = if input_file = "-" then stdin else open_in input_file in prerr_endline ("Running: "^idetop_name^" "^ (String.concat " " (Array.to_list coqtop_args))); diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2adc35ae3e..2be8f862ea 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -367,6 +367,17 @@ let export_option_state s = { Interface.opt_value = export_option_value s.Goptions.opt_value; } +exception NotSupported of string + +let proof_diff (diff_opt, sid) = + let diff_opt = Proof_diffs.string_to_diffs diff_opt in + let doc = get_doc () in + match Stm.get_proof ~doc sid with + | None -> CErrors.user_err (Pp.str "No proofs to diff.") + | Some proof -> + let old = Stm.get_prev_proof ~doc sid in + Proof_diffs.diff_proofs ~diff_opt ?old proof + let get_options () = let table = Goptions.get_tables () in let fold key state accu = (key, export_option_state state) :: accu in @@ -455,6 +466,7 @@ let eval_call c = Interface.hints = interruptible hints; Interface.status = interruptible status; Interface.search = interruptible search; + Interface.proof_diff = interruptible proof_diff; Interface.get_options = interruptible get_options; Interface.set_options = interruptible set_options; Interface.mkcases = interruptible idetop_make_cases; @@ -479,6 +491,8 @@ let print_xml = let m = Mutex.create () in fun oc xml -> Mutex.lock m; + if !Flags.xml_debug then + Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e @@ -507,7 +521,7 @@ let loop run_mode ~opts:_ state = set_doc state.doc; init_signal_handler (); catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in + let in_ch, out_ch = Spawned.get_channels () in let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in let in_lb = Lexing.from_function (fun s len -> CThread.thread_friendly_read in_ch s ~off:0 ~len) in @@ -518,7 +532,8 @@ let loop run_mode ~opts:_ state = while not !quit do try let xml_query = Xml_parser.parse xml_ic in -(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) + if !Flags.xml_debug then + pr_with_pid (Xml_printer.to_string_fmt xml_query); let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in let r = eval_call q in diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml index 646012dcaa..86a81446e8 100644 --- a/ide/coqide/protocol/interface.ml +++ b/ide/coqide/protocol/interface.ml @@ -187,6 +187,10 @@ type status_rty = status type search_sty = search_flags type search_rty = string coq_object list +(** Diffs between the proof term at a given stateid and the previous one *) +type proof_diff_sty = string * Stateid.t +type proof_diff_rty = Pp.t + (** Retrieve the list of options of the current toplevel *) type get_options_sty = unit type get_options_rty = (option_name * option_state) list @@ -252,6 +256,7 @@ type handler = { stop_worker : stop_worker_sty -> stop_worker_rty; print_ast : print_ast_sty -> print_ast_rty; annotate : annotate_sty -> annotate_rty; + proof_diff : proof_diff_sty -> proof_diff_rty; handle_exn : handle_exn_sty -> handle_exn_rty; init : init_sty -> init_rty; quit : quit_sty -> quit_rty; diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 6cb0cec008..0780f03903 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -12,7 +12,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20170413" +let protocol_version = "20200911" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -278,6 +278,7 @@ module ReifType : sig 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 pp_t : Pp.t val_t val of_value_type : 'a val_t -> 'a -> xml val to_value_type : 'a val_t -> xml -> 'a @@ -314,6 +315,7 @@ end = struct | State_id : state_id val_t | Route_id : route_id val_t | Search_cst : search_constraint val_t + | Pp : Pp.t val_t type value_type = Value_type : 'a val_t -> value_type @@ -340,6 +342,7 @@ end = struct let state_id_t = State_id let route_id_t = Route_id let search_cst_t = Search_cst + let pp_t = Pp let of_value_type (ty : 'a val_t) : 'a -> xml = let rec convert : type a. a val_t -> a -> xml = function @@ -362,6 +365,7 @@ end = struct | State_id -> of_stateid | Route_id -> of_routeid | Search_cst -> of_search_cst + | Pp -> of_pp in convert ty @@ -386,6 +390,7 @@ end = struct | State_id -> to_stateid | Route_id -> to_routeid | Search_cst -> to_search_cst + | Pp -> to_pp in convert ty @@ -443,6 +448,8 @@ end = struct | In_Module s -> "In_Module " ^ String.concat "." s | Include_Blacklist -> "Include_Blacklist" + let pr_pp = Pp.string_of_ppcmds + let rec print : type a. a val_t -> a -> string = function | Unit -> pr_unit | Bool -> pr_bool @@ -463,6 +470,7 @@ end = struct | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id | Route_id -> pr_int + | Pp -> pr_pp (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -489,6 +497,7 @@ end = struct 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" + | Pp -> assert(true : Pp.t exists); "Pp.t" let print_type = function Value_type ty -> print_val_t ty @@ -507,6 +516,8 @@ end = struct (pr_xml (of_pair of_bool of_int (false,3))); Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) (pr_xml (of_union of_bool of_int (Inl false))); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp) + (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") ))); print_endline ("All other types are records represented by a node named like the OCaml\n"^ "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) @@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t let stop_worker_sty_t : stop_worker_sty val_t = string_t let print_ast_sty_t : print_ast_sty val_t = state_id_t let annotate_sty_t : annotate_sty val_t = string_t +let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) @@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string let stop_worker_rty_t : stop_worker_rty val_t = unit_t let print_ast_rty_t : print_ast_rty val_t = xml_t let annotate_rty_t : annotate_rty val_t = xml_t +let proof_diff_rty_t : proof_diff_rty val_t = pp_t let ($) x = erase x let calls = [| @@ -585,6 +598,7 @@ let calls = [| "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; + "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; |] type 'a call = @@ -609,7 +623,9 @@ type 'a call = | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call | Annotate : annotate_sty -> annotate_rty call + | PDiff : proof_diff_sty -> proof_diff_rty call +(* the order of the entries must match the order in "calls" above *) let id_of_call : type a. a call -> int = function | Add _ -> 0 | Edit_at _ -> 1 @@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function | StopWorker _ -> 16 | PrintAst _ -> 17 | Annotate _ -> 18 + | PDiff _ -> 19 let str_of_call c = pi1 calls.(id_of_call c) @@ -652,8 +669,9 @@ 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 -let annotate x : annotate_rty call = Annotate x +let print_ast x : print_ast_rty call = PrintAst x +let annotate x : annotate_rty call = Annotate x +let proof_diff x : proof_diff_rty call = PDiff x let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> let mkGood : type a. a -> a value = fun x -> Good x in @@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | StopWorker x -> mkGood (handler.stop_worker x) | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) + | PDiff x -> mkGood (handler.proof_diff x) with any -> let any = Exninfo.capture any in Fail (handler.handle_exn any) @@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) + | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) let of_answer msg_fmt = msg_format := msg_fmt; of_answer @@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) | Annotate _ -> to_value (to_value_type annotate_rty_t ) + | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) let of_call : type a. a call -> xml = fun q -> let mkCall x = constructor "call" (str_of_call q) [x] in @@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q -> | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) | Annotate x -> mkCall (of_value_type annotate_sty_t x) + | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) let to_call : xml -> unknown_call = do_match "call" (fun s a -> @@ -774,6 +796,7 @@ let to_call : xml -> unknown_call = | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) + | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | x -> raise (Marshal_error("call",PCData x))) (** Debug printing *) @@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value | Annotate _ -> pr_value_gen (print annotate_rty_t ) value + | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value let pr_call : type a. a call -> string = fun call -> let return what x = str_of_call call ^ " " ^ print what x in match call with @@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call -> | StopWorker x -> return stop_worker_sty_t x | PrintAst x -> return print_ast_sty_t x | Annotate x -> return annotate_sty_t x + | PDiff x -> return proof_diff_sty_t x let document to_string_fmt = Printf.printf "=== Available calls ===\n\n"; diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli index 44584d44d7..4dc05c18a9 100644 --- a/ide/coqide/protocol/xmlprotocol.mli +++ b/ide/coqide/protocol/xmlprotocol.mli @@ -37,6 +37,7 @@ val wait : wait_sty -> wait_rty call val interp : interp_sty -> interp_rty call val print_ast : print_ast_sty -> print_ast_rty call val annotate : annotate_sty -> annotate_rty call +val proof_diff : proof_diff_sty -> proof_diff_rty call val abstract_eval_call : handler -> 'a call -> 'a value -- cgit v1.2.3