# HG changeset patch
# User wenzelm
# Date 1267459782 -3600
# Node ID 4c7cba1f7ce937e71ecb1f32ddd0a829dbe48fde
# Parent  b8dead547d9e93d4ab652593e3f66cdae76069dd
added type_notation command;

diff -r b8dead547d9e -r 4c7cba1f7ce9 NEWS
--- 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 ***
 
diff -r b8dead547d9e -r 4c7cba1f7ce9 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- 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.
 *}
 
 
diff -r b8dead547d9e -r 4c7cba1f7ce9 src/Pure/Isar/isar_syn.ML
--- 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));
diff -r b8dead547d9e -r 4c7cba1f7ce9 src/Pure/Isar/specification.ML
--- 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 *)