diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 9 | ||||
| -rw-r--r-- | interp/notation.ml | 13 | ||||
| -rw-r--r-- | interp/notation.mli | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 4 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 9 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
11 files changed, 51 insertions, 11 deletions
@@ -4,6 +4,7 @@ Changes from V8.5beta2 to ... Vernacular commands - New command "Redirect" to redirect the output of a command to a file. +- New command "Undelimit Scope" to remove the delimiter of a scope. Tactics diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 37cbd1eac..aabc8a899 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available. \subsubsection{Local opening of an interpretation scope \label{scopechange} \index{\%} -\comindex{Delimit Scope}} +\comindex{Delimit Scope} +\comindex{Undelimit Scope}} It is possible to locally extend the interpretation scope stack using the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey} @@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} \end{quote} +To remove a delimiting key of a scope, use the command + +\begin{quote} +\texttt{Undelimit Scope} {\scope} +\end{quote} + \subsubsection{Binding arguments of a constant to an interpretation scope \comindex{Arguments}} diff --git a/interp/notation.ml b/interp/notation.ml index 555dfa804..0b5791d32 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -200,6 +200,19 @@ let declare_delimiters scope key = end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map +let remove_delimiters scope = + let sc = find_scope scope in + let newsc = { sc with delimiters = None } in + match sc.delimiters with + | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".") + | Some key -> + scope_map := String.Map.add scope newsc !scope_map; + try + let _ = ignore (String.Map.find key !delimiters_map) in + delimiters_map := String.Map.remove key !delimiters_map + with Not_found -> + assert false (* A delimiter for scope [scope] should exist *) + let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> diff --git a/interp/notation.mli b/interp/notation.mli index 854c52b2c..38bd5fc7b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -55,6 +55,7 @@ val find_scope : scope_name -> scope (** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit +val remove_delimiters : scope_name -> unit val find_delimiters_scope : Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d7b269a1d..0ca3bb35f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -284,7 +284,7 @@ type vernac_expr = | VernacSyntaxExtension of obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) - | VernacDelimiters of scope_name * string + | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * reference or_by_notation list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e8a1b512c..fe9c58240 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -96,12 +96,12 @@ GEXTEND Gram | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_poly -> v ] + | v = vernac_poly -> v ] ] ; - vernac_poly: + vernac_poly: [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) - | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) | v = vernac_aux -> v ] ] ; @@ -146,7 +146,7 @@ GEXTEND Gram ] ] ; - subgoal_command: + subgoal_command: [ [ c = query_command; "." -> begin function | Some (SelectNth g) -> c (Some g) @@ -1043,7 +1043,9 @@ GEXTEND Gram VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc,key) + VernacDelimiters (sc, Some key) + | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> + VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 smart_global -> VernacBindScope (sc,refl) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0..4e889e55f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -644,11 +644,15 @@ module Make keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) - | VernacDelimiters (sc,key) -> + | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ str key ) + | VernacDelimiters (sc, None) -> + return ( + keyword "Undelimit Scope" ++ spc () ++ str sc + ) | VernacBindScope (sc,cll) -> return ( keyword "Bind Scope" ++ spc () ++ str sc ++ diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c7..aaa6c2c07 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -509,8 +509,10 @@ let rec tmpp v loc = | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] - | VernacDelimiters (name,tag) -> + | VernacDelimiters (name,Some tag) -> xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope loc "undelimit" name ~attr:[] [] | VernacBindScope (name,l) -> xmlScope loc "bind" name (List.map (function diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 300bf5b49..7616bfff6 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1383,7 +1383,10 @@ let add_infix local ((loc,inf),modifiers) pr sc = (**********************************************************************) (* Delimiters and classes bound to scopes *) -type scope_command = ScopeDelim of string | ScopeClasses of scope_class list +type scope_command = + | ScopeDelim of string + | ScopeClasses of scope_class list + | ScopeRemove let load_scope_command _ (_,(scope,dlm)) = Notation.declare_scope scope @@ -1393,6 +1396,7 @@ let open_scope_command i (_,(scope,o)) = match o with | ScopeDelim dlm -> Notation.declare_delimiters scope dlm | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl + | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = load_scope_command 1 o; @@ -1418,6 +1422,9 @@ let inScopeCommand : scope_name * scope_command -> obj = let add_delimiters scope key = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let remove_delimiters scope = + Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) + let add_class_scope scope cl = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 38a377577..f22839f48 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit (** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit +val remove_delimiters : scope_name -> unit val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d9f8f52c..04d572cd3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -424,7 +424,9 @@ let vernac_syntax_extension locality local = let local = enforce_module_locality locality local in Metasyntax.add_syntax_extension local -let vernac_delimiters = Metasyntax.add_delimiters +let vernac_delimiters sc = function + | Some lr -> Metasyntax.add_delimiters sc lr + | None -> Metasyntax.remove_delimiters sc let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) |