Now CoqIDE relies on the option query mechanism to set printing options. Still a bit hackish.

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

3 files changed, 26 insertions, 39 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 77f3c44ae2..4d7437fa43 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -219,40 +219,31 @@ let hints coqtop = eval_call coqtop Ide_intf.hints
 module PrintOpt =
 struct
   type t = string list
-  let implicit = ["Implicit"]
-  let coercions = ["Coercions"]
-  let raw_matching = ["Matching";"Synth"]
-  let notations = ["Notations"]
-  let all_basic = ["All"]
-  let existential = ["Existential Instances"]
-  let universes = ["Universes"]
+  let implicit = ["Printing"; "Implicit"]
+  let coercions = ["Printing"; "Coercions"]
+  let raw_matching = ["Printing"; "Matching"; "Synth"]
+  let notations = ["Printing"; "Notations"]
+  let all_basic = ["Printing"; "All"]
+  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 ]
 
-  let set coqtop opt value =
-    Hashtbl.replace state_hack opt value;
-    List.fold_left
-      (fun acc cmd -> 
-         let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         match interp coqtop ~raw:true ~verbose:false str with
-           | Interface.Good _ -> acc
-           | Interface.Fail (l,errstr) ->  Interface.Fail (l,"Could not eval \""^str^"\": "^errstr)
-      )
-      (Interface.Good ())
-      opt
-
-  let enforce_hack coqtop = Hashtbl.fold
-    (fun opt v acc ->
-      match set coqtop opt v with
-        | Interface.Good () -> Interface.Good ()
-        | Interface.Fail str -> Interface.Fail str)
-    state_hack (Interface.Good ())
+  let set coqtop options =
+    let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
+    let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
+    match eval_call coqtop (Ide_intf.set_options options) with
+    | Interface.Good () -> ()
+    | _ -> raise (Failure "Cannot set options.")
+
+  let enforce_hack coqtop =
+    let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in
+    set coqtop elements
+
 end
 
 let goals coqtop =
-  match PrintOpt.enforce_hack coqtop with
-    | Interface.Good () -> eval_call coqtop Ide_intf.goals
-    | Interface.Fail str -> Interface.Fail str
-
+  let () = PrintOpt.enforce_hack coqtop in
+  eval_call coqtop Ide_intf.goals
diff --git a/ide/coq.mli b/ide/coq.mli
index eb26c60352..5b58113928 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -68,5 +68,5 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> t -> bool -> unit Interface.value
+  val set : coqtop -> (t * bool) list -> unit
 end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 498660081e..e02d35f1a5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -340,12 +340,8 @@ let print_items = [
 ]
 
 let setopts ct opts v =
-  List.fold_left
-    (fun acc o ->
-      match Coq.PrintOpt.set ct o v with
-        | Interface.Good () -> acc
-        | Interface.Fail lstr -> Interface.Fail lstr
-    ) (Interface.Good ()) opts
+  let opts = List.map (fun o -> (o, v)) opts in
+  Coq.PrintOpt.set ct opts
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -1499,8 +1495,8 @@ let create_session file =
     proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in
   let _ =
     GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
-  let _ =
-    List.map (fun (opts,_,_,_,dflt) -> setopts !ct opts dflt) print_items in
+  let () =
+    List.iter (fun (opts,_,_,_,dflt) -> setopts !ct opts dflt) print_items in
   let _ = legacy_av#activate () in
   let _ =
     proof#event#connect#motion_notify ~callback:
@@ -2534,7 +2530,7 @@ let main files =
          GAction.add_toggle_action name ~active:dflt ~label
 	   ~accel:(!current.modifier_for_display^key)
           ~callback:(fun v -> do_or_activate (fun a ->
-            ignore (setopts !(session_notebook#current_term.toplvl) opts v#get_active);
+            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
             a#show_goals) ()) display_actions)
       print_items;
     GAction.add_actions compile_actions [