diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:45:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 15:47:09 +0200 |
| commit | b46020a6ea52d77b49a12e6891575b3516b8d766 (patch) | |
| tree | bf1fe9bc6d70ac44111f755dca30ed3c4d90b286 /ide | |
| parent | d02c9c566c58e566a1453827038f2b49b695c0a5 (diff) | |
| parent | decdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 2 | ||||
| -rw-r--r-- | ide/session.ml | 6 | ||||
| -rw-r--r-- | ide/texmacspp.ml | 3 |
4 files changed, 6 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index d1a799a77..450bfcdfb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -937,7 +937,6 @@ let emit_to_focus window sgn = let build_ui () = let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true ~width:window_width#get ~height:window_height#get ~title:"CoqIde" () in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4171eb20d..48fd0a93e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -104,7 +104,7 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then diff --git a/ide/session.ml b/ide/session.ml index e99833760..fc6340d28 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -108,10 +108,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -124,7 +124,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 328ddd0cd..9890a518c 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -185,7 +185,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] |