diff options
| -rw-r--r-- | ide/coq.ml | 61 | ||||
| -rw-r--r-- | ide/coq.mli | 20 | ||||
| -rw-r--r-- | ide/coqOps.ml | 74 | ||||
| -rw-r--r-- | ide/coqOps.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 54 | ||||
| -rw-r--r-- | ide/session.ml | 130 | ||||
| -rw-r--r-- | ide/session.mli | 5 |
7 files changed, 188 insertions, 158 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 553e3da16..78e917bdb 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -518,10 +518,8 @@ module PrintOpt = struct type t = string list - let width_ref = ref None - let set_printing_width w = width_ref := Some w + (* Boolean options *) - let width = ["Printing"; "Width"] let implicit = ["Printing"; "Implicit"] let coercions = ["Printing"; "Coercions"] let raw_matching = ["Printing"; "Matching"] @@ -530,29 +528,56 @@ struct let existential = ["Printing"; "Existential"; "Instances"] let universes = ["Printing"; "Universes"] - let state_hack = Hashtbl.create 11 - let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false) - [ implicit; coercions; raw_matching; notations; - all_basic; existential; universes ] + type bool_descr = { opts : t list; init : bool; label : string } + + let bool_items = [ + { opts = [implicit]; init = false; label = "Display _implicit arguments" }; + { opts = [coercions]; init = false; label = "Display _coercions" }; + { opts = [raw_matching]; init = true; + label = "Display raw _matching expressions" }; + { opts = [notations]; init = true; label = "Display _notations" }; + { opts = [all_basic]; init = false; + label = "Display _all basic low-level contents" }; + { opts = [existential]; init = false; + label = "Display _existential variable instances" }; + { opts = [universes]; init = false; label = "Display _universe levels" }; + { opts = [all_basic;existential;universes]; init = false; + label = "Display all _low-level contents" } + ] + + (** The current status of the boolean options *) + + let current_state = Hashtbl.create 11 + + let set opt v = Hashtbl.replace current_state opt v + + let reset () = + let init_descr d = List.iter (fun o -> set o d.init) d.opts in + List.iter init_descr bool_items + + let _ = reset () - let set opts h k = - List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) opts; - let opts = List.map (fun (n, v) -> (n, Interface.BoolValue v)) opts in - let opts = (width, Interface.IntValue !width_ref):: opts in + (** Integer option *) + + let width = ["Printing"; "Width"] + let width_state = ref None + let set_printing_width w = width_state := Some w + + (** Transmitting options to coqtop *) + + let enforce h k = + let mkopt o v acc = (o, Interface.BoolValue v) :: acc in + let opts = Hashtbl.fold mkopt current_state [] in + let opts = (width, Interface.IntValue !width_state) :: opts in eval_call (Serialize.set_options opts) h (function | Interface.Good () -> k () | _ -> failwith "Cannot set options. Resetting coqtop") - let enforce_hack h k = - let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] - in - set elements h k - end let goals h k = - PrintOpt.enforce_hack h (fun () -> eval_call Serialize.goals h k) + PrintOpt.enforce h (fun () -> eval_call Serialize.goals h k) let evars h k = - PrintOpt.enforce_hack h (fun () -> eval_call Serialize.evars h k) + PrintOpt.enforce h (fun () -> eval_call Serialize.evars h k) diff --git a/ide/coq.mli b/ide/coq.mli index 041485237..52f58caa6 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -128,15 +128,17 @@ val search : Interface.search_flags -> string Interface.coq_object list atask module PrintOpt : sig - type t - val implicit : t - val coercions : t - val raw_matching : t - val notations : t - val all_basic : t - val existential : t - val universes : t + type t (** Representation of an option *) + type bool_descr = { opts : t list; init : bool; label : string } + + val bool_items : bool_descr list + + val set : t -> bool -> unit val set_printing_width : int -> unit - val set : (t * bool) list -> task + + (** [enforce] transmits to coq the current option values. + It is also called by [goals] and [evars] above. *) + + val enforce : task end diff --git a/ide/coqOps.ml b/ide/coqOps.ml index f289c424e..94036e9a1 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -28,7 +28,7 @@ object method raw_coq_query : string -> Coq.task method show_goals : Coq.task method backtrack_last_phrase : Coq.task - method include_file_dir_in_path : Coq.task + method initialize : Coq.task end class coqops @@ -357,9 +357,9 @@ object(self) clear_info (); push_info "Restarted"; (* apply the initial commands to coq *) - self#include_file_dir_in_path h k; + self#initialize h k; - method include_file_dir_in_path h k = + method private include_file_dir_in_path h k = match get_filename () with |None -> k () |Some f -> @@ -378,70 +378,8 @@ object(self) k () |Interface.Good _ | Interface.Unsafe _ -> k ())) -(** NB: Events during text edition: + method initialize h k = + self#include_file_dir_in_path h + (fun () -> Coq.PrintOpt.enforce h k) - - [begin_user_action] - - [insert_text] (or [delete_range] when deleting) - - [changed] - - [end_user_action] - - When pasting a text containing tags (e.g. the sentence terminators), - there is actually many [insert_text] and [changed]. For instance, - for "a. b.": - - - [begin_user_action] - - [insert_text] (for "a") - - [changed] - - [insert_text] (for ".") - - [changed] - - [apply_tag] (for the tag of ".") - - [insert_text] (for " b") - - [changed] - - [insert_text] (for ".") - - [changed] - - [apply_tag] (for the tag of ".") - - [end_user_action] - - Since these copy-pasted tags may interact badly with the retag mechanism, - we now don't monitor the "changed" event, but rather the "begin_user_action" - and "end_user_action". We begin by setting a mark at the initial cursor - point. At the end, the zone between the mark and the cursor is to be - untagged and then retagged. *) - - initializer - let _ = buffer#connect#insert_text - ~callback:(fun it s -> - (* If a #insert happens in the locked zone, we discard it. - Other solution: always use #insert_interactive and similar *) - if (it#compare self#get_start_of_input)<0 then - GtkSignal.stop_emit (); - if String.length s > 1 then - let () = Minilib.log "insert_text: Placing cursor" in - buffer#place_cursor ~where:it; - if String.contains s '\n' then - let () = Minilib.log "insert_text: Recentering" in - script#recenter_insert) - in - let _ = buffer#connect#begin_user_action - ~callback:(fun () -> - let where = self#get_insert in - buffer#move_mark (`NAME "prev_insert") ~where; - let start = self#get_start_of_input in - let stop = buffer#end_iter in - buffer#remove_tag Tags.Script.error ~start ~stop) - in - let _ = buffer#connect#end_user_action - ~callback:(fun () -> Sentence.tag_on_insert buffer) - in - let _ = buffer#connect#after#mark_set - ~callback:(fun it m -> - !set_location - (Printf.sprintf "Line: %5d Char: %3d" - (self#get_insert#line + 1) - (self#get_insert#line_offset + 1)); - match GtkText.Mark.get_name m with - | Some "insert" -> () - | Some s -> Minilib.log (s^" moved") - | None -> ()) - in () end diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 2a6963fee..acc80cd62 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -17,7 +17,7 @@ object method raw_coq_query : string -> Coq.task method show_goals : Coq.task method backtrack_last_phrase : Coq.task - method include_file_dir_in_path : Coq.task + method initialize : Coq.task end class coqops : diff --git a/ide/coqide.ml b/ide/coqide.ml index bcd638689..7b5ccca83 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -88,27 +88,7 @@ let make_coqtop_args = function |Append_args -> get_args the_file @ !sup_args |Subst_args -> get_args the_file -module Opt = Coq.PrintOpt - -let print_items = [ - ([Opt.implicit],"Display implicit arguments","Display _implicit arguments", - "i",false); - ([Opt.coercions],"Display coercions","Display _coercions","c",false); - ([Opt.raw_matching],"Display raw matching expressions", - "Display raw _matching expressions","m",true); - ([Opt.notations],"Display notations","Display _notations","n",true); - ([Opt.all_basic],"Display all basic low-level contents", - "Display _all basic low-level contents","a",false); - ([Opt.existential],"Display existential variable instances", - "Display _existential variable instances","e",false); - ([Opt.universes],"Display universe levels","Display _universe levels", - "u",false); - ([Opt.all_basic;Opt.existential;Opt.universes], - "Display all low-level contents", "Display all _low-level contents", - "l",false) -] - -let create_session f = Session.create f (make_coqtop_args f) print_items +let create_session f = Session.create f (make_coqtop_args f) (** Auxiliary functions for the File operations *) @@ -550,10 +530,8 @@ let tactic_wizard_callback l _ = let printopts_callback opts v = let b = v#get_active in - let opts = List.map (fun o -> (o,b)) opts in - send_to_coq (fun sn h k -> - Coq.PrintOpt.set opts h - (fun () -> sn.coqops#show_goals h k)) + let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in + send_to_coq (fun sn -> sn.coqops#show_goals) (** Templates menu *) @@ -791,11 +769,27 @@ let item = GAction.add_action let toggle_item = GAction.add_toggle_action +(** Search the first '_' in a label string and return the following + character as shortcut, plus the string without the '_' *) + +let get_shortcut s = + try + let n = String.length s in + let i = String.index s '_' in + let k = String.make 1 s.[i+1] in + let s' = (String.sub s 0 i) ^ (String.sub s (i+1) (n-i-1)) in + Some k, s' + with _ -> None,s + +module Opt = Coq.PrintOpt + let toggle_items menu_name l = - let f (opts,name,label,key,dflt) = - toggle_item name ~active:dflt ~label - ~accel:(prefs.modifier_for_display^key) - ~callback:(printopts_callback opts) + let f d = + let label = d.Opt.label in + let k, name = get_shortcut label in + let accel = Option.map ((^) prefs.modifier_for_display) k in + toggle_item name ~label ?accel ~active:d.Opt.init + ~callback:(printopts_callback d.Opt.opts) menu_name in List.iter f l @@ -977,7 +971,7 @@ let build_ui () = then ccw#frame#misc#hide () else ccw#frame#misc#show ()) ]; - toggle_items view_menu print_items; + toggle_items view_menu Coq.PrintOpt.bool_items; menu navigation_menu [ item "Navigation" ~label:"_Navigation"; diff --git a/ide/session.ml b/ide/session.ml index ac23e2f0a..13950cd4c 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -26,17 +26,7 @@ type session = { tab_label : GMisc.label; } -type print_items = - (Coq.PrintOpt.t list * string * string * string * bool) list - -let create file coqtop_args print_items = - let basename = match file with - |None -> "*scratch*" - |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f) - in - let coqtop = Coq.spawn_coqtop coqtop_args in - let reset () = Coq.reset_coqtop coqtop - in +let create_buffer () = let buffer = GSourceView2.source_buffer ~tag_table:Tags.Script.table ~highlight_matching_brackets:true @@ -47,38 +37,122 @@ let create file coqtop_args print_items = let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in let _ = buffer#place_cursor ~where:buffer#start_iter in - let _ = buffer#add_selection_clipboard Ideutils.cb - in - let script = Wg_ScriptView.script_view coqtop ~source_buffer:buffer + let _ = buffer#add_selection_clipboard Ideutils.cb in + buffer + +let create_script coqtop source_buffer = + let script = Wg_ScriptView.script_view coqtop ~source_buffer ~show_line_numbers:true ~wrap_mode:`NONE () in let _ = script#misc#set_name "ScriptWindow" in + script + +(** NB: Events during text edition: + + - [begin_user_action] + - [insert_text] (or [delete_range] when deleting) + - [changed] + - [end_user_action] + + When pasting a text containing tags (e.g. the sentence terminators), + there is actually many [insert_text] and [changed]. For instance, + for "a. b.": + + - [begin_user_action] + - [insert_text] (for "a") + - [changed] + - [insert_text] (for ".") + - [changed] + - [apply_tag] (for the tag of ".") + - [insert_text] (for " b") + - [changed] + - [insert_text] (for ".") + - [changed] + - [apply_tag] (for the tag of ".") + - [end_user_action] + + Since these copy-pasted tags may interact badly with the retag mechanism, + we now don't monitor the "changed" event, but rather the "begin_user_action" + and "end_user_action". We begin by setting a mark at the initial cursor + point. At the end, the zone between the mark and the cursor is to be + untagged and then retagged. *) + +let set_buffer_handlers buffer script = + let start_of_input () = buffer#get_iter_at_mark (`NAME "start_of_input") in + let get_insert () = buffer#get_iter_at_mark `INSERT + in + let _ = buffer#connect#insert_text + ~callback:(fun it s -> + (* If a #insert happens in the locked zone, we discard it. + Other solution: always use #insert_interactive and similar *) + if (it#compare (start_of_input ()))<0 then + GtkSignal.stop_emit (); + if String.length s > 1 then + let () = Minilib.log "insert_text: Placing cursor" in + buffer#place_cursor ~where:it; + if String.contains s '\n' then + let () = Minilib.log "insert_text: Recentering" in + script#recenter_insert) + in + let _ = buffer#connect#begin_user_action + ~callback:(fun () -> + (* We remove any error red zone, and place the [prev_insert] mark *) + let where = get_insert () in + buffer#move_mark (`NAME "prev_insert") ~where; + let start = start_of_input () in + let stop = buffer#end_iter in + buffer#remove_tag Tags.Script.error ~start ~stop) + in + let _ = buffer#connect#end_user_action + ~callback:(fun () -> Sentence.tag_on_insert buffer) + in + let _ = buffer#connect#after#mark_set + ~callback:(fun it m -> + let ins = get_insert () in + !Ideutils.set_location + (Printf.sprintf "Line: %5d Char: %3d" + (ins#line + 1) + (ins#line_offset + 1)); + match GtkText.Mark.get_name m with + | Some "insert" -> () + | Some s -> Minilib.log (s^" moved") + | None -> ()) + in () + +let create_proof () = let proof = Wg_ProofView.proof_view () in let _ = proof#misc#set_can_focus true in - let _ = - GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] + let _ = GtkBase.Widget.add_events proof#as_widget + [`ENTER_NOTIFY;`POINTER_MOTION] in + proof + +let create_messages () = let messages = Wg_MessageView.message_view () in - let _ = messages#misc#set_can_focus true + let _ = messages#misc#set_can_focus true in + messages + +let create file coqtop_args = + let basename = match file with + |None -> "*scratch*" + |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f) in + let coqtop = Coq.spawn_coqtop coqtop_args in + let reset () = Coq.reset_coqtop coqtop in + let buffer = create_buffer () in + let script = create_script coqtop buffer in + let _ = set_buffer_handlers (buffer :> GText.buffer) script in + let proof = create_proof () in + let messages = create_messages () in let command = new Wg_Command.command_window coqtop in let finder = new Wg_Find.finder (script :> GText.view) in let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in + let _ = fops#update_stats in let cops = new CoqOps.coqops script proof messages (fun () -> fops#filename) in let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in - let _ = fops#update_stats in - let _ = Coq.init_coqtop coqtop - (fun h k -> - cops#include_file_dir_in_path h - (fun () -> - let fold accu (opts, _, _, _, dflt) = - List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts - in - let options = List.fold_left fold [] print_items in - Coq.PrintOpt.set options h k)) - in + let _ = Coq.init_coqtop coqtop cops#initialize in { buffer = (buffer :> GText.buffer); script=script; diff --git a/ide/session.mli b/ide/session.mli index 75b03d860..e98cbbd7d 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -22,11 +22,8 @@ type session = { tab_label : GMisc.label; } -type print_items = - (Coq.PrintOpt.t list * string * string * string * bool) list - (** [create filename coqtop_args] *) -val create : string option -> string list -> print_items -> session +val create : string option -> string list -> session val kill : session -> unit |