From 2834cf72add1459d7460e3c1757e7352a1ff7466 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:34:19 +0200 Subject: Extending the grammar for CoqIDE preferences so as to match trunk. --- ide/config_lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 87cc6d06e7..3671535680 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -17,7 +17,7 @@ let space = [' ' '\010' '\013' '\009' '\012'] let char = ['A'-'Z' 'a'-'z' '_' '0'-'9'] -let ident = char+ +let ident = (char | '.')+ let ignore = space | ('#' [^ '\n']*) rule prefs m = parse -- cgit v1.2.3 From 490160d25d3caac1d2ea5beebbbebc959b1b3832 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 7 Jun 2015 14:39:18 +0200 Subject: Fixing bug #2498: Coqide navigation preferences delayed effect. --- ide/preferences.ml | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index c59642d3a7..1bd9f587c7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -711,38 +711,61 @@ let configure ?(apply=(fun () -> ())) () = ~f:(fun s -> current.project_file_name <- s) current.project_file_name in + let update_modifiers prefix mds = + let change ~path ~key ~modi ~changed = + if CString.is_sub prefix path 0 then + ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path) + in + GtkData.AccelMap.foreach change + in let help_string = "restart to apply" in let the_valid_mod = str_to_mod_list current.modifiers_valid in let modifier_for_tactics = + let cb l = + current.modifier_for_tactics <- mod_list_to_str l; + update_modifiers "/Tactics/" l + in modifiers ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l) + ~f:cb ~help:help_string "Modifiers for Tactics Menu" (str_to_mod_list current.modifier_for_tactics) in let modifier_for_templates = + let cb l = + current.modifier_for_templates <- mod_list_to_str l; + update_modifiers "/Templates/" l + in modifiers ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l) + ~f:cb ~help:help_string "Modifiers for Templates Menu" (str_to_mod_list current.modifier_for_templates) in let modifier_for_navigation = + let cb l = + current.modifier_for_navigation <- mod_list_to_str l; + update_modifiers "/Navigation/" l + in modifiers ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l) + ~f:cb ~help:help_string "Modifiers for Navigation Menu" (str_to_mod_list current.modifier_for_navigation) in let modifier_for_display = + let cb l = + current.modifier_for_display <- mod_list_to_str l; + update_modifiers "/View/" l + in modifiers ~allow:the_valid_mod - ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l) + ~f:cb ~help:help_string "Modifiers for View Menu" (str_to_mod_list current.modifier_for_display) -- cgit v1.2.3 From 42ab65d7c7eed4f6696dacedceaf7c695e0d06d6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Sep 2015 16:56:42 +0200 Subject: Removing a warning in CoqOps. --- ide/coqOps.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index c6d3149475..ba9ab9672e 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -204,7 +204,7 @@ object(self) let on_changed (i, f) = segment#add i (flags_to_color f) in let on_push s = set_index s document_length; - (SentenceId.connect s)#changed on_changed; + ignore ((SentenceId.connect s)#changed on_changed); document_length <- succ document_length; segment#set_length document_length; let flags = List.map mem_flag_of_flag s.flags in -- cgit v1.2.3 From 06d1ad739b952febce3220c372aa2dedf18e1c79 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Aug 2015 23:30:16 +0200 Subject: Adding a tag preference --- ide/preferences.ml | 152 ++++++++++++++++++++++++++++++++++++++++++++++++++++ ide/preferences.mli | 10 ++++ 2 files changed, 162 insertions(+) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 765dc7e59f..aea00d98de 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -17,6 +17,14 @@ let style_manager = GSourceView2.source_style_scheme_manager ~default:true let () = style_manager#set_search_path ((Minilib.coqide_data_dirs ())@style_manager#search_path) +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} + (** Generic preferences *) type obj = { @@ -170,6 +178,30 @@ object | _ -> None end +let tag : tag repr = +let _to s = if s = "" then None else Some s in +let _of = function None -> "" | Some s -> s in +object + method from tag = [ + _of tag.tag_fg_color; + _of tag.tag_bg_color; + string_of_bool tag.tag_bold; + string_of_bool tag.tag_italic; + string_of_bool tag.tag_underline; + ] + method into = function + | [fg; bg; bd; it; ul] -> + (try Some { + tag_fg_color = _to fg; + tag_bg_color = _to bg; + tag_bold = bool_of_string bd; + tag_italic = bool_of_string it; + tag_underline = bool_of_string ul; + } + with _ -> None) + | _ -> None +end + end let get_config_file name = @@ -354,6 +386,18 @@ let processing_color = let _ = attach_bg processing_color Tags.Script.to_process let _ = attach_bg processing_color Tags.Script.incomplete +let default_tag = { + tag_fg_color = None; + tag_bg_color = None; + tag_bold = false; + tag_italic = false; + tag_underline = false; +} + +let tags = ref Util.String.Map.empty + +let list_tags () = !tags + let processed_color = new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string) @@ -400,6 +444,74 @@ let highlight_current_line = let nanoPG = new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) +class tag_button (box : Gtk.box Gtk.obj) = +object (self) + + inherit GObj.widget box + + val fg_color = GButton.color_button () + val fg_unset = GButton.toggle_button () + val bg_color = GButton.color_button () + val bg_unset = GButton.toggle_button () + val bold = GButton.toggle_button () + val italic = GButton.toggle_button () + val underline = GButton.toggle_button () + + method set_tag tag = + let track c but set = match c with + | None -> set#set_active true + | Some c -> + set#set_active false; + but#set_color (Tags.color_of_string c) + in + track tag.tag_bg_color bg_color bg_unset; + track tag.tag_fg_color fg_color fg_unset; + bold#set_active tag.tag_bold; + italic#set_active tag.tag_italic; + underline#set_active tag.tag_underline; + + method tag = + let get but set = + if set#active then None + else Some (Tags.string_of_color but#color) + in + { + tag_bg_color = get bg_color bg_unset; + tag_fg_color = get fg_color fg_unset; + tag_bold = bold#active; + tag_italic = italic#active; + tag_underline = underline#active; + } + + initializer + let box = new GPack.box box in + let set_stock button stock = + let stock = GMisc.image ~stock ~icon_size:`BUTTON () in + button#set_image stock#coerce + in + set_stock fg_unset `CANCEL; + set_stock bg_unset `CANCEL; + set_stock bold `BOLD; + set_stock italic `ITALIC; + set_stock underline `UNDERLINE; + box#pack fg_color#coerce; + box#pack fg_unset#coerce; + box#pack bg_color#coerce; + box#pack bg_unset#coerce; + box#pack bold#coerce; + box#pack italic#coerce; + box#pack underline#coerce; + let cb but obj = obj#set_sensitive (not but#active) in + let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in + let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in + () + +end + +let tag_button () = + let box = GPack.hbox () in + new tag_button (Gobject.unsafe_cast box#as_widget) + (** Old style preferences *) let save_pref () = @@ -503,6 +615,44 @@ let configure ?(apply=(fun () -> ())) () = custom ~label box callback true in + let config_tags = + let box = GPack.vbox () in + let scroll = GBin.scrolled_window + ~hpolicy:`NEVER + ~vpolicy:`AUTOMATIC + ~packing:(box#pack ~expand:true) + () + in + let table = GPack.table + ~row_spacings:5 + ~col_spacings:5 + ~border_width:2 + ~packing:scroll#add_with_viewport () + in + let reset_button = GButton.button + ~label:"Reset" + ~packing:box#pack () + in + let i = ref 0 in + let cb = ref [] in + let iter text tag = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) () + in + let () = label#set_xalign 0. in + let button = tag_button () in + let callback () = tag#set button#tag in + button#set_tag tag#get; + table#attach ~left:1 ~top:!i button#coerce; + incr i; + cb := callback :: !cb; + in + let () = Util.String.Map.iter iter !tags in + let label = "Tag configuration" in + let callback () = List.iter (fun f -> f ()) !cb in + custom ~label box callback true + in + let config_editor = let label = "Editor configuration" in let box = GPack.vbox () in @@ -706,6 +856,8 @@ let configure ?(apply=(fun () -> ())) () = [config_font]); Section("Colors", Some `SELECT_COLOR, [config_color; source_language; source_style]); + Section("Tags", Some `SELECT_COLOR, + [config_tags]); Section("Editor", Some `EDIT, [config_editor]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; diff --git a/ide/preferences.mli b/ide/preferences.mli index d815c01ddf..b5c7ea2221 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -12,6 +12,14 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} + class type ['a] repr = object method into : string list -> 'a option @@ -33,6 +41,8 @@ object method default : 'a end +val list_tags : unit -> tag preference Util.String.Map.t + val cmd_coqtop : string option preference val cmd_coqc : string preference val cmd_make : string preference -- cgit v1.2.3 From 05fc256eecfea634d8c726c5b7f81269a87eca18 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 18:07:23 +0200 Subject: Adding standard printing tags to CoqIDE. --- ide/preferences.ml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index aea00d98de..743f6e2a62 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -398,6 +398,29 @@ let tags = ref Util.String.Map.empty let list_tags () = !tags +let () = + let iter name = + let pref = new preference ~name:[name] ~init:default_tag ~repr:Repr.(tag) in + tags := Util.String.Map.add name pref !tags + in + List.iter iter [ + "constr.evar"; + "constr.keyword"; + "constr.notation"; + "constr.path"; + "constr.reference"; + "constr.type"; + "constr.variable"; + "message.debug"; + "message.error"; + "message.warning"; + "module.definition"; + "module.keyword"; + "tactic.keyword"; + "tactic.primitive"; + "tactic.string"; + ] + let processed_color = new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string) -- cgit v1.2.3 From 8b609e4e6df906dc16e8fa506a71046ab3b8f16c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 18:09:48 +0200 Subject: Pluging in tag preferences into buffer printing. --- ide/ideutils.ml | 18 ++++++++++++++++++ ide/preferences.ml | 38 ++++++++++++++++++++++++++++++++++---- 2 files changed, 52 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 053bba805d..88a8486f47 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,7 +37,25 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) +module StringMap = Map.Make(String) +let translate s = s + +let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml = + let open Xml_datatype in + let tag name = + let name = translate name in + match GtkText.TagTable.lookup buf#tag_table name with + | None -> raise Not_found + | Some tag -> new GText.tag tag + in + let rec insert tags = function + | PCData s -> buf#insert ~tags:(List.rev tags) s + | Element (t, _, children) -> + let tags = try tag t :: tags with Not_found -> tags in + List.iter (fun xml -> insert tags xml) children + in + insert tags xml let set_location = ref (function s -> failwith "not ready") diff --git a/ide/preferences.ml b/ide/preferences.ml index 743f6e2a62..dedd62902c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -398,11 +398,41 @@ let tags = ref Util.String.Map.empty let list_tags () = !tags -let () = - let iter name = - let pref = new preference ~name:[name] ~init:default_tag ~repr:Repr.(tag) in - tags := Util.String.Map.add name pref !tags +let create_tag name default = + let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in + let set_tag tag = + begin match pref#get.tag_bg_color with + | None -> () + | Some c -> tag#set_property (`BACKGROUND c) + end; + begin match pref#get.tag_fg_color with + | None -> () + | Some c -> tag#set_property (`FOREGROUND c) + end; + begin match pref#get.tag_bold with + | false -> () + | true -> tag#set_property (`WEIGHT `BOLD) + end; + begin match pref#get.tag_italic with + | false -> () + | true -> tag#set_property (`STYLE `ITALIC) + end; + begin match pref#get.tag_underline with + | false -> () + | true -> tag#set_property (`UNDERLINE `SINGLE) + end; + in + let iter table = + let tag = GText.tag ~name () in + table#add tag#as_tag; + pref#connect#changed (fun _ -> set_tag tag); + set_tag tag; in + List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; + tags := Util.String.Map.add name pref !tags + +let () = + let iter name = create_tag name default_tag in List.iter iter [ "constr.evar"; "constr.keyword"; -- cgit v1.2.3 From 481d2b681463d2758fec6b2417631491be69f216 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Sep 2015 16:29:48 +0200 Subject: Do not canonicalize messages received by CoqIDE. --- ide/coq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index d061df6fd0..8392b7dbf4 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -336,7 +336,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let lex = Lexing.from_string s in let p = Xml_parser.make (Xml_parser.SLexbuf lex) in let rec loop () = - let xml = Xml_parser.parse p in + let xml = Xml_parser.parse ~do_not_canonicalize:true p in let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; -- cgit v1.2.3 From f4584f8a332c9077844e227c8b86d3cb1daf8b12 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 14 Sep 2015 16:40:28 +0200 Subject: Adding rich printing primitives. --- ide/coqOps.ml | 8 ++++++++ ide/ideutils.ml | 6 ++---- ide/ideutils.mli | 3 +++ ide/interface.mli | 1 + 4 files changed, 14 insertions(+), 4 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index e97a2eceef..6a7c2e8195 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -164,6 +164,14 @@ let flags_to_color f = else if List.mem `INCOMPLETE f then `NAME "gray" else `NAME Preferences.processed_color#get +let validate s = + let open Xml_datatype in + let rec validate = function + | PCData s -> Glib.Utf8.validate s + | Element (_, _, children) -> List.for_all validate children + in + validate (Richpp.repr s) + module Doc = Document class coqops diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 88a8486f47..25cb89be3c 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,11 +37,9 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) -module StringMap = Map.Make(String) - let translate s = s -let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml = +let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = let name = translate name in @@ -55,7 +53,7 @@ let insert_xml ?(tags = []) (buf : #GText.buffer_skel) xml = let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in - insert tags xml + insert tags (Richpp.repr msg) let set_location = ref (function s -> failwith "not ready") diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 1fb30e4d72..ea4c41ff0a 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,6 +52,9 @@ val pop_info : unit -> unit val clear_info : unit -> unit val flash_info : ?delay:int -> string -> unit +val insert_xml : ?tags:GText.tag list -> + #GText.buffer_skel -> Richpp.richpp -> unit + val set_location : (string -> unit) ref (* In win32, when a command-line is to be executed via cmd.exe diff --git a/ide/interface.mli b/ide/interface.mli index 464e851f6d..9d19f1c3c5 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,6 +12,7 @@ type raw = bool type verbose = bool +type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { -- cgit v1.2.3 From 85fca507c6c4810d0858d6fbd8f5a1ece52e755c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 20:16:07 +0200 Subject: Rich printing of goals. --- ide/ide_slave.ml | 5 +++-- ide/interface.mli | 4 ++-- ide/wg_ProofView.ml | 27 ++++++++++++++++----------- ide/xmlprotocol.ml | 15 +++++++-------- 4 files changed, 28 insertions(+), 23 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 94f9c9a361..562de45620 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -184,12 +184,13 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in + Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) + in let process_hyp d (env,l) = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in (List.fold_right Environ.push_named d' env, - (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in + (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = Context.fold_named_list_context process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in diff --git a/ide/interface.mli b/ide/interface.mli index 9d19f1c3c5..848fb817d4 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -18,9 +18,9 @@ type richpp = Richpp.richpp type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : string list; + goal_hyp : richpp list; (** List of hypotheses *) - goal_ccl : string; + goal_ccl : richpp; (** Goal conclusion *) } diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 6402789ec3..148add6e9c 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -8,6 +8,7 @@ open Util open Preferences +open Ideutils class type proof_view = object @@ -83,7 +84,8 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = hook_tag_cb tag hint sel_cb on_hover in [tag], hints in - let () = proof#buffer#insert ~tags (hyp ^ "\n") in + let () = insert_xml ~tags proof#buffer hyp in + proof#buffer#insert "\n"; insert_hyp rem_hints hs in let () = proof#buffer#insert head_str in @@ -96,13 +98,14 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with else [] in proof#buffer#insert (goal_str 1 goals_cnt); - proof#buffer#insert ~tags cur_goal; + insert_xml proof#buffer cur_goal; proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = proof#buffer#insert (goal_str i goals_cnt); - proof#buffer#insert (g ^ "\n") + insert_xml proof#buffer g; + proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -116,10 +119,12 @@ let mode_cesar (proof : #GText.view_skel) = function | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ -> proof#buffer#insert " *** Declarative Mode ***\n"; List.iter - (fun hyp -> proof#buffer#insert (hyp^"\n")) + (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n") hyps; proof#buffer#insert "______________________________________\n"; - proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); + proof#buffer#insert "thesis := \n "; + insert_xml proof#buffer cur_goal; + proof#buffer#insert "\n"; ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) let rec flatten = function @@ -152,8 +157,8 @@ let display mode (view : #GText.view_skel) goals hints evars = (* The proof is finished, with the exception of given up goals. *) view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iter iter given_up_goals; view#buffer#insert "\nYou need to go back and solve them." @@ -161,8 +166,8 @@ let display mode (view : #GText.view_skel) goals hints evars = (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iter iter shelved_goals | _, _, _, _ -> @@ -174,8 +179,8 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iteri iter bg end diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d337a911d8..8afe1cd56e 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 = "20150815" (** * Interface of calls to Coq by CoqIde *) @@ -131,14 +131,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 +318,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) = -- cgit v1.2.3 From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- ide/coq.ml | 12 ++++++------ ide/coqOps.ml | 28 ++++++++++++++-------------- ide/coqide.ml | 32 ++++++++++++++++---------------- ide/ide_slave.ml | 6 +++--- ide/ideutils.ml | 15 +++++++++++++-- ide/ideutils.mli | 6 ++++-- ide/wg_Command.ml | 5 ++++- ide/wg_MessageView.ml | 22 +++++++++++++++------- ide/wg_MessageView.mli | 9 +++++---- ide/xmlprotocol.ml | 2 +- 10 files changed, 81 insertions(+), 56 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 8392b7dbf4..a60f327b4f 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -302,13 +302,13 @@ let handle_intermediate_message handle xml = let logger = match handle.waiting_for with | Some (_, l) -> l | None -> function - | Pp.Error -> Minilib.log ~level:`ERROR - | Pp.Info -> Minilib.log ~level:`INFO - | Pp.Notice -> Minilib.log ~level:`NOTICE - | Pp.Warning -> Minilib.log ~level:`WARNING - | Pp.Debug _ -> Minilib.log ~level:`DEBUG + | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) + | Pp.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) + | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) + | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) + | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) in - logger level content + logger level (Richpp.richpp_of_xml content) let handle_feedback feedback_processor xml = let feedback = Feedback.to_feedback xml in diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6a7c2e8195..80a32cc65b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -329,14 +329,14 @@ object(self) let display_error s = if not (Glib.Utf8.validate s) then flash_info "This error is so nasty that I can't even display it." - else messages#add s; + else messages#add_string s; in let query = Coq.query ~logger:messages#push (phrase,Stateid.dummy) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> - messages#add msg; Coq.return () + messages#add_string msg; Coq.return () in Coq.bind (Coq.seq action query) next @@ -564,7 +564,7 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error "You muse close the proof with Qed or Admitted"; + logger Pp.Error (Richpp.richpp_of_string "You muse close the proof with Qed or Admitted"); self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> @@ -580,7 +580,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Pp.Notice msg; + logger Pp.Notice (Richpp.richpp_of_string msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -588,13 +588,13 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Pp.Notice msg; + logger Pp.Notice (Richpp.richpp_of_string msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) | Fail (id, loc, msg) -> let sentence = Doc.pop document in - self#process_interp_error queue sentence loc msg tip id in + self#process_interp_error queue sentence loc (Richpp.richpp_of_string msg) tip id in Coq.bind coq_query handle_answer in let tip = @@ -607,7 +607,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Pp.Info "All proof terms checked by the kernel"; + messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -701,8 +701,8 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Pp.Error "Fixme LOC"; - messages#push Pp.Error msg; + if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC"); + messages#push Pp.Error (Richpp.richpp_of_string msg); if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -720,7 +720,7 @@ object(self) ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = messages#clear; - messages#push Pp.Error msg; + messages#push Pp.Error (Richpp.richpp_of_string msg); ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else @@ -779,7 +779,7 @@ object(self) let display_error (loc, s) = if not (Glib.Utf8.validate s) then flash_info "This error is so nasty that I can't even display it." - else messages#add s + else messages#add_string s in let try_phrase phrase stop more = let action = log "Sending to coq now" in @@ -787,10 +787,10 @@ object(self) let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add ("Unsuccessfully tried: "^phrase); + messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase)); more | Good msg -> - messages#add msg; + messages#add_string msg; stop Tags.Script.processed in Coq.bind (Coq.seq action query) next @@ -834,7 +834,7 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return () + | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return () | Good id -> initial_state <- id; Coq.return () in Coq.bind (Coq.init (get_filename ())) next in Coq.seq get_initial_state Coq.PrintOpt.enforce diff --git a/ide/coqide.ml b/ide/coqide.ml index 6769ce768b..e591f205f9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -318,10 +318,10 @@ let export kind sn = local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1" in - sn.messages#set ("Running: "^cmd); + sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); let finally st = flash_info (cmd ^ pr_exit_status st) in - run_command sn.messages#add finally cmd + run_command (fun msg -> sn.messages#add_string msg) finally cmd let export kind = cb_on_current_term (export kind) @@ -431,9 +431,9 @@ let compile sn = ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in - sn.messages#set ("Running: "^cmd); + sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); let display s = - sn.messages#add s; + sn.messages#add_string s; Buffer.add_string buf s in let finally st = @@ -441,8 +441,8 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#set "Compilation output:\n"; - sn.messages#add (Buffer.contents buf); + sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); + sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf)); end in run_command display finally cmd @@ -464,13 +464,13 @@ let make sn = |Some f -> File.saveall (); let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in - sn.messages#set "Compilation output:\n"; + sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); Buffer.reset last_make_buf; last_make := ""; last_make_index := 0; last_make_dir := Filename.dirname f; let display s = - sn.messages#add s; + sn.messages#add_string s; Buffer.add_string last_make_buf s in let finally st = flash_info (cmd_make#get ^ pr_exit_status st) @@ -508,11 +508,11 @@ let next_error sn = let stopi = b#get_iter_at_byte ~line:(line-1) stop in b#apply_tag Tags.Script.error ~start:starti ~stop:stopi; b#place_cursor ~where:starti; - sn.messages#set error_msg; + sn.messages#set (Richpp.richpp_of_string error_msg); sn.script#misc#grab_focus () with Not_found -> last_make_index := 0; - sn.messages#set "No more errors.\n" + sn.messages#set (Richpp.richpp_of_string "No more errors.\n") let next_error = cb_on_current_term next_error @@ -718,7 +718,7 @@ let initial_about () = else "" in let msg = initial_string ^ version_info ^ log_file_message () in - on_current_term (fun term -> term.messages#add msg) + on_current_term (fun term -> term.messages#add_string msg) let coq_icon () = (* May raise Nof_found *) @@ -783,7 +783,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Pp.Error msg + sn.messages#push Pp.Error (Richpp.richpp_of_string msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in @@ -1140,17 +1140,17 @@ let build_ui () = item "Help" ~label:"_Help"; item "Browse Coq Manual" ~label:"Browse Coq _Manual" ~callback:(fun _ -> - browse notebook#current_term.messages#add (doc_url ())); + browse notebook#current_term.messages#add_string (doc_url ())); item "Browse Coq Library" ~label:"Browse Coq _Library" ~callback:(fun _ -> - browse notebook#current_term.messages#add library_url#get); + browse notebook#current_term.messages#add_string library_url#get); item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> - browse_keyword sn.messages#add (get_current_word sn))); + browse_keyword sn.messages#add_string (get_current_word sn))); item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> sn.messages#clear; - sn.messages#add (NanoPG.get_documentation ()))); + sn.messages#add_string (NanoPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 562de45620..414c360246 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -429,12 +429,12 @@ let print_xml = let slave_logger xml_oc level message = (* convert the message into XML *) - let msg = string_of_ppcmds (hov 0 message) in + let msg = hov 0 message in let message = { Pp.message_level = level; - Pp.message_content = msg; + Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); } in - let () = pr_debug (Printf.sprintf "-> %S" msg) in + let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in let xml = Pp.of_message message in print_xml xml_oc xml diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 25cb89be3c..2e4adba735 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,6 +37,17 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) +let xml_to_string xml = + let open Xml_datatype in + let buf = Buffer.create 1024 in + let rec iter = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, children) -> + List.iter iter children + in + let () = iter (Richpp.repr xml) in + Buffer.contents buf + let translate s = s let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = @@ -288,7 +299,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 = Pp.message_level -> string -> unit +type logger = Pp.message_level -> Richpp.richpp -> unit let default_logger level message = let level = match level with @@ -298,7 +309,7 @@ let default_logger level message = | Pp.Warning -> `WARNING | Pp.Error -> `ERROR in - Minilib.log ~level message + Minilib.log ~level (xml_to_string message) (** {6 File operations} *) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index ea4c41ff0a..db2dce5a39 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,6 +52,8 @@ val pop_info : unit -> unit val clear_info : unit -> unit val flash_info : ?delay:int -> string -> unit +val xml_to_string : Richpp.richpp -> string + val insert_xml : ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit @@ -67,9 +69,9 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Pp.message_level -> string -> unit +type logger = Pp.message_level -> Richpp.richpp -> unit -val default_logger : Pp.message_level -> string -> unit +val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) (** {6 I/O operations} *) diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 163bd28b13..0ae57ee748 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -100,7 +100,10 @@ object(self) if Str.string_match (Str.regexp "\\. *$") com 0 then com else com ^ " " ^ arg ^" . " in - let log level message = result#buffer#insert (message^"\n") in + let log level message = + Ideutils.insert_xml result#buffer message; + result#buffer#insert "\n"; + in let process = Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 30bb48e3f3..615e989de9 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -12,7 +12,7 @@ class type message_view_signals = object inherit GObj.misc_signals inherit GUtil.add_ml_signals - method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id + method pushed : callback:Ideutils.logger -> GtkSignal.id end class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals = @@ -28,9 +28,10 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : string -> unit - method set : string -> unit - method push : Pp.message_level -> string -> unit + method add : Richpp.richpp -> unit + method add_string : string -> unit + method set : Richpp.richpp -> unit + method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) @@ -76,14 +77,21 @@ let message_view () : message_view = | Pp.Warning -> [Tags.Message.warning] | _ -> [] in - if msg <> "" then begin - buffer#insert ~tags msg; - buffer#insert ~tags "\n"; + let rec non_empty = function + | Xml_datatype.PCData "" -> false + | Xml_datatype.PCData _ -> true + | Xml_datatype.Element (_, _, children) -> List.exists non_empty children + in + if non_empty (Richpp.repr msg) then begin + Ideutils.insert_xml buffer ~tags msg; + buffer#insert (*~tags*) "\n"; push#call (level, msg) end method add msg = self#push Pp.Notice msg + method add_string s = self#add (Richpp.richpp_of_string s) + method set msg = self#clear; self#add msg method buffer = text_buffer diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 457ece0900..388ab259fd 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -10,7 +10,7 @@ class type message_view_signals = object inherit GObj.misc_signals inherit GUtil.add_ml_signals - method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id + method pushed : callback:Ideutils.logger -> GtkSignal.id end class type message_view = @@ -18,9 +18,10 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : string -> unit - method set : string -> unit - method push : Pp.message_level -> string -> unit + method add : Richpp.richpp -> unit + method add_string : string -> unit + method set : Richpp.richpp -> unit + method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 8afe1cd56e..46e5d6f370 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20150815" +let protocol_version = "20150821" (** * Interface of calls to Coq by CoqIde *) -- cgit v1.2.3 From 002cd2e8f6ae5722e72a5db136cda7414f9218d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Sep 2015 17:19:18 +0200 Subject: Rich printing of CoqIDE protocol failure. --- ide/coqOps.ml | 14 +++++++------- ide/ide_slave.ml | 10 +++++++--- ide/interface.mli | 4 ++-- ide/wg_Command.ml | 2 +- ide/xmlprotocol.ml | 15 ++++++++------- 5 files changed, 25 insertions(+), 20 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 80a32cc65b..8bfc70b63f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -327,9 +327,9 @@ object(self) method raw_coq_query phrase = let action = log "raw_coq_query starting now" in let display_error s = - if not (Glib.Utf8.validate s) then + if not (validate s) then flash_info "This error is so nasty that I can't even display it." - else messages#add_string s; + else messages#add s; in let query = Coq.query ~logger:messages#push (phrase,Stateid.dummy) in @@ -594,7 +594,7 @@ object(self) else loop tip (List.rev topstack) | Fail (id, loc, msg) -> let sentence = Doc.pop document in - self#process_interp_error queue sentence loc (Richpp.richpp_of_string msg) tip id in + self#process_interp_error queue sentence loc msg tip id in Coq.bind coq_query handle_answer in let tip = @@ -702,7 +702,7 @@ object(self) conclusion () | Fail (safe_id, loc, msg) -> if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC"); - messages#push Pp.Error (Richpp.richpp_of_string msg); + messages#push Pp.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -720,7 +720,7 @@ object(self) ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = messages#clear; - messages#push Pp.Error (Richpp.richpp_of_string msg); + messages#push Pp.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else @@ -777,9 +777,9 @@ object(self) self#show_goals in let display_error (loc, s) = - if not (Glib.Utf8.validate s) then + if not (validate s) then flash_info "This error is so nasty that I can't even display it." - else messages#add_string s + else messages#add s in let try_phrase phrase stop more = let action = log "Sending to coq now" in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 414c360246..c28ed68605 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -330,10 +330,14 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in - let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in + let mk_msg () = + let msg = read_stdout () in + let msg = str msg ++ fnl () ++ Errors.print ~info e in + Richpp.richpp_of_pp msg + in match e with - | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" + | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" + | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () diff --git a/ide/interface.mli b/ide/interface.mli index 848fb817d4..f3777ba36c 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -118,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * string) + | Fail of (state_id * location * richpp) type ('a, 'b) union = ('a, 'b) Util.union @@ -202,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * string +type handle_exn_rty = state_id * location * richpp (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 0ae57ee748..7d8993aa8b 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -107,7 +107,7 @@ object(self) let process = Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - result#buffer#insert str; + Ideutils.insert_xml result#buffer str; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 46e5d6f370..7445ce5ca0 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20150821" +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 @@ -671,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) @@ -730,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: *) -- cgit v1.2.3 From 0ac3a2f4de0dc02b973c9f5d59b3c0a97f888141 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 21 Sep 2015 10:35:56 +0200 Subject: Change the default modifiers for navigation. (Fix bug #4295) On most systems (including Windows, according to the bug report), shortcuts Ctrl+Alt+Arrows are preempted by the window manager by default. So don't use them for navigation in Coqide by default. Note that this change only has an impact when installing on a fresh system; it won't change anything for existing users. --- ide/preferences.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 1bd9f587c7..90862d0647 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -190,7 +190,7 @@ let current = { automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; - modifier_for_navigation = ""; + modifier_for_navigation = ""; modifier_for_templates = ""; modifier_for_tactics = ""; modifier_for_display = ""; -- cgit v1.2.3 From 8a031dc29abf1e16b2ee78322a7221b8b5c19a33 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Sep 2015 08:23:36 +0200 Subject: Fixing unsetting of CoqIDE tags. --- ide/preferences.ml | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index dedd62902c..313d97086f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -402,24 +402,34 @@ let create_tag name default = let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in let set_tag tag = begin match pref#get.tag_bg_color with - | None -> () - | Some c -> tag#set_property (`BACKGROUND c) + | None -> tag#set_property (`BACKGROUND_SET false) + | Some c -> + tag#set_property (`BACKGROUND_SET true); + tag#set_property (`BACKGROUND c) end; begin match pref#get.tag_fg_color with - | None -> () - | Some c -> tag#set_property (`FOREGROUND c) + | None -> tag#set_property (`FOREGROUND_SET false) + | Some c -> + tag#set_property (`FOREGROUND_SET true); + tag#set_property (`FOREGROUND c) end; begin match pref#get.tag_bold with - | false -> () - | true -> tag#set_property (`WEIGHT `BOLD) + | false -> tag#set_property (`WEIGHT_SET false) + | true -> + tag#set_property (`WEIGHT_SET true); + tag#set_property (`WEIGHT `BOLD) end; begin match pref#get.tag_italic with - | false -> () - | true -> tag#set_property (`STYLE `ITALIC) + | false -> tag#set_property (`STYLE_SET false) + | true -> + tag#set_property (`STYLE_SET true); + tag#set_property (`STYLE `ITALIC) end; begin match pref#get.tag_underline with - | false -> () - | true -> tag#set_property (`UNDERLINE `SINGLE) + | false -> tag#set_property (`UNDERLINE_SET false) + | true -> + tag#set_property (`UNDERLINE_SET true); + tag#set_property (`UNDERLINE `SINGLE) end; in let iter table = -- cgit v1.2.3 From 39b2c31fed01073a4308e2e85d8a53ccecde73e7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 16:45:30 +0200 Subject: Use default GTK styles for CoqIDE tags. --- ide/preferences.ml | 40 ++++++++++++++++++++++++---------------- 1 file changed, 24 insertions(+), 16 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 23426cad65..a605014f2c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -398,6 +398,14 @@ let tags = ref Util.String.Map.empty let list_tags () = !tags +let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = { + tag_fg_color = fg; + tag_bg_color = bg; + tag_bold = bold; + tag_italic = italic; + tag_underline = underline; +} + let create_tag name default = let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in let set_tag tag = @@ -442,23 +450,23 @@ let create_tag name default = tags := Util.String.Map.add name pref !tags let () = - let iter name = create_tag name default_tag in + let iter (name, tag) = create_tag name tag in List.iter iter [ - "constr.evar"; - "constr.keyword"; - "constr.notation"; - "constr.path"; - "constr.reference"; - "constr.type"; - "constr.variable"; - "message.debug"; - "message.error"; - "message.warning"; - "module.definition"; - "module.keyword"; - "tactic.keyword"; - "tactic.primitive"; - "tactic.string"; + ("constr.evar", make_tag ()); + ("constr.keyword", make_tag ~fg:"dark green" ()); + ("constr.notation", make_tag ()); + ("constr.path", make_tag ()); + ("constr.reference", make_tag ~fg:"navy"()); + ("constr.type", make_tag ~fg:"#008080" ()); + ("constr.variable", make_tag ()); + ("message.debug", make_tag ()); + ("message.error", make_tag ()); + ("message.warning", make_tag ()); + ("module.definition", make_tag ~fg:"orange red" ~bold:true ()); + ("module.keyword", make_tag ()); + ("tactic.keyword", make_tag ()); + ("tactic.primitive", make_tag ()); + ("tactic.string", make_tag ()); ] let processed_color = -- cgit v1.2.3 From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2015 14:11:19 +0200 Subject: Goptions: new value type: optional string These options can be set to a string value, but also unset. Internal data is of type string option. --- ide/ide_slave.ml | 4 ++++ ide/interface.mli | 1 + ide/xmlprotocol.ml | 4 ++++ 3 files changed, 9 insertions(+) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 94f9c9a361..041f2f83b8 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -291,11 +291,13 @@ let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b | Goptions.IntValue x -> Interface.IntValue x | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s let import_option_value = function | Interface.BoolValue b -> Goptions.BoolValue b | Interface.IntValue x -> Goptions.IntValue x | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s let export_option_state s = { Interface.opt_sync = s.Goptions.opt_sync; @@ -314,6 +316,8 @@ let set_options options = | BoolValue b -> Goptions.set_bool_option_value name b | IntValue i -> Goptions.set_int_option_value name i | StringValue s -> Goptions.set_string_option_value name s + | StringOptValue (Some s) -> Goptions.set_string_option_value name s + | StringOptValue None -> Goptions.unset_option_value_gen None name in List.iter iter options diff --git a/ide/interface.mli b/ide/interface.mli index 464e851f6d..767c49d2bd 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -61,6 +61,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d337a911d8..84fd8929bd 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -62,10 +62,12 @@ let of_option_value = function | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] | StringValue s -> constructor "option_value" "stringvalue" [of_string s] + | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s] let to_option_value = do_match "option_value" (fun s args -> match s with | "intvalue" -> IntValue (to_option to_int (singleton args)) | "boolvalue" -> BoolValue (to_bool (singleton args)) | "stringvalue" -> StringValue (to_string (singleton args)) + | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) | _ -> raise Marshal_error) let of_option_state s = @@ -337,6 +339,8 @@ end = struct | IntValue None -> "none" | IntValue (Some i) -> string_of_int i | StringValue s -> s + | StringOptValue None -> "none" + | StringOptValue (Some s) -> s | BoolValue b -> if b then "true" else "false" let pr_option_state (s : option_state) = Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- ide/coq.mli | 6 +++--- ide/coqide.ml | 4 ++-- ide/utf8_convert.mll | 2 +- ide/wg_ScriptView.ml | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) (limited to 'ide') diff --git a/ide/coq.mli b/ide/coq.mli index a72c67b43e..2dc5ad3078 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -16,7 +16,7 @@ type coqtop Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly, this module is responsible for relaunching the whole process. The reset handler set through [set_reset_handler] will be called after such an - abrupt failure. It is also called when explicitely requesting coqtop to + abrupt failure. It is also called when explicitly requesting coqtop to reset. *) type 'a task @@ -29,7 +29,7 @@ type 'a task ([is_computing] will answer [true]), and any other task submission will be rejected by [try_grab]. - Any exception occuring within the task will trigger a coqtop reset. + Any exception occurring within the task will trigger a coqtop reset. Beware, because of the GTK scheduler, you never know when a task will actually be executed. If you need to sequentialize imperative actions, you @@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task (** Monadic binding of tasks *) val lift : (unit -> 'a) -> 'a task -(** Return the impertative computation waiting to be processed. *) +(** Return the imperative computation waiting to be processed. *) val seq : unit task -> 'a task -> 'a task (** Sequential composition *) diff --git a/ide/coqide.ml b/ide/coqide.ml index c0e2281258..f15e5fa34a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1125,10 +1125,10 @@ let build_ui () = ~accel:(prefs.modifier_for_navigation^"h");*) item "Previous" ~label:"_Previous" ~stock:`GO_BACK ~callback:Nav.previous_occ - ~tooltip:"Previous occurence" + ~tooltip:"Previous occurrence" ~accel:(prefs.modifier_for_navigation^"less"); item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ - ~tooltip:"Next occurence" + ~tooltip:"Next occurrence" ~accel:(prefs.modifier_for_navigation^"greater"); item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document ~tooltip:"Fully check the document" diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 621833ddea..4ebf9a62e1 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -12,7 +12,7 @@ } -(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) +(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) let digit = ['0'-'9''A'-'Z''a'-'z'] let short = digit digit digit digit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 8298d9954f..ae50b28377 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -139,7 +139,7 @@ object(self) (** We don't care about atomicity. Return: 1. `OK when there was no error, `FAIL otherwise - 2. `NOOP if no write occured, `WRITE otherwise + 2. `NOOP if no write occurred, `WRITE otherwise *) method private process_action = function | Insert ins -> -- cgit v1.2.3 From d0530179206ff98a327bc189139f75b83ece35ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 22 Oct 2015 15:43:52 +0200 Subject: Using GADTs in Xmlprotocol. This removes 109 Obj.magic in one patch! --- ide/ide_slave.ml | 2 +- ide/xmlprotocol.ml | 394 +++++++++++++++++++++++++++------------------------- ide/xmlprotocol.mli | 4 +- 3 files changed, 206 insertions(+), 194 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 1dcef22b91..a6c42b28c2 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -474,7 +474,7 @@ let loop () = try let xml_query = Xml_parser.parse xml_ic in (* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) - let q = Xmlprotocol.to_call xml_query in + let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in let () = pr_debug_answer q r in diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 32c39e20d4..bb6a18158d 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -221,22 +221,31 @@ module ReifType : sig end = struct - type value_type = - | Unit | String | Int | Bool | Xml - - | Option of value_type - | List of value_type - | Pair of value_type * value_type - | Union of value_type * value_type - - | Goals | Evar | State | Option_state | Option_value | Coq_info - | Coq_object of value_type - | State_id - | Search_cst - - type 'a val_t = value_type - - let erase (x : 'a val_t) : value_type = x + type _ val_t = + | Unit : unit val_t + | String : string val_t + | Int : int val_t + | Bool : bool val_t + | Xml : Xml_datatype.xml val_t + + | Option : 'a val_t -> 'a option val_t + | List : 'a val_t -> 'a list val_t + | Pair : 'a val_t * 'b val_t -> ('a * 'b) val_t + | Union : 'a val_t * 'b val_t -> ('a, 'b) union val_t + + | Goals : goals val_t + | Evar : evar val_t + | State : status val_t + | Option_state : option_state val_t + | Option_value : option_value val_t + | Coq_info : coq_info val_t + | Coq_object : 'a val_t -> 'a coq_object val_t + | State_id : state_id val_t + | Search_cst : search_constraint val_t + + type value_type = Value_type : 'a val_t -> value_type + + let erase (x : 'a val_t) = Value_type x let unit_t = Unit let string_t = String @@ -260,48 +269,48 @@ end = struct let search_cst_t = Search_cst let of_value_type (ty : 'a val_t) : 'a -> xml = - let rec convert ty : 'a -> xml = match ty with - | Unit -> Obj.magic of_unit - | Bool -> Obj.magic of_bool - | Xml -> Obj.magic (fun x -> x) - | String -> Obj.magic of_string - | Int -> Obj.magic of_int - | State -> Obj.magic of_status - | Option_state -> Obj.magic of_option_state - | Option_value -> Obj.magic of_option_value - | Coq_info -> Obj.magic of_coq_info - | Goals -> Obj.magic of_goals - | Evar -> Obj.magic of_evar - | List t -> Obj.magic (of_list (convert t)) - | Option t -> Obj.magic (of_option (convert t)) - | Coq_object t -> Obj.magic (of_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) - | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2)) - | State_id -> Obj.magic Stateid.to_xml - | Search_cst -> Obj.magic of_search_cst + let rec convert : type a. a val_t -> a -> xml = function + | Unit -> of_unit + | Bool -> of_bool + | Xml -> (fun x -> x) + | String -> of_string + | Int -> of_int + | State -> of_status + | Option_state -> of_option_state + | Option_value -> of_option_value + | Coq_info -> of_coq_info + | Goals -> of_goals + | Evar -> of_evar + | List t -> (of_list (convert t)) + | Option t -> (of_option (convert t)) + | Coq_object t -> (of_coq_object (convert t)) + | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) + | Union (t1,t2) -> (of_union (convert t1) (convert t2)) + | State_id -> Stateid.to_xml + | Search_cst -> of_search_cst in convert ty let to_value_type (ty : 'a val_t) : xml -> 'a = - let rec convert ty : xml -> 'a = match ty with - | Unit -> Obj.magic to_unit - | Bool -> Obj.magic to_bool - | Xml -> Obj.magic (fun x -> x) - | String -> Obj.magic to_string - | Int -> Obj.magic to_int - | State -> Obj.magic to_status - | Option_state -> Obj.magic to_option_state - | Option_value -> Obj.magic to_option_value - | Coq_info -> Obj.magic to_coq_info - | Goals -> Obj.magic to_goals - | Evar -> Obj.magic to_evar - | List t -> Obj.magic (to_list (convert t)) - | Option t -> Obj.magic (to_option (convert t)) - | Coq_object t -> Obj.magic (to_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) - | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2)) - | State_id -> Obj.magic Stateid.of_xml - | Search_cst -> Obj.magic to_search_cst + let rec convert : type a. a val_t -> xml -> a = function + | Unit -> to_unit + | Bool -> to_bool + | Xml -> (fun x -> x) + | String -> to_string + | Int -> to_int + | State -> to_status + | Option_state -> to_option_state + | Option_value -> to_option_value + | Coq_info -> to_coq_info + | Goals -> to_goals + | Evar -> to_evar + | List t -> (to_list (convert t)) + | Option t -> (to_option (convert t)) + | Coq_object t -> (to_coq_object (convert t)) + | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) + | Union (t1,t2) -> (to_union (convert t1) (convert t2)) + | State_id -> Stateid.of_xml + | Search_cst -> to_search_cst in convert ty @@ -350,6 +359,7 @@ end = struct let pr_coq_object (o : 'a coq_object) = "FIXME" let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x + let pr_state_id = Stateid.to_string let pr_search_cst = function | Name_Pattern s -> "Name_Pattern " ^ s @@ -358,30 +368,30 @@ end = struct | In_Module s -> "In_Module " ^ String.concat "." s | Include_Blacklist -> "Include_Blacklist" - let rec print = function - | Unit -> Obj.magic pr_unit - | Bool -> Obj.magic pr_bool - | String -> Obj.magic pr_string - | Xml -> Obj.magic Xml_printer.to_string_fmt - | Int -> Obj.magic pr_int - | State -> Obj.magic pr_status - | Option_state -> Obj.magic pr_option_state - | Option_value -> Obj.magic pr_option_value - | Search_cst -> Obj.magic pr_search_cst - | Coq_info -> Obj.magic pr_coq_info - | Goals -> Obj.magic pr_goal - | Evar -> Obj.magic pr_evar - | List t -> Obj.magic (pr_list (print t)) - | Option t -> Obj.magic (pr_option (print t)) - | Coq_object t -> Obj.magic pr_coq_object - | Pair (t1,t2) -> Obj.magic (pr_pair (print t1) (print t2)) - | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2)) - | State_id -> Obj.magic pr_int + let rec print : type a. a val_t -> a -> string = function + | Unit -> pr_unit + | Bool -> pr_bool + | String -> pr_string + | Xml -> Xml_printer.to_string_fmt + | Int -> pr_int + | State -> pr_status + | Option_state -> pr_option_state + | Option_value -> pr_option_value + | Search_cst -> pr_search_cst + | Coq_info -> pr_coq_info + | Goals -> pr_goal + | Evar -> pr_evar + | List t -> (pr_list (print t)) + | Option t -> (pr_option (print t)) + | Coq_object t -> pr_coq_object + | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) + | Union (t1,t2) -> (pr_union (print t1) (print t2)) + | State_id -> pr_state_id (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool - let rec print_type = function + let rec print_val_t : type a. a val_t -> string = function | Unit -> "unit" | Bool -> "bool" | String -> "string" @@ -394,33 +404,35 @@ end = struct | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" | Goals -> assert(true : goals exists); "Interface.goals" | Evar -> assert(true : evar exists); "Interface.evar" - | List t -> Printf.sprintf "(%s list)" (print_type t) - | Option t -> Printf.sprintf "(%s option)" (print_type t) + | List t -> Printf.sprintf "(%s list)" (print_val_t t) + | Option t -> Printf.sprintf "(%s option)" (print_val_t t) | Coq_object t -> assert(true : 'a coq_object exists); - Printf.sprintf "(%s Interface.coq_object)" (print_type t) - | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2) + Printf.sprintf "(%s Interface.coq_object)" (print_val_t t) + | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_val_t t1) (print_val_t t2) | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); - Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2) + Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" + let print_type = function Value_type ty -> print_val_t ty + let document_type_encoding pr_xml = Printf.printf "\n=== Data encoding by examples ===\n\n"; - Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ())); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool) + Printf.printf "%s:\n\n%s\n\n" (print_val_t Unit) (pr_xml (of_unit ())); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t Bool) (pr_xml (of_bool true)) (pr_xml (of_bool false)); - Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello")); - Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256)); - Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (Stateid.to_xml Stateid.initial)); - Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5])); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int)) + Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello")); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (Stateid.to_xml Stateid.initial)); + Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5])); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int)) (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); - Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int))) + Printf.printf "%s:\n\n%s\n\n" (print_val_t (Pair (Bool,Int))) (pr_xml (of_pair of_bool of_int (false,3))); - Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int))) + Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) (pr_xml (of_union of_bool of_int (Inl false))); 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_type Option_state) + Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) (pr_xml (of_option_state { opt_sync = true; opt_depr = false; opt_name = "name1"; opt_value = IntValue (Some 37) })); @@ -496,27 +508,27 @@ let calls = [| |] type 'a call = - | Add of add_sty - | Edit_at of edit_at_sty - | Query of query_sty - | Goal of goals_sty - | Evars of evars_sty - | Hints of hints_sty - | Status of status_sty - | Search of search_sty - | GetOptions of get_options_sty - | SetOptions of set_options_sty - | MkCases of mkcases_sty - | Quit of quit_sty - | About of about_sty - | Init of init_sty - | StopWorker of stop_worker_sty + | Add : add_sty -> add_rty call + | Edit_at : edit_at_sty -> edit_at_rty call + | Query : query_sty -> query_rty call + | Goal : goals_sty -> goals_rty call + | Evars : evars_sty -> evars_rty call + | Hints : hints_sty -> hints_rty call + | Status : status_sty -> status_rty call + | Search : search_sty -> search_rty call + | GetOptions : get_options_sty -> get_options_rty call + | SetOptions : set_options_sty -> set_options_rty call + | MkCases : mkcases_sty -> mkcases_rty call + | Quit : quit_sty -> quit_rty call + | About : about_sty -> about_rty call + | Init : init_sty -> init_rty call + | StopWorker : stop_worker_sty -> stop_worker_rty call (* retrocompatibility *) - | Interp of interp_sty - | PrintAst of print_ast_sty - | Annotate of annotate_sty + | Interp : interp_sty -> interp_rty call + | PrintAst : print_ast_sty -> print_ast_rty call + | Annotate : annotate_sty -> annotate_rty call -let id_of_call = function +let id_of_call : type a. a call -> int = function | Add _ -> 0 | Edit_at _ -> 1 | Query _ -> 2 @@ -538,7 +550,7 @@ let id_of_call = function let str_of_call c = pi1 calls.(id_of_call c) -type unknown +type unknown_call = Unknown : 'a call -> unknown_call (** We use phantom types and GADT to protect ourselves against wild casts *) let add x : add_rty call = Add x @@ -559,8 +571,8 @@ 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 abstract_eval_call handler (c : 'a call) : 'a value = - let mkGood x : 'a value = Good (Obj.magic x) in +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 try match c with | Add x -> mkGood (handler.add x) @@ -586,47 +598,47 @@ let abstract_eval_call handler (c : 'a call) : 'a value = Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) -let of_answer (q : 'a call) (v : 'a value) : xml = match q with - | Add _ -> of_value (of_value_type add_rty_t ) (Obj.magic v) - | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) (Obj.magic v) - | Query _ -> of_value (of_value_type query_rty_t ) (Obj.magic v) - | Goal _ -> of_value (of_value_type goals_rty_t ) (Obj.magic v) - | Evars _ -> of_value (of_value_type evars_rty_t ) (Obj.magic v) - | Hints _ -> of_value (of_value_type hints_rty_t ) (Obj.magic v) - | Status _ -> of_value (of_value_type status_rty_t ) (Obj.magic v) - | Search _ -> of_value (of_value_type search_rty_t ) (Obj.magic v) - | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v) - | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v) - | MkCases _ -> of_value (of_value_type mkcases_rty_t ) (Obj.magic v) - | Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v) - | About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v) - | Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v) - | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v) - | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v) - | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) (Obj.magic v) - | Annotate _ -> of_value (of_value_type annotate_rty_t ) (Obj.magic v) - -let to_answer (q : 'a call) (x : xml) : 'a value = match q with - | Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x) - | Edit_at _ -> Obj.magic (to_value (to_value_type edit_at_rty_t ) x) - | Query _ -> Obj.magic (to_value (to_value_type query_rty_t ) x) - | Goal _ -> Obj.magic (to_value (to_value_type goals_rty_t ) x) - | Evars _ -> Obj.magic (to_value (to_value_type evars_rty_t ) x) - | Hints _ -> Obj.magic (to_value (to_value_type hints_rty_t ) x) - | Status _ -> Obj.magic (to_value (to_value_type status_rty_t ) x) - | Search _ -> Obj.magic (to_value (to_value_type search_rty_t ) x) - | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x) - | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x) - | MkCases _ -> Obj.magic (to_value (to_value_type mkcases_rty_t ) x) - | Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x) - | About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x) - | Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x) - | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x) - | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x) - | PrintAst _ -> Obj.magic (to_value (to_value_type print_ast_rty_t ) x) - | Annotate _ -> Obj.magic (to_value (to_value_type annotate_rty_t ) x) - -let of_call (q : 'a call) : xml = +let of_answer : type a. a call -> a value -> xml = function + | Add _ -> of_value (of_value_type add_rty_t ) + | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) + | Query _ -> of_value (of_value_type query_rty_t ) + | Goal _ -> of_value (of_value_type goals_rty_t ) + | Evars _ -> of_value (of_value_type evars_rty_t ) + | Hints _ -> of_value (of_value_type hints_rty_t ) + | Status _ -> of_value (of_value_type status_rty_t ) + | Search _ -> of_value (of_value_type search_rty_t ) + | GetOptions _ -> of_value (of_value_type get_options_rty_t) + | 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 ) + | 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 ) + | 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 ) + +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 ) + | Query _ -> to_value (to_value_type query_rty_t ) + | Goal _ -> to_value (to_value_type goals_rty_t ) + | Evars _ -> to_value (to_value_type evars_rty_t ) + | Hints _ -> to_value (to_value_type hints_rty_t ) + | Status _ -> to_value (to_value_type status_rty_t ) + | Search _ -> to_value (to_value_type search_rty_t ) + | GetOptions _ -> to_value (to_value_type get_options_rty_t) + | 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 ) + | 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 ) + | 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 ) + +let of_call : type a. a call -> xml = fun q -> let mkCall x = constructor "call" (str_of_call q) [x] in match q with | Add x -> mkCall (of_value_type add_sty_t x) @@ -648,28 +660,28 @@ let of_call (q : 'a call) : xml = | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) | Annotate x -> mkCall (of_value_type annotate_sty_t x) -let to_call : xml -> unknown call = +let to_call : xml -> unknown_call = do_match "call" (fun s a -> let mkCallArg vt a = to_value_type vt (singleton a) in match s with - | "Add" -> Add (mkCallArg add_sty_t a) - | "Edit_at" -> Edit_at (mkCallArg edit_at_sty_t a) - | "Query" -> Query (mkCallArg query_sty_t a) - | "Goal" -> Goal (mkCallArg goals_sty_t a) - | "Evars" -> Evars (mkCallArg evars_sty_t a) - | "Hints" -> Hints (mkCallArg hints_sty_t a) - | "Status" -> Status (mkCallArg status_sty_t a) - | "Search" -> Search (mkCallArg search_sty_t a) - | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a) - | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a) - | "MkCases" -> MkCases (mkCallArg mkcases_sty_t a) - | "Quit" -> Quit (mkCallArg quit_sty_t a) - | "About" -> About (mkCallArg about_sty_t a) - | "Init" -> Init (mkCallArg init_sty_t a) - | "Interp" -> Interp (mkCallArg interp_sty_t a) - | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a) - | "PrintAst" -> PrintAst (mkCallArg print_ast_sty_t a) - | "Annotate" -> Annotate (mkCallArg annotate_sty_t a) + | "Add" -> Unknown (Add (mkCallArg add_sty_t a)) + | "Edit_at" -> Unknown (Edit_at (mkCallArg edit_at_sty_t a)) + | "Query" -> Unknown (Query (mkCallArg query_sty_t a)) + | "Goal" -> Unknown (Goal (mkCallArg goals_sty_t a)) + | "Evars" -> Unknown (Evars (mkCallArg evars_sty_t a)) + | "Hints" -> Unknown (Hints (mkCallArg hints_sty_t a)) + | "Status" -> Unknown (Status (mkCallArg status_sty_t a)) + | "Search" -> Unknown (Search (mkCallArg search_sty_t a)) + | "GetOptions" -> Unknown (GetOptions (mkCallArg get_options_sty_t a)) + | "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)) + | "About" -> Unknown (About (mkCallArg about_sty_t a)) + | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) + | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) + | "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)) | _ -> raise Marshal_error) (** Debug printing *) @@ -681,26 +693,26 @@ let pr_value_gen pr = function "FAIL "^Stateid.to_string id^ " ("^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) - | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) (Obj.magic value) - | Query _ -> pr_value_gen (print query_rty_t ) (Obj.magic value) - | Goal _ -> pr_value_gen (print goals_rty_t ) (Obj.magic value) - | Evars _ -> pr_value_gen (print evars_rty_t ) (Obj.magic value) - | Hints _ -> pr_value_gen (print hints_rty_t ) (Obj.magic value) - | Status _ -> pr_value_gen (print status_rty_t ) (Obj.magic value) - | Search _ -> pr_value_gen (print search_rty_t ) (Obj.magic value) - | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) - | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) - | MkCases _ -> pr_value_gen (print mkcases_rty_t ) (Obj.magic value) - | Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value) - | About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value) - | Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value) - | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value) - | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value) - | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) (Obj.magic value) - | Annotate _ -> pr_value_gen (print annotate_rty_t ) (Obj.magic value) -let pr_call call = +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 + | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) value + | Query _ -> pr_value_gen (print query_rty_t ) value + | Goal _ -> pr_value_gen (print goals_rty_t ) value + | Evars _ -> pr_value_gen (print evars_rty_t ) value + | Hints _ -> pr_value_gen (print hints_rty_t ) value + | Status _ -> pr_value_gen (print status_rty_t ) value + | Search _ -> pr_value_gen (print search_rty_t ) value + | GetOptions _ -> pr_value_gen (print get_options_rty_t) value + | 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 + | 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 + | 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 +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 | Add x -> return add_sty_t x diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 2c8ebc655a..7806550d1c 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -13,7 +13,7 @@ open Xml_datatype type 'a call -type unknown +type unknown_call = Unknown : 'a call -> unknown_call val add : add_sty -> add_rty call val edit_at : edit_at_sty -> edit_at_rty call @@ -43,7 +43,7 @@ val protocol_version : string (** * XML data marshalling *) val of_call : 'a call -> xml -val to_call : xml -> unknown call +val to_call : xml -> unknown_call val of_answer : 'a call -> 'a value -> xml val to_answer : 'a call -> xml -> 'a value -- cgit v1.2.3 From 8d99e4bf4c54e9eabb0910740f79375ff399b844 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 30 Oct 2015 16:10:33 +0100 Subject: Fix typo. --- ide/coqOps.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index ba9ab9672e..c7e0810fdc 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -559,7 +559,7 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error "You muse close the proof with Qed or Admitted"; + logger Pp.Error "You must close the proof with Qed or Admitted"; self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> -- cgit v1.2.3 From 469cb750c6c1aa46f77b2a89a36f79f29aa97073 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 14 Dec 2015 13:33:47 +0100 Subject: Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk 2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the fix to trunk instead. This reverts commits: 490160d25d3caac1d2ea5beebbbebc959b1b3832. ef8718a7fd3bcd960d954093d8c636525e6cc492. 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d. 901a9b29adf507370732aeafbfea6718c1842f1b. --- ide/preferences.ml | 31 ++++--------------------------- 1 file changed, 4 insertions(+), 27 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 90862d0647..01ce454834 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -711,61 +711,38 @@ let configure ?(apply=(fun () -> ())) () = ~f:(fun s -> current.project_file_name <- s) current.project_file_name in - let update_modifiers prefix mds = - let change ~path ~key ~modi ~changed = - if CString.is_sub prefix path 0 then - ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path) - in - GtkData.AccelMap.foreach change - in let help_string = "restart to apply" in let the_valid_mod = str_to_mod_list current.modifiers_valid in let modifier_for_tactics = - let cb l = - current.modifier_for_tactics <- mod_list_to_str l; - update_modifiers "/Tactics/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l) ~help:help_string "Modifiers for Tactics Menu" (str_to_mod_list current.modifier_for_tactics) in let modifier_for_templates = - let cb l = - current.modifier_for_templates <- mod_list_to_str l; - update_modifiers "/Templates/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l) ~help:help_string "Modifiers for Templates Menu" (str_to_mod_list current.modifier_for_templates) in let modifier_for_navigation = - let cb l = - current.modifier_for_navigation <- mod_list_to_str l; - update_modifiers "/Navigation/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l) ~help:help_string "Modifiers for Navigation Menu" (str_to_mod_list current.modifier_for_navigation) in let modifier_for_display = - let cb l = - current.modifier_for_display <- mod_list_to_str l; - update_modifiers "/View/" l - in modifiers ~allow:the_valid_mod - ~f:cb + ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l) ~help:help_string "Modifiers for View Menu" (str_to_mod_list current.modifier_for_display) -- cgit v1.2.3 From fa08993b9330623c8cb259ac8ebff93ecce9c2f6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Dec 2015 14:04:12 +0100 Subject: CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message --- ide/preferences.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 01ce454834..8988dbc60b 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -754,6 +754,13 @@ let configure ?(apply=(fun () -> ())) () = "Allowed modifiers" the_valid_mod in + let modifier_notice = + let b = GPack.hbox () in + let _lbl = + GMisc.label ~markup:"You need to restart CoqIDE after changing these settings" + ~packing:b#add () in + custom b (fun () -> ()) true + in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo @@ -855,7 +862,7 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; modifier_notice]); Section("Misc", Some `ADD, misc)] in -- cgit v1.2.3 From 2ab8455cffef4097a441eb6befaa29f6f3076824 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:25:15 +0200 Subject: Fixing little bug of coq_makefile with unterminated comment. Force failing when reaching end of file with unterminated comment when parsing Make (project) file. --- ide/project_file.ml4 | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f7279f9cfe..152f76cc0e 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,6 +28,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) + | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s -- cgit v1.2.3 From 1b5d54b58f4ecea66ef9bf439d23b115d2c77050 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:29:11 +0100 Subject: Remove unplugged button from the interface. --- ide/preferences.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index a605014f2c..3d11e94feb 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -700,10 +700,6 @@ let configure ?(apply=(fun () -> ())) () = ~border_width:2 ~packing:scroll#add_with_viewport () in - let reset_button = GButton.button - ~label:"Reset" - ~packing:box#pack () - in let i = ref 0 in let cb = ref [] in let iter text tag = -- cgit v1.2.3 From d5b1807e65f7ea29d435c3f894aa551370c5989f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:47:59 +0100 Subject: Fix typos. --- ide/FAQ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/FAQ b/ide/FAQ index 07b818246a..c8b0a5d328 100644 --- a/ide/FAQ +++ b/ide/FAQ @@ -1,7 +1,7 @@ CoqIde FAQ Q0) What is CoqIde? -R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations. +R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations. Q1) How to enable Emacs keybindings? R1: Insert -- cgit v1.2.3 From 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:50:02 +0100 Subject: Remove useless rec flags. --- ide/sentence.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/sentence.ml b/ide/sentence.ml index dd6b10a461..8195051c6c 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -63,13 +63,13 @@ let grab_sentence_start (iter:GText.iter) soi = (** Search forward the first character immediately after a sentence end *) -let rec grab_sentence_stop (start:GText.iter) = +let grab_sentence_stop (start:GText.iter) = (forward_search is_sentence_end start)#forward_char (** Search forward the first character immediately after a "." sentence end (and not just a "\{" or "\}" or comment end *) -let rec grab_ending_dot (start:GText.iter) = +let grab_ending_dot (start:GText.iter) = let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in (forward_search is_ending_dot start)#forward_char -- cgit v1.2.3 From 82ac0604888679bc2fbdeda9ac264d7cd10f7928 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:52:33 +0100 Subject: Avoid warnings about loop indices. --- ide/document.ml | 2 +- ide/ideutils.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/document.ml b/ide/document.ml index 9823e7576c..41d5a7564b 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -154,7 +154,7 @@ let cut_at d id = if stateid_opt_equal state_id (Some id) then CSig.Stop (n, zone) else CSig.Cont (n + 1, data :: zone) in let n, zone = CList.fold_left_until aux (0, []) d.stack in - for i = 1 to n do ignore(pop d) done; + for _i = 1 to n do ignore(pop d) done; List.rev zone let find_id d f = diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 2e4adba735..ffa07ead7e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -31,7 +31,7 @@ let push_info,pop_info,clear_info = let size = ref 0 in (fun s -> incr size; ignore (status_context#push s)), (fun () -> decr size; status_context#pop ()), - (fun () -> for i = 1 to !size do status_context#pop () done; size := 0) + (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0) let flash_info = let flash_context = status#new_context ~name:"Flash" in -- cgit v1.2.3 From 74c29764359272b29af081b30762549777ae8825 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:05:03 +0100 Subject: Remove some useless type declarations. --- ide/ideutils.ml | 2 -- ide/wg_Find.ml | 2 -- 2 files changed, 4 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ffa07ead7e..51ae76ff54 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -9,8 +9,6 @@ open Preferences -exception Forbidden - let warn_image () = let img = GMisc.image () in img#set_stock `DIALOG_WARNING; diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index a0949ca0c8..dc7071c278 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type mode = [ `FIND | `REPLACE ] - let b2c = Ideutils.byte_offset_to_char_offset class finder name (view : GText.view) = -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- ide/coq.ml | 5 ----- ide/document.ml | 6 ------ ide/wg_ProofView.ml | 13 ------------- 3 files changed, 24 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index a60f327b4f..268a95a336 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines = "Command was: "^cmd^"\n"^ "Answer was: "^(String.concat "\n " lines)) -let check_remaining_opt arg = - if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg) - let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in @@ -200,8 +197,6 @@ module GlibMainLoop = struct let read_all = Ideutils.io_read_all let async_chan_of_file fd = Glib.Io.channel_of_descr fd let async_chan_of_socket s = !gio_channel_of_descr_socket s - let add_timeout ~sec callback = - ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback) end module CoqTop = Spawn.Async(GlibMainLoop) diff --git a/ide/document.ml b/ide/document.ml index 41d5a7564b..bb431e7914 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -124,12 +124,6 @@ let context d = let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in List.map (flat pair true) top, List.map (flat pair true) bot -let iter d f = - let a, s, b = to_lists d in - List.iter (flat f false) a; - List.iter (flat f true) s; - List.iter (flat f false) b - let stateid_opt_equal = Option.equal Stateid.equal let is_in_focus d id = diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 148add6e9c..642a577878 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -114,19 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with (Some Tags.Proof.goal))); ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) -let mode_cesar (proof : #GText.view_skel) = function - | [] -> assert false - | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ -> - proof#buffer#insert " *** Declarative Mode ***\n"; - List.iter - (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n") - hyps; - proof#buffer#insert "______________________________________\n"; - proof#buffer#insert "thesis := \n "; - insert_xml proof#buffer cur_goal; - proof#buffer#insert "\n"; - ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) - let rec flatten = function | [] -> [] | (lg, rg) :: l -> -- cgit v1.2.3 From 8b5d02d8706f99015c2ce8efcad32b7af228dd53 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 6 Jan 2016 11:32:31 +0100 Subject: Prevent coq_makefile from parsing project files in the reverse order. (Fix bug #4477) The bug was a bit subtle. Function process_cmd_line can be called in three different ways: 1. tail-recursively to accumulate parsed options in reverse order, 2. directly to parse a file (coqide) or a command line (coq_makefile), 3. recursively to handle a "-f" option. Once its execution finished, the function reversed its accumulator so that the parsed options are in correct order. Due to the third case, this means that the final local order of options was depending on the parity of the depth of "-f" options. This commit fixes it by changing the function so that the recursive call gets the actual accumulator rather than its reversed version. Warning: this will break all the projects that were inadvertently (or not) relying on the bug. This might also require a further commit if coq_makefile itself was relying on the bug. --- ide/project_file.ml4 | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 152f76cc0e..07ab5344d2 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -48,7 +48,7 @@ let parse f = res let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts,List.rev l + | [] -> opts, l | ("-h"|"--help") :: _ -> raise Parsing_error | ("-no-opt"|"-byte") :: r -> @@ -128,6 +128,10 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) else if (Filename.check_suffix f ".mlpack") then MLPACK f else Subdir f) :: l) r +let process_cmd_line orig_dir opts l args = + let (opts, l) = process_cmd_line orig_dir opts l args in + opts, List.rev l + let rec post_canonize f = if Filename.basename f = Filename.current_dir_name then let dir = Filename.dirname f in -- cgit v1.2.3 From d0d46d9c5a93de25ecf0202a0ab3dbd83f1ed693 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 6 Jan 2016 14:49:31 +0100 Subject: Make code more readable by not mixing list traversal and option processing. --- ide/project_file.ml4 | 80 +++++++++++++++++++++++++--------------------------- 1 file changed, 38 insertions(+), 42 deletions(-) (limited to 'ide') diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 07ab5344d2..f66fd31c20 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -139,48 +139,44 @@ let rec post_canonize f = else f (* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) -let split_arguments = - let rec aux = function - | V n :: r -> - let (v,m,o,s),i,d = aux r in ((CUnix.remove_path_dot n::v,m,o,s),i,d) - | ML n :: r -> - let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) - | MLI n :: r -> - let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) - | ML4 n :: r -> - let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) - | MLLIB n :: r -> - let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) - | MLPACK n :: r -> - let (v,(mli,ml4,ml,mllib,mlpack),o,s),i,d = aux r in - ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) - | Special (n,dep,is_phony,c) :: r -> - let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,is_phony,c)::o,s),i,d) - | Subdir n :: r -> - let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d) - | MLInclude p :: r -> - let t,(ml,q,r),d = aux r in (t,((CUnix.remove_path_dot (post_canonize p), - CUnix.canonical_path_name p)::ml,q,r),d) - | Include (p,l) :: r -> - let t,(ml,i,r),d = aux r in - let i_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml,i_new::i,r),d) - | RInclude (p,l) :: r -> - let t,(ml,i,r),d = aux r in - let r_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml,i,r_new::r),d) - | Def (v,def) :: r -> - let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs)) - | Arg a :: r -> - let t,i,(args,defs) = aux r in (t,i,(a::args,defs)) - | [] -> ([],([],[],[],[],[]),[],[]),([],[],[]),([],[]) - in aux +let split_arguments args = + List.fold_right + (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), + (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> + match a with + | V n -> + ((CUnix.remove_path_dot n::v,m,o,s),i,d) + | ML n -> + ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) + | MLI n -> + ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) + | ML4 n -> + ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) + | MLLIB n -> + ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) + | MLPACK n -> + ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) + | Special (n,dep,is_phony,c) -> + ((v,m,(n,dep,is_phony,c)::o,s),i,d) + | Subdir n -> + ((v,m,o,n::s),i,d) + | MLInclude p -> + let ml_new = (CUnix.remove_path_dot (post_canonize p), + CUnix.canonical_path_name p) in + (t,(ml_new::ml_inc,q_inc,r_inc),d) + | Include (p,l) -> + let q_new = (CUnix.remove_path_dot (post_canonize p),l, + CUnix.canonical_path_name p) in + (t,(ml_inc,q_new::q_inc,r_inc),d) + | RInclude (p,l) -> + let r_new = (CUnix.remove_path_dot (post_canonize p),l, + CUnix.canonical_path_name p) in + (t,(ml_inc,q_inc,r_new::r_inc),d) + | Def (v,def) -> + (t,i,(args,(v,def)::defs)) + | Arg a -> + (t,i,(a::args,defs))) + args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) let read_project_file f = split_arguments -- cgit v1.2.3 From 6599e31f04b6e8980de72e9d3913b70c04b6698c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 6 Jan 2016 15:08:08 +0100 Subject: Remove deprecated command-line options such as "-as". --- ide/project_file.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f66fd31c20..081094e2b6 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -86,7 +86,6 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r | "-I" :: d :: r -> process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: "-as" :: lp :: r | "-R" :: p :: lp :: r -> process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- ide/ide_slave.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index a6c42b28c2..d8b8bd4610 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -187,12 +187,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in + let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = - Context.fold_named_list_context process_hyp + Context.NamedList.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- ide/MacOS/Info.plist.template | 2 +- ide/config_lexer.mll | 2 +- ide/coq.ml | 2 +- ide/coq.mli | 2 +- ide/coqOps.ml | 2 +- ide/coqOps.mli | 2 +- ide/coq_commands.ml | 2 +- ide/coq_lex.mll | 2 +- ide/coqide.ml | 2 +- ide/coqide.mli | 2 +- ide/coqide_main.ml4 | 2 +- ide/fileOps.ml | 2 +- ide/fileOps.mli | 2 +- ide/gtk_parsing.ml | 2 +- ide/ide_slave.ml | 2 +- ide/ideutils.ml | 2 +- ide/ideutils.mli | 2 +- ide/interface.mli | 2 +- ide/nanoPG.ml | 2 +- ide/preferences.ml | 2 +- ide/preferences.mli | 2 +- ide/sentence.ml | 2 +- ide/sentence.mli | 2 +- ide/session.ml | 2 +- ide/session.mli | 2 +- ide/tags.ml | 2 +- ide/tags.mli | 2 +- ide/utf8_convert.mll | 2 +- ide/wg_Command.ml | 2 +- ide/wg_Command.mli | 2 +- ide/wg_Completion.ml | 2 +- ide/wg_Completion.mli | 2 +- ide/wg_Detachable.ml | 2 +- ide/wg_Detachable.mli | 2 +- ide/wg_Find.ml | 2 +- ide/wg_Find.mli | 2 +- ide/wg_MessageView.ml | 2 +- ide/wg_MessageView.mli | 2 +- ide/wg_Notebook.ml | 2 +- ide/wg_Notebook.mli | 2 +- ide/wg_ProofView.ml | 2 +- ide/wg_ProofView.mli | 2 +- ide/wg_ScriptView.ml | 2 +- ide/wg_ScriptView.mli | 2 +- ide/wg_Segment.ml | 2 +- ide/wg_Segment.mli | 2 +- ide/xmlprotocol.ml | 2 +- ide/xmlprotocol.mli | 2 +- 48 files changed, 48 insertions(+), 48 deletions(-) (limited to 'ide') diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template index e224e81204..fbe7773dd4 100644 --- a/ide/MacOS/Info.plist.template +++ b/ide/MacOS/Info.plist.template @@ -66,7 +66,7 @@ CFBundleGetInfoString Coq_vVERSION NSHumanReadableCopyright - Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS + Copyright 1999-2016, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS CFBundleHelpBookFolder share/doc/coq/html/ CFAppleHelpAnchor diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 3671535680..ac9cc57bc0 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- ide/ide_slave.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 20cf48d7f8..12ef0e0751 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -130,7 +130,8 @@ let annotate phrase = (** Goal display *) -let hyp_next_tac sigma env (id,_,ast) = +let hyp_next_tac sigma env decl = + let (id,_,ast) = Context.Named.Declaration.to_tuple decl in let id_s = Names.Id.to_string id in let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ @@ -187,8 +188,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in - let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in + let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in + let d' = List.map (fun name -> let open Context.Named.Declaration in + match pi2 d with + | None -> LocalAssum (name, pi3 d) + | Some value -> LocalDef (name, value, pi3 d)) + (pi1 d) in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = -- cgit v1.2.3 From 37479c1b59b7492abb5c89a42c5a76d4cd9d48cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Feb 2016 19:13:40 +0100 Subject: CoqIDE: STOP button also stops workers (fix #4542) --- ide/coq.ml | 15 +++++++++++---- ide/coq.mli | 4 ++-- ide/coqide.ml | 2 +- ide/session.ml | 3 +++ ide/session.mli | 1 + 5 files changed, 18 insertions(+), 7 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 98576a9811..7edae47ca1 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -465,10 +465,6 @@ let close_coqtop coqtop = let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop -let break_coqtop coqtop = - try !interrupter (CoqTop.unixpid coqtop.handle.proc) - with _ -> Minilib.log "Error while sending Ctrl-C" - let get_arguments coqtop = coqtop.sup_args let set_arguments coqtop args = @@ -518,6 +514,17 @@ 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 break_coqtop coqtop workers = + if coqtop.status = Busy then + try !interrupter (CoqTop.unixpid coqtop.handle.proc) + with _ -> Minilib.log "Error while sending Ctrl-C" + else + let rec aux = function + | [] -> Void + | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws) + in + let Void = aux workers in () + module PrintOpt = struct type t = string list diff --git a/ide/coq.mli b/ide/coq.mli index d9eda0f342..7cef6a4d0a 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit (** Finish initializing a freshly spawned coqtop, by running a first task on it. The task should run its inner continuation at the end. *) -val break_coqtop : coqtop -> unit -(** Interrupt the current computation of coqtop. *) +val break_coqtop : coqtop -> string list -> unit +(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *) val close_coqtop : coqtop -> unit (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 608cf82ff8..36aab30e60 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -574,7 +574,7 @@ module Nav = struct let restart _ = on_current_term restart let interrupt sn = Minilib.log "User break received"; - Coq.break_coqtop sn.coqtop + Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data)) let interrupt = cb_on_current_term interrupt let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end diff --git a/ide/session.ml b/ide/session.ml index 34c533b8e5..168ddd4df9 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -19,6 +19,7 @@ class type ['a] page = method update : 'a -> unit method on_update : callback:('a -> unit) -> unit method refresh_color : unit -> unit + method data : 'a end class type control = @@ -321,6 +322,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = end method on_update ~callback:cb = callback := cb method refresh_color () = refresh () + method data = !last_update end let create_jobpage coqtop coqops : jobpage = @@ -361,6 +363,7 @@ let create_jobpage coqtop coqops : jobpage = end method on_update ~callback:cb = callback := cb method refresh_color () = refresh () + method data = !last_update end let create_proof () = diff --git a/ide/session.mli b/ide/session.mli index 0881e40392..ef39ab2e0d 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -15,6 +15,7 @@ class type ['a] page = method update : 'a -> unit method on_update : callback:('a -> unit) -> unit method refresh_color : unit -> unit + method data : 'a end class type control = -- cgit v1.2.3 From e54d014ce10dea4a74b66e5091d25e4b26bd71fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 20:17:24 +0100 Subject: Fixing bug #4540: CoqIDE bottom progress bar does not update. --- ide/coqOps.ml | 67 +++++++++++++++++++++++++-------- ide/document.ml | 27 +++++++++----- ide/document.mli | 4 +- ide/wg_Segment.ml | 106 ++++++++++++++++++++--------------------------------- ide/wg_Segment.mli | 14 +++++-- 5 files changed, 119 insertions(+), 99 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 89f4e513ed..58f5eda62e 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -169,6 +169,55 @@ let flags_to_color f = module Doc = Document +let segment_model (doc : sentence Doc.document) : Wg_Segment.model = +object (self) + + val mutable cbs = [] + + val mutable document_length = 0 + + method length = document_length + + method changed ~callback = cbs <- callback :: cbs + + method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu -> + let fold accu _ _ s = + let flags = List.map mem_flag_of_flag s.flags in + f accu (flags_to_color flags) + in + Doc.fold_all doc accu fold + + method private on_changed (i, f) = + let data = (i, flags_to_color f) in + List.iter (fun f -> f (`SET data)) cbs + + method private on_push s ctx = + let after = match ctx with + | None -> [] + | Some (l, _) -> l + in + List.iter (fun s -> set_index s (s.index + 1)) after; + set_index s (document_length - List.length after); + ignore ((SentenceId.connect s)#changed self#on_changed); + document_length <- document_length + 1; + List.iter (fun f -> f `INSERT) cbs + + method private on_pop s ctx = + let () = match ctx with + | None -> () + | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l + in + set_index s (-1); + document_length <- document_length - 1; + List.iter (fun f -> f `REMOVE) cbs + + initializer + let _ = (Doc.connect doc)#pushed self#on_push in + let _ = (Doc.connect doc)#popped self#on_pop in + () + +end + class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) @@ -201,20 +250,8 @@ object(self) script#misc#set_has_tooltip true; ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback); feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback; - let on_changed (i, f) = segment#add i (flags_to_color f) in - let on_push s = - set_index s document_length; - ignore ((SentenceId.connect s)#changed on_changed); - document_length <- succ document_length; - segment#set_length document_length; - let flags = List.map mem_flag_of_flag s.flags in - segment#add s.index (flags_to_color flags); - in - let on_pop s = - set_index s (-1); - document_length <- pred document_length; - segment#set_length document_length; - in + let md = segment_model document in + segment#set_model md; let on_click id = let find _ _ s = Int.equal s.index id in let sentence = Doc.find document find in @@ -230,8 +267,6 @@ object(self) script#buffer#place_cursor iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in - let _ = (Doc.connect document)#pushed on_push in - let _ = (Doc.connect document)#popped on_pop in let _ = segment#connect#clicked on_click in () diff --git a/ide/document.ml b/ide/document.ml index 9823e7576c..6566ee3f81 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -16,8 +16,8 @@ type id = Stateid.t class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end class ['a] signal () = @@ -32,14 +32,14 @@ end type 'a document = { mutable stack : 'a sentence list; mutable context : ('a sentence list * 'a sentence list) option; - pushed_sig : 'a signal; - popped_sig : 'a signal; + pushed_sig : ('a * ('a list * 'a list) option) signal; + popped_sig : ('a * ('a list * 'a list) option) signal; } -let connect d = +let connect d : 'a signals = object - method pushed ~callback = d.pushed_sig#connect callback - method popped ~callback = d.popped_sig#connect callback + method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx) + method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx) end let create () = { @@ -49,6 +49,12 @@ let create () = { popped_sig = new signal (); } +let repr_context s = match s.context with +| None -> None +| Some (cl, cr) -> + let map s = s.data in + Some (List.map map cl, List.map map cr) + (* Invariant, only the tip is a allowed to have state_id = None *) let invariant l = l = [] || (List.hd l).state_id <> None @@ -64,12 +70,13 @@ let tip_data = function let push d x = assert(invariant d.stack); d.stack <- { data = x; state_id = None } :: d.stack; - d.pushed_sig#call x + d.pushed_sig#call (x, repr_context d) let pop = function | { stack = [] } -> raise Empty - | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data - + | { stack = { data }::xs } as s -> + s.stack <- xs; s.popped_sig#call (data, repr_context s); data + let focus d ~cond_top:c_start ~cond_bot:c_stop = assert(invariant d.stack); if d.context <> None then invalid_arg "focus"; diff --git a/ide/document.mli b/ide/document.mli index 0d803ff003..fb96cb6d76 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -108,8 +108,8 @@ val print : class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end val connect : 'a document -> 'a signals diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index b4b02a7fa2..47fdeb127b 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -10,53 +10,13 @@ open Util type color = GDraw.color -module Segment : -sig - type +'a t - val length : 'a t -> int - val resize : 'a t -> int -> 'a t - val empty : 'a t - val add : int -> 'a -> 'a t -> 'a t - val remove : int -> 'a t -> 'a t - val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b -end = -struct - type 'a t = { - length : int; - content : 'a Int.Map.t; - } - - let empty = { length = 0; content = Int.Map.empty } - - let length s = s.length - - let resize s len = - if s.length <= len then { s with length = len } - else - let filter i v = i < len in - { length = len; content = Int.Map.filter filter s.content } - - let add i v s = - if i < s.length then - { s with content = Int.Map.add i v s.content } - else s - - let remove i s = { s with content = Int.Map.remove i s.content } - - let fold eq f s accu = - let make k v (cur, accu) = match cur with - | None -> Some (k, k, v), accu - | Some (i, j, w) -> - if k = j + 1 && eq v w then Some (i, k, w), accu - else Some (k, k, v), (i, j, w) :: accu - in - let p, segments = Int.Map.fold make s.content (None, []) in - let segments = match p with - | None -> segments - | Some p -> p :: segments - in - List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a end let i2f = float_of_int @@ -95,7 +55,7 @@ object (self) val mutable width = 1 val mutable height = 20 - val mutable data = Segment.empty + val mutable model : model option = None val mutable default : color = `WHITE val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 () val clicked = new GUtil.signal () @@ -113,10 +73,12 @@ object (self) end in let _ = box#misc#connect#size_allocate cb in - let clicked_cb ev = + let clicked_cb ev = match model with + | None -> true + | Some md -> let x = GdkEvent.Button.x ev in let (width, _) = pixmap#size in - let len = Segment.length data in + let len = md#length in let idx = f2i ((x *. i2f len) /. i2f width) in let () = clicked#call idx in true @@ -125,17 +87,23 @@ object (self) (** Initial pixmap *) draw#set_pixmap pixmap - method length = Segment.length data - - method set_length len = - data <- Segment.resize data len; - if self#misc#visible then self#refresh () + method set_model md = + model <- Some md; + let changed_cb = function + | `INSERT | `REMOVE -> + if self#misc#visible then self#refresh () + | `SET (i, color) -> + if self#misc#visible then self#fill_range color i (i + 1) + in + md#changed changed_cb - method private fill_range color i j = + method private fill_range color i j = match model with + | None -> () + | Some md -> let i = i2f i in let j = i2f j in let width = i2f width in - let len = i2f (Segment.length data) in + let len = i2f md#length in let x = f2i ((i *. width) /. len) in let x' = f2i ((j *. width) /. len) in let w = x' - x in @@ -143,14 +111,6 @@ object (self) pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true (); draw#set_mask None; - method add i color = - data <- Segment.add i color data; - if self#misc#visible then self#fill_range color i (i + 1) - - method remove i = - data <- Segment.remove i data; - if self#misc#visible then self#fill_range default i (i + 1) - method set_default_color color = default <- color method default_color = default @@ -159,11 +119,23 @@ object (self) draw#set_pixmap pixmap; self#refresh (); - method private refresh () = + method private refresh () = match model with + | None -> () + | Some md -> pixmap#set_foreground default; pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true (); - let fold i j v () = self#fill_range v i (j + 1) in - Segment.fold color_eq fold data (); + let make (k, cur, accu) v = match cur with + | None -> pred k, Some (k, k, v), accu + | Some (i, j, w) -> + if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu + else pred k, Some (k, k, v), (i, j, w) :: accu + in + let _, p, segments = md#fold make (md#length - 1, None, []) in + let segments = match p with + | None -> segments + | Some p -> p :: segments + in + List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments; draw#set_mask None; method connect = diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index 0fc8ebd75e..29cbbedacf 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -8,6 +8,8 @@ type color = GDraw.color +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] + class type segment_signals = object inherit GObj.misc_signals @@ -15,15 +17,19 @@ object method clicked : callback:(int -> unit) -> GtkSignal.id end +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method set_model : model -> unit method connect : segment_signals - method length : int - method set_length : int -> unit method default_color : color method set_default_color : color -> unit - method add : int -> color -> unit - method remove : int -> unit end -- cgit v1.2.3 From e5b40d615d0ed9819f6ac8345ed924d8a501172e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 19:47:49 +0100 Subject: CoqIDE is more resilient to initialization errors. We force the STM to finish after the initialization request so as to raise exceptions that may have been generated by the initialization process. Likewise, we simply die when the initialization request fails in CoqIDE instead of just printing an error message. This is the fix for the underlying issue of bug #4591, but it does not solve the bug yet. --- ide/coqOps.ml | 5 ++++- ide/ide_slave.ml | 1 + 2 files changed, 5 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 58f5eda62e..850b41e596 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -864,7 +864,10 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return () + | Fail (_, _, message) -> + let message = "Couldn't initialize coqtop\n\n" ^ message in + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in + ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; Coq.return () in Coq.bind (Coq.init (get_filename ())) next in Coq.seq get_initial_state Coq.PrintOpt.enforce diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bd98fe16e3..2e6a361c66 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -361,6 +361,7 @@ let init = 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in Stm.set_compilation_hints file; + Stm.finish (); initial_id end -- cgit v1.2.3