diff options
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 104 |
2 files changed, 43 insertions, 63 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 4bce3af9a..a0f192c01 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -85,7 +85,7 @@ val is_closed : coqtop -> bool val killer : (int -> unit) ref val interrupter : (int -> unit) ref -(** * Calls to Coqtop, cf [Ide_intf] for more details *) +(** * Calls to Coqtop, cf [Serialize] for more details *) val interp : handle -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value diff --git a/ide/coqide.ml b/ide/coqide.ml index dc00c063c..9108226b1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -626,38 +626,27 @@ object(self) (b#place_cursor start; self#recenter_insert) - val mutable full_goal_done = true - method show_goals handle = - if not full_goal_done then - proof_view#buffer#set_text ""; - begin - let menu_callback = if current.contextual_menus_on_goal then - (fun s () -> ignore (self#insert_this_phrase_on_success handle - true true ("progress "^s) s)) - else - (fun _ _ -> ()) in - try - begin match Coq.goals handle with - | Interface.Fail (l, str) -> - self#set_message ("Error in coqtop :\n"^str) - | Interface.Good goals -> - begin match Coq.evars handle with - | Interface.Fail (l, str) -> - self#set_message ("Error in coqtop :\n"^str) - | Interface.Good evs -> - let hints = match Coq.hints handle with - | Interface.Fail (_, _) -> None - | Interface.Good hints -> hints - in - Ideproof.display - (Ideproof.mode_tactic menu_callback) - proof_view goals hints evs - end - end - with - | e -> Minilib.log (Printexc.to_string e) - end + let menu_callback s () = + if current.contextual_menus_on_goal then + ignore (self#insert_this_phrase_on_success handle + true true ("progress "^s) s) + in + match Coq.goals handle with + | Interface.Fail (l, str) -> + self#set_message ("Error in coqtop :\n"^str) + | Interface.Good goals -> + begin match Coq.evars handle with + | Interface.Fail (l, str) -> + self#set_message ("Error in coqtop :\n"^str) + | Interface.Good evs -> + let hints = match Coq.hints handle with + | Interface.Fail (_, _) -> None + | Interface.Good hints -> hints + in + Ideproof.display (Ideproof.mode_tactic menu_callback) + proof_view goals hints evs + end method private send_to_coq handle verbose phrase show_output show_error = let display_output msg = @@ -670,10 +659,7 @@ object(self) self#insert_message s; end end in - full_goal_done <- false; Minilib.log "Send_to_coq starting now"; - (* It's important here to work with [ct] and not [!mycoqtop], otherwise - we could miss a restart of coqtop and continue sending it orders. *) match Coq.interp handle ~verbose phrase with | Interface.Fail (l,str) -> sync display_error (l,str); None | Interface.Good msg -> sync display_output msg; Some Safe @@ -688,12 +674,9 @@ object(self) flash_info "This error is so nasty that I can't even display it." else self#insert_message s; in - try - match Coq.interp handle ~raw:true ~verbose:false phrase with - | Interface.Fail (_, err) -> sync display_error err - | Interface.Good msg -> sync self#insert_message msg - with - | e -> sync display_error (Printexc.to_string e) + match Coq.interp handle ~raw:true ~verbose:false phrase with + | Interface.Fail (_, err) -> sync display_error err + | Interface.Good msg -> sync self#insert_message msg method private find_phrase_starting_at (start:GText.iter) = try @@ -916,7 +899,6 @@ object(self) (* backtrack Coq to the phrase preceding iterator [i] *) method private backtrack_to_no_lock handle i = Minilib.log "Backtracking_to iter starts now."; - full_goal_done <- false; (* pop Coq commands until we reach iterator [i] *) let rec n_step n = if Stack.is_empty cmd_stack then n else @@ -930,24 +912,23 @@ object(self) else n_step (succ n) end in - begin - try - self#do_backtrack handle (fun _ -> ()) (n_step 0); - (* We may have backtracked too much: let's replay *) - self#process_until_iter_or_error handle i - with _ -> - push_info - ("WARNING: undo failed badly.\n" ^ - "Coq might be in an inconsistent state.\n" ^ - "Please restart and report."); - end + self#do_backtrack handle (fun _ -> ()) (n_step 0); + (* We may have backtracked too much: let's replay *) + self#process_until_iter_or_error handle i method private backtrack_to handle i = - if Mutex.try_lock coq_may_stop then - (push_info "Undoing..."; - self#backtrack_to_no_lock handle i; Mutex.unlock coq_may_stop; - pop_info ()) - else Minilib.log "backtrack_to : discarded (lock is busy)" + if Mutex.try_lock coq_may_stop then begin + push_info "Undoing..."; + (* A bit hackish; may deserve a FIXME *) + let err = + try self#backtrack_to_no_lock handle i; None + with err -> Some err + in + Mutex.unlock coq_may_stop; + pop_info (); + match err with None -> () | Some e -> raise e + end else + Minilib.log "backtrack_to : discarded (lock is busy)" method go_to_insert handle = let point = self#get_insert in @@ -956,7 +937,6 @@ object(self) else self#backtrack_to handle point method undo_last_step handle = - full_goal_done <- false; if Mutex.try_lock coq_may_stop then (push_info "Undoing last step..."; (try @@ -1830,13 +1810,13 @@ let main files = ~callback:(fun _ -> do_if_active (fun handle a -> a#tactic_wizard handle [s]) ()) in let query_callback command _ = let word = get_current_word () in + let term = session_notebook#current_term in + let f query handle = term.analyzed_view#raw_coq_query handle query in if not (word = "") then - let term = session_notebook#current_term in let query = command ^ " " ^ word ^ "." in term.message_view#buffer#set_text ""; - Coq.try_grab term.toplvl - (fun handle -> term.analyzed_view#raw_coq_query handle query) - ignore + try Coq.try_grab term.toplvl (f query) ignore + with e -> term.message_view#buffer#set_text (Printexc.to_string e) in let query_shortcut s accel = GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s) |