diff options
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 76 | ||||
| -rw-r--r-- | test-suite/success/attribute_syntax.v | 7 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 30 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
4 files changed, 60 insertions, 55 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 48c65f631f..895886605d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,34 +91,30 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? {| Local | Global | Export } } Set @flag +.. cmd:: Set @flag :name: Set - Sets :token:`flag` on. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` on. -.. cmd:: {? {| Local | Global | Export } } Unset @flag +.. cmd:: Unset @flag :name: Unset - Sets :token:`flag` off. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` off. .. cmd:: Test @flag Prints the current value of :token:`flag`. -.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } +.. cmd:: Set @option {| @num | @string } :name: Set @option - Sets :token:`option` to the specified value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to the specified value. -.. cmd:: {? {| Local | Global | Export } } Unset @option +.. cmd:: Unset @option :name: Unset @option - Sets :token:`option` to its default value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to its default value. .. cmd:: Test @option @@ -157,27 +153,37 @@ capital letter. A synonym for :cmd:`Print Options`. -.. _set_unset_scope_qualifiers: +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. -Scope qualifiers for :cmd:`Set` and :cmd:`Unset` -````````````````````````````````````````````````` - -:n:`{? {| Local | Global | Export } }` - -Flag and option settings can be global in scope or local to nested scopes created by -:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - -* no qualifier: the original setting is *not* restored at the end of the current module or section. -* **Local**: the setting is applied within the current scope. The original value of the option - or flag is restored at the end of the current module or section. -* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current - module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing - the file sets the option. -* **Export**: similar to **Local**, the original value of the option or flag is restored at the - end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing - the file sets the option. +.. note:: -Newly opened scopes inherit the current settings. + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). .. _requests-to-the-environment: @@ -1192,9 +1198,11 @@ Controlling the locality of commands .. attr:: export - Some commands support an :attr:`export` attribute. The effect of the attribute - is to make the effect of the command available when the module containing it - is imported. The :cmd:`Hint` command accepts it for instance. + Some commands support an :attr:`export` attribute. The effect of + the attribute is to make the effect of the command available when + the module containing it is imported. It is supported in + particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + commands. .. _controlling-typing-flags: diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index 4717759dec..b403fc120c 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -36,3 +36,10 @@ Check M.zed@{_}. Fail Check zed. Check M.kats@{_}. Fail Check kats. + +Export Set Foo. + +#[ export ] Set Foo. + +Fail #[ export ] Export Foo. +(* Attribute for Locality specified twice *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1ea4d6cb02..295db70bc9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1493,40 +1493,29 @@ let vernac_set_opacity ~local (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let get_option_locality export local = - if export then - if Option.is_empty local then OptExport - else user_err Pp.(str "Locality modifiers forbidden with Export") - else match local with - | Some true -> OptLocal - | Some false -> OptGlobal - | None -> OptDefault - -let vernac_set_option0 ~local export key opt = - let locality = get_option_locality export local in +let vernac_set_option0 ~locality key opt = match opt with | OptionUnset -> unset_option_value_gen ~locality key | OptionSetString s -> set_string_option_value_gen ~locality key s | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n) | OptionSetTrue -> set_bool_option_value_gen ~locality key true -let vernac_set_append_option ~local export key s = - let locality = get_option_locality export local in +let vernac_set_append_option ~locality key s = set_string_option_append_value_gen ~locality key s -let vernac_set_option ~local export table v = match v with +let vernac_set_option ~locality table v = match v with | OptionSetString s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then - vernac_set_append_option ~local export table s + vernac_set_append_option ~locality table s else let (last, prefix) = List.sep_last table in if String.equal last "Append" && not (List.is_empty prefix) then - vernac_set_append_option ~local export prefix s + vernac_set_append_option ~locality prefix s else - vernac_set_option0 ~local export table v -| _ -> vernac_set_option0 ~local export table v + vernac_set_option0 ~locality table v +| _ -> vernac_set_option0 ~locality table v let vernac_add_option key lv = let f = function @@ -2193,9 +2182,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl) | VernacSetStrategy l -> VtDefault(fun () -> with_locality ~atts vernac_set_strategy l) - | VernacSetOption (export, key,v) -> + | VernacSetOption (export,key,v) -> + let atts = if export then ("export", VernacFlagEmpty) :: atts else atts in VtDefault(fun () -> - vernac_set_option ~local:(only_locality atts) export key v) + vernac_set_option ~locality:(parse option_locality atts) key v) | VernacRemoveOption (key,v) -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 67e1fb9495..b7c6d3c490 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -399,7 +399,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacSetOption of export_flag * Goptions.option_name * option_setting + | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting | 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 |