diff options
Diffstat (limited to 'ide')
55 files changed, 135 insertions, 97 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index ac9cc57bc0..eb575b95ff 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq.ml b/ide/coq.ml index cd45e2fcdc..42ab86dd62 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -366,7 +366,14 @@ let bind_self_as f = (** This launches a fresh handle from its command line arguments. *) let spawn_handle args respawner feedback_processor = let prog = coqtop_path () in - let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in + let async_default = + (* disable async processing by default in Windows *) + if List.mem Sys.os_type ["Win32"; "Cygwin"] then + "off" + else + "on" + in + let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in let env = match !Flags.ideslave_coqtop_flags with | None -> None @@ -403,8 +410,19 @@ let clear_handle h = let mkready coqtop = fun () -> coqtop.status <- Ready; Void +let save_all = ref (fun () -> assert false) + let rec respawn_coqtop ?(why=Unexpected) coqtop = - if why = Unexpected then warning "Coqtop died badly. Resetting."; + let () = match why with + | Unexpected -> + let title = "Warning" in + let icon = (warn_image ())#coerce in + let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in + let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in + if ans = 2 then (!save_all (); GtkMain.Main.quit ()) + else if ans = 3 then GtkMain.Main.quit () + | Planned -> () + in clear_handle coqtop.handle; ignore_error (fun () -> coqtop.handle <- diff --git a/ide/coq.mli b/ide/coq.mli index e8e2f5239e..463dd134a4 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -170,3 +170,4 @@ val check_connection : string list -> unit may terminate coqide in case of trouble *) val interrupter : (int -> unit) ref +val save_all : (unit -> unit) ref diff --git a/ide/coqOps.ml b/ide/coqOps.ml index d30d7ab5e0..364fc883ba 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -58,7 +58,7 @@ module SentenceId : sig val connect : sentence -> signals val dbg_to_string : - GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds + GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t end = struct @@ -163,7 +163,7 @@ let flags_to_color f = else `NAME Preferences.processed_color#get (* Move to utils? *) -let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with +let rec validate (s : Pp.t) = match Pp.repr s with | Pp.Ppcmd_empty | Pp.Ppcmd_print_break _ | Pp.Ppcmd_force_newline -> true @@ -373,7 +373,8 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,sid) in + let route_id = 0 in + Coq.query (route_id,(phrase,sid)) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> Coq.return () @@ -841,15 +842,14 @@ object(self) in let try_phrase phrase stop more = let action = log "Sending to coq now" in - let query = Coq.query (phrase,Stateid.dummy) in + let route_id = 0 in + let query = Coq.query (route_id,(phrase,Stateid.dummy)) in let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); more - | Good msg -> - messages#add_string msg; - stop Tags.Script.processed + | Good () -> stop Tags.Script.processed in Coq.bind (Coq.seq action query) next in diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 332c18f2f0..013db684ef 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 5912bec357..1873d5acf8 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index b6286c49fb..8bfd937e38 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coqide.ml b/ide/coqide.ml index a1e78ee3c9..7b65c9fec9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -284,6 +284,8 @@ let saveall _ = | Some f -> ignore (sn.fileops#save f)) notebook#pages +let () = Coq.save_all := saveall + let revert_all _ = List.iter (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert) diff --git a/ide/coqide.mli b/ide/coqide.mli index 744b974ffa..39b4d9ae2f 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 534a3f179d..73a30b18f1 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/document.mli b/ide/document.mli index fb96cb6d76..ab8e71808c 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -102,7 +102,7 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list (** debug print *) val print : - 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds + 'a document -> (bool -> id option -> 'a -> Pp.t) -> Pp.t (** Callbacks on documents *) diff --git a/ide/fileOps.ml b/ide/fileOps.ml index 7be1bdb927..7c09f8628b 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/fileOps.mli b/ide/fileOps.mli index 9f0b75ac56..76014ec752 100644 --- a/ide/fileOps.mli +++ b/ide/fileOps.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index f905053ddb..f0575e325a 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef1..67391f5567 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,7 +1,7 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,9 +20,8 @@ module CompactedDecl = Context.Compacted.Declaration (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered - when the -ideslave option is passed to Coqtop. Currently CoqIDE is - the only one using this mode, but we try here to be as generic as - possible, so this may change in the future... *) + when the -ideslave option is passed to Coqtop. *) + (** Signal handling: we postpone ^C during input and output phases, but make it directly raise a Sys.Break during evaluation of the request. *) @@ -65,7 +64,7 @@ let is_known_option cmd = match cmd with (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks ~id (loc,ast) = - let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in + let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_debug ast then user_error "Debug mode not available in the IDE"; @@ -109,9 +108,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = +let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id pa; "" + Stm.query ~at:id ~route pa let annotate phrase = let (loc, ast) = @@ -178,11 +177,9 @@ let process_goal sigma g = let min_env = Environ.reset_context env in let id = Goal.uid g in let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - pr_goal_concl_style_env env sigma norm_constr + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in let process_hyp d (env,l) = - let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, (pr_compacted_decl env sigma d) :: l) in @@ -211,7 +208,7 @@ let evars () = Stm.finish (); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in + let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el @@ -341,6 +338,7 @@ let about () = { } let handle_exn (e, info) = + let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) @@ -508,4 +506,4 @@ let () = Coqtop.toploop_run := loop let () = Usage.add_to_usage "coqidetop" " --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ -\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +\n --help-XML-protocol print documentation of the Coq XML protocol\n" diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8a0e507c0b..83e5da9509 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -316,7 +316,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit let default_logger level message = let level = match level with diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 4b4ba72b0b..f06a48aebe 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,7 +67,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/interface.mli b/ide/interface.mli index 62f63aefb9..1939a8427c 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,9 +17,9 @@ type verbose = bool type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : Pp.std_ppcmds list; + goal_hyp : Pp.t list; (** List of hypotheses *) - goal_ccl : Pp.std_ppcmds; + goal_ccl : Pp.t; (** Goal conclusion *) } @@ -112,6 +112,7 @@ type coq_info = { type location = (int * int) option (* start and end of the error *) type state_id = Stateid.t +type route_id = Feedback.route_id (* Obsolete *) type edit_id = int @@ -120,7 +121,7 @@ type edit_id = int should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * Pp.std_ppcmds) + | Fail of (state_id * location * Pp.t) type ('a, 'b) union = ('a, 'b) Util.union @@ -154,8 +155,8 @@ type edit_at_rty = (unit, state_id * (state_id * state_id)) union has been deprecated in favor of sending the query answers as feedback. It will be removed in a future version of the protocol. *) -type query_sty = string * state_id -type query_rty = string +type query_sty = route_id * (string * state_id) +type query_rty = unit (** Fetching the list of current goals. Return [None] if no proof is in progress, [Some gl] otherwise. *) @@ -212,7 +213,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * Pp.std_ppcmds +type handle_exn_rty = state_id * location * Pp.t (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/minilib.mli b/ide/minilib.mli index 4517a23744..c96e59b226 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,7 @@ type level = [ (** debug printing *) val debug : bool ref -val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log_pp : ?level:level -> Pp.t -> unit val log : ?level:level -> string -> unit val coqide_config_home : unit -> string diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 93bdeb324c..664fa7fb42 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/preferences.ml b/ide/preferences.ml index 08739d013e..7c251f79c6 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -407,11 +407,15 @@ let opposite_tabs = let background_color = new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) +let attach_tag (pref : string preference) (tag : GText.tag) f = + tag#set_property (f pref#get); + pref#connect#changed ~callback:(fun c -> tag#set_property (f c)) + let attach_bg (pref : string preference) (tag : GText.tag) = - pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c)) + attach_tag pref tag (fun c -> `BACKGROUND c) let attach_fg (pref : string preference) (tag : GText.tag) = - pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c)) + attach_tag pref tag (fun c -> `FOREGROUND c) let processing_color = new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) diff --git a/ide/preferences.mli b/ide/preferences.mli index 801869d1dc..9dab43ba99 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/richpp.ml b/ide/richpp.ml index 522a3e0b31..5e176bdf14 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/richpp.mli b/ide/richpp.mli index ea4b189ba8..84adc61ca2 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -24,7 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml +val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -47,5 +47,5 @@ type richpp = Xml_datatype.xml (** Type of text with style annotations *) -val richpp_of_pp : int -> Pp.std_ppcmds -> richpp +val richpp_of_pp : int -> Pp.t -> richpp (** Extract style information from formatted text *) diff --git a/ide/sentence.ml b/ide/sentence.ml index e332682dd0..9386ac123d 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/sentence.mli b/ide/sentence.mli index feb3c0ac03..0e093a31c3 100644 --- a/ide/sentence.mli +++ b/ide/sentence.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/serialize.ml b/ide/serialize.ml index 7b568501ed..e874b9ff27 100644 --- a/ide/serialize.ml +++ b/ide/serialize.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/serialize.mli b/ide/serialize.mli index bf9e184ebb..2f18f0de24 100644 --- a/ide/serialize.mli +++ b/ide/serialize.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/session.ml b/ide/session.ml index 7aea75ac84..0a09cc9f57 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/session.mli b/ide/session.mli index 028a1f9de6..b0866ddc95 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/tags.ml b/ide/tags.ml index e4510e7af4..08ca47a842 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/tags.mli b/ide/tags.mli index 02e15a5ae4..265dfe46e3 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 5cc8cbc0d2..6a9e238797 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 621c46b94a..031af6e2a2 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index 341322be1b..f22ec96ef1 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 3bb6b780e6..f87730461f 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index dd496aa5f5..149563bb72 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index cbc34462e2..3d3a5ccb22 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,7 +19,7 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) = inherit GPack.box_skel (obj :> Gtk.box Gobject.obj) as super val but = GButton.button () - val win = GWindow.window () + val win = GWindow.window ~type_hint:`DIALOG () val frame = GBin.frame ~shadow_type:`NONE () val mutable detached = false val mutable detached_cb = (fun _ -> ()) diff --git a/ide/wg_Detachable.mli b/ide/wg_Detachable.mli index a7e8f46763..7261c1e035 100644 --- a/ide/wg_Detachable.mli +++ b/ide/wg_Detachable.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index f84b9063bf..a62ff2de58 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli index 1ef1c4d499..1055ba9164 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 3d0cd46cd4..65df2b8494 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,9 +28,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index d065fcbc80..6bd0625f0e 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,9 +18,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index 0e5284c2f9..e0979af9a1 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Notebook.mli b/ide/wg_Notebook.mli index 34eb1d11e3..01cf043a20 100644 --- a/ide/wg_Notebook.mli +++ b/ide/wg_Notebook.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 0bf5afbfdb..eccebce124 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index a90d429d04..7c33f0ae5a 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 7430f07d47..f9b9f44937 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 6cce5e5b43..29ad2615a0 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index d527a0d13a..523d41709a 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index 29cbbedacf..5ec5421f55 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml index 40ab4ce9cb..10ed3004d9 100644 --- a/ide/xml_printer.ml +++ b/ide/xml_printer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/xml_printer.mli b/ide/xml_printer.mli index f24f51fff5..f2bb2f850d 100644 --- a/ide/xml_printer.mli +++ b/ide/xml_printer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 53eb1a95ff..4b521a9682 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 = "20150913" +let protocol_version = "20170413" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -95,6 +95,13 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) +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] @@ -110,7 +117,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with +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] @@ -142,7 +149,7 @@ let rec to_pp xpp = let open Pp in let of_richpp x = Element ("richpp", [], [x]) (* Run-time Selectable *) -let of_pp (pp : Pp.std_ppcmds) = +let of_pp (pp : Pp.t) = match !msg_format with | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) | Ppcmds -> of_pp pp @@ -269,6 +276,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 @@ -304,6 +312,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 @@ -329,6 +338,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 = @@ -350,6 +360,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 @@ -373,6 +384,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 @@ -450,6 +462,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 @@ -475,6 +488,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 @@ -506,7 +520,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 @@ -528,7 +542,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 = diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 9cefab517f..d1c678b90f 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |