Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

6 files changed, 13 insertions, 8 deletions

diff --git a/lib/options.ml b/lib/options.ml
index f1e40a89ec..b60210fdef 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -45,8 +45,7 @@ let if_verbose f x = if not !silent then f x
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
-let set_print_hyps_limit n = print_hyps_limit := Some n
-let unset_print_hyps_limit () = print_hyps_limit := None
+let set_print_hyps_limit n = print_hyps_limit := n
 let print_hyps_limit () = !print_hyps_limit
 
 (* A list of the areas of the system where "unsafe" operation
diff --git a/lib/options.mli b/lib/options.mli
index efc8617de0..53e796f9a9 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -28,8 +28,8 @@ val silently : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
-val set_print_hyps_limit : int -> unit
-val unset_print_hyps_limit : unit -> unit
+(* If [None], no limit *)
+val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
 
 val add_unsafe : string -> unit
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 2e84767901..78b78020d3 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -95,6 +95,8 @@ let deep_ft = with_output_to stdout
 let _ = set_gp deep_ft deep_gp
 
 (* For parametrization through vernacular *)
-let set_depth_boxes v  = Format.pp_set_max_boxes std_ft v
-let get_depth_boxes () = Format.pp_get_max_boxes std_ft ()
+let default = Format.pp_get_max_boxes std_ft ()
+let get_depth_boxes () = Some (Format.pp_get_max_boxes std_ft ())
+let set_depth_boxes v =
+  Format.pp_set_max_boxes std_ft (match v with None -> default | Some v -> v)
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 2551726df3..548b98a7f5 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -42,5 +42,5 @@ val deep_ft : Format.formatter
 
 (*s For parametrization through vernacular. *)
 
-val set_depth_boxes : int -> unit
-val get_depth_boxes : unit -> int
+val set_depth_boxes : int option -> unit
+val get_depth_boxes : unit -> int option
diff --git a/lib/util.ml b/lib/util.ml
index cd575bf08a..3354bba53e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -22,6 +22,8 @@ let errorlabstrm l pps = raise (UserError(l,pps))
 
 (* raising located exceptions *)
 type loc = int * int
+type 'a located = loc * 'a
+let dummy_loc = (0,0)
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
diff --git a/lib/util.mli b/lib/util.mli
index 6bbe609cbd..e9cd97a7c8 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -27,7 +27,9 @@ val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
 
 type loc = int * int
+type 'a located = loc * 'a
 
+val dummy_loc : loc
 val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a