--- a/NEWS Mon Mar 01 17:07:36 2010 +0100
+++ b/NEWS Mon Mar 01 17:09:42 2010 +0100
@@ -51,6 +51,10 @@
datatype constructors have been renamed from InfixName to Infix etc.
Minor INCOMPATIBILITY.
+* Commands 'type_notation' and 'no_type_notation' declare type syntax
+within a local theory context, with explicit checking of the
+constructors involved (in contrast to the raw 'syntax' versions).
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 01 17:07:36 2010 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Mar 01 17:09:42 2010 +0100
@@ -357,32 +357,47 @@
*}
-section {* Explicit term notation *}
+section {* Explicit notation *}
text {*
\begin{matharray}{rcll}
+ @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
\begin{rail}
+ ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+ ;
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
\end{rail}
\begin{description}
+ \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
+ syntax with an existing type constructor. The arity of the
+ constructor is retrieved from the context.
+
+ \item @{command "no_type_notation"} is similar to @{command
+ "type_notation"}, but removes the specified syntax annotation from
+ the present context.
+
\item @{command "notation"}~@{text "c (mx)"} associates mixfix
- syntax with an existing constant or fixed variable. This is a
- robust interface to the underlying @{command "syntax"} primitive
- (\secref{sec:syn-trans}). Type declaration and internal syntactic
- representation of the given entity is retrieved from the context.
+ syntax with an existing constant or fixed variable. The type
+ declaration of the given entity is retrieved from the context.
\item @{command "no_notation"} is similar to @{command "notation"},
but removes the specified syntax annotation from the present
context.
\end{description}
+
+ Compared to the underlying @{command "syntax"} and @{command
+ "no_syntax"} primitives (\secref{sec:syn-trans}), the above commands
+ provide explicit checking wrt.\ the logical context, and work within
+ general local theory targets, not just the global theory.
*}
--- a/src/Pure/Isar/isar_syn.ML Mon Mar 01 17:07:36 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Mar 01 17:09:42 2010 +0100
@@ -226,6 +226,16 @@
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
+ OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
+ (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
+ >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+
+val _ =
+ OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
+ (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
+ >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+
+val _ =
OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
(opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
--- a/src/Pure/Isar/specification.ML Mon Mar 01 17:07:36 2010 +0100
+++ b/src/Pure/Isar/specification.ML Mon Mar 01 17:09:42 2010 +0100
@@ -42,6 +42,8 @@
local_theory -> local_theory
val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
local_theory -> local_theory
+ val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+ val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
@@ -255,12 +257,24 @@
(* notation *)
+local
+
+fun gen_type_notation prep_type add mode args lthy =
+ lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
+
fun gen_notation prep_const add mode args lthy =
lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
+in
+
+val type_notation = gen_type_notation (K I);
+val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
+
val notation = gen_notation (K I);
val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
+end;
+
(* fact statements *)