Coqide: cleaner Coq.PrintOpt and session creation

 PrintOpt.set now only updates the state Hashtbl of options,
 a PrintOpt.enforce is mandatory to transmit them to coqtop.
 This enforce is done for instance by Coq.goals.

 The various signal handlers about coqide's buffer are now installed
 in session creation, and not anymore via the coqops initializer.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16105 85f007b7-540e-0410-9357-904b9bb8a0f7

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