From d1593f3524cfc1d0fdbd0194e05703d15dc9ba00 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 14 Aug 2009 16:17:52 +0000 Subject: Ajout de la gestion de Local et Global pour les options (au sens de Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 4 ++-- library/goptions.ml | 61 +++++++++++++++++++++++++++++++++++------------ library/goptions.mli | 5 ++++ library/libobject.mli | 4 ++-- parsing/g_vernac.ml4 | 10 ++++---- parsing/ppvernac.ml | 11 ++++++--- toplevel/vernacentries.ml | 18 +++++++------- toplevel/vernacexpr.ml | 23 ++++++++---------- 8 files changed, 87 insertions(+), 49 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 35feb59ed..4fd48a306 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -275,8 +275,8 @@ let rec attribute_of_vernac_command = function | VernacDeclareImplicits _ -> [] | VernacReserve _ -> [] | VernacSetOpacity _ -> [] - | VernacSetOption (["Ltac";"Debug"], _) -> [DebugCommand] - | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> + | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] + | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> if coqide_known_option o then [KnownOptionCommand] else [] | VernacSetOption _ -> [] | VernacRemoveOption _ -> [] diff --git a/library/goptions.ml b/library/goptions.ml index bf431e1fc..86012b113 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -235,24 +235,46 @@ let declare_option cast uncast { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in - let write = if sync then - let (decl_obj,_) = - declare_object {(default_object (nickname key)) with + (* spiwack: I use two spaces in the nicknames of "local" and "global" objects. + That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are + lists of strings *without* spaces. *) + let (write,lwrite,gwrite) = if sync then + let (ldecl_obj,_) = (* "Local": doesn't survive section or modules. *) + declare_object {(default_object ("L "^nickname key)) with cache_function = (fun (_,v) -> write v); classify_function = (fun _ -> Dispose)} in + let (decl_obj,_) = (* default locality: survives sections but not modules. *) + declare_object {(default_object (nickname key)) with + cache_function = (fun (_,v) -> write v); + classify_function = (fun _ -> Dispose); + discharge_function = (fun (_,v) -> Some v)} + in + let (gdecl_obj,_) = (* "Global": survives section and modules. *) + declare_object {(default_object ("G "^nickname key)) with + cache_function = (fun (_,v) -> write v); + classify_function = (fun v -> Keep v); + discharge_function = (fun (_,v) -> Some v); + load_function = (fun _ (_,v) -> write v); + (* spiwack: I'm unsure whether this function does anyting *) + export_function = (fun v -> Some v)} + in let _ = declare_summary (nickname key) { freeze_function = read; unfreeze_function = write; init_function = (fun () -> write default) } in - fun v -> add_anonymous_leaf (decl_obj v) - else write + begin fun v -> add_anonymous_leaf (decl_obj v) end , + begin fun v -> add_anonymous_leaf (ldecl_obj v) end , + begin fun v -> add_anonymous_leaf (gdecl_obj v) end + else write,write,write in let cread () = cast (read ()) in let cwrite v = write (uncast v) in - value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; - write + let clwrite v = lwrite (uncast v) in + let cgwrite v = gwrite (uncast v) in + value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab; + write type 'a write_function = 'a -> unit @@ -273,28 +295,37 @@ let declare_string_option = (* Setting values of options *) -let set_option_value check_and_cast key v = - let (name,(_,read,write)) = +let set_option_value locality check_and_cast key v = + let (name,(_,read,write,lwrite,gwrite)) = try get_option key with Not_found -> error ("There is no option "^(nickname key)^".") in + let write = match locality with + | None -> write + | Some true -> lwrite + | Some false -> gwrite + in write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option" -let set_int_option_value = set_option_value +let set_int_option_value_gen locality = set_option_value locality (fun v -> function | (IntValue _) -> IntValue v | _ -> bad_type_error ()) -let set_bool_option_value = set_option_value +let set_bool_option_value_gen locality = set_option_value locality (fun v -> function | (BoolValue _) -> BoolValue v | _ -> bad_type_error ()) -let set_string_option_value = set_option_value +let set_string_option_value_gen locality = set_option_value locality (fun v -> function | (StringValue _) -> StringValue v | _ -> bad_type_error ()) +let set_int_option_value = set_int_option_value_gen None +let set_bool_option_value = set_bool_option_value_gen None +let set_string_option_value = set_string_option_value_gen None + (* Printing options/tables *) let msg_option_value (name,v) = @@ -307,7 +338,7 @@ let msg_option_value (name,v) = | IdentValue r -> pr_global_env Idset.empty r let print_option_value key = - let (name,(_,read,_)) = get_option key in + let (name,(_,read,_,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -322,7 +353,7 @@ let print_tables () = msg (str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name,(sync,read,write)) p -> + (fun key (name,(sync,read,_,_,_)) p -> if sync then p ++ str (" "^(nickname key)^": ") ++ msg_option_value (name,read()) ++ fnl () @@ -331,7 +362,7 @@ let print_tables () = !value_tab (mt ()) ++ str "Asynchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name,(sync,read,write)) p -> + (fun key (name,(sync,read,_,_,_)) p -> if sync then p else diff --git a/library/goptions.mli b/library/goptions.mli index aefddbbda..eba44a896 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -153,6 +153,11 @@ val get_ref_table : mem : reference -> unit; print : unit > +(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *) +val set_int_option_value_gen : bool option -> option_name -> int option -> unit +val set_bool_option_value_gen : bool option -> option_name -> bool -> unit +val set_string_option_value_gen : bool option -> option_name -> string -> unit + val set_int_option_value : option_name -> int option -> unit val set_bool_option_value : option_name -> bool -> unit val set_string_option_value : option_name -> string -> unit diff --git a/library/libobject.mli b/library/libobject.mli index f32d3baa7..a8b5702f8 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -29,7 +29,7 @@ open Mod_subst * an opening function, specifying what to do when the module containing the object is opened (imported); If the object wishes to register its visibility in the Nametab, - it should do so for the sufix of the length the "int" argument + it should do so for the suffix of the length the "int" argument * a classification function, specyfying what to do with the object, when the current module (containing the object) is ended; @@ -49,7 +49,7 @@ open Mod_subst * a substitution function, performing the substitution; this function should be declared for substitutive objects - only (see obove) + only (see above) * a discharge function, that is applied at section closing time to collect the data necessary to rebuild the discharged form of the diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ea686e5a3..d10a2950c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -637,11 +637,11 @@ GEXTEND Gram (* Pour intervenir sur les tables de paramtres *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) + VernacSetOption (use_locality_full(),table,v) | "Set"; table = option_table -> - VernacSetOption (table,BoolValue true) + VernacSetOption (use_locality_full(),table,BoolValue true) | IDENT "Unset"; table = option_table -> - VernacUnsetOption table + VernacUnsetOption (use_locality_full(),table) | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table @@ -779,10 +779,10 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (["Ltac";"Debug"], BoolValue true) + VernacSetOption (None,["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (["Ltac";"Debug"], BoolValue false) + VernacSetOption (None,["Ltac";"Debug"], BoolValue false) ] ]; END diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 3bf2f0ede..656c38497 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -147,6 +147,10 @@ let pr_search a b pr_p = match a with | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b +let pr_locality_full = function + | None -> mt() + | Some true -> str"Local " + | Some false -> str"Global " let pr_locality local = if local then str "Local " else str "" let pr_non_locality local = if local then str "" else str "Global " @@ -854,9 +858,10 @@ let rec pr_vernac = function str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) - | VernacUnsetOption na -> - hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) + | VernacUnsetOption (l,na) -> + hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None) + | VernacSetOption (l,na,v) -> + hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v) | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1de9d739a..0e11ba582 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -983,15 +983,15 @@ let vernac_set_opacity local str = let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in Redexpr.set_strategy local str -let vernac_set_option key = function - | StringValue s -> set_string_option_value key s - | IntValue n -> set_int_option_value key (Some n) - | BoolValue b -> set_bool_option_value key b +let vernac_set_option locality key = function + | StringValue s -> set_string_option_value_gen locality key s + | IntValue n -> set_int_option_value_gen locality key (Some n) + | BoolValue b -> set_bool_option_value_gen locality key b -let vernac_unset_option key = - try set_bool_option_value key false +let vernac_unset_option locality key = + try set_bool_option_value_gen locality key false with _ -> - set_int_option_value key None + set_int_option_value_gen locality key None let vernac_add_option key lv = let f = function @@ -1371,8 +1371,8 @@ let interp c = match c with | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl - | VernacSetOption (key,v) -> vernac_set_option key v - | VernacUnsetOption key -> vernac_unset_option key + | VernacSetOption (locality,key,v) -> vernac_set_option locality key v + | VernacUnsetOption (locality,key) -> vernac_unset_option locality key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ee86f982e..eaa434956 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -309,8 +309,8 @@ type vernac_expr = | VernacReserve of lident list * constr_expr | VernacSetOpacity of locality_flag * (Conv_oracle.level * lreference list) list - | VernacUnsetOption of Goptions.option_name - | VernacSetOption of Goptions.option_name * option_value + | VernacUnsetOption of bool option * Goptions.option_name + | VernacSetOption of bool option * Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list @@ -367,24 +367,21 @@ let check_locality () = if !locality_flag = Some false then syntax_checking_error "This command does not support the \"Global\" prefix." -let use_locality () = - let local = match !locality_flag with Some true -> true | _ -> false in +let use_locality_full () = + let r = !locality_flag in locality_flag := None; - local + r + +let use_locality () = + match use_locality_full () with Some true -> true | _ -> false let use_locality_exp () = local_of_bool (use_locality ()) let use_section_locality () = - let local = - match !locality_flag with Some b -> b | None -> Lib.sections_are_opened () - in - locality_flag := None; - local + match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened () let use_non_locality () = - let local = match !locality_flag with Some false -> false | _ -> true in - locality_flag := None; - local + match use_locality_full () with Some false -> false | _ -> true let enforce_locality () = let local = -- cgit v1.2.3