1.1 --- a/NEWS	Mon Mar 01 17:07:36 2010 +0100
     1.2 +++ b/NEWS	Mon Mar 01 17:09:42 2010 +0100
     1.3 @@ -51,6 +51,10 @@
     1.4  datatype constructors have been renamed from InfixName to Infix etc.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Commands 'type_notation' and 'no_type_notation' declare type syntax
     1.8 +within a local theory context, with explicit checking of the
     1.9 +constructors involved (in contrast to the raw 'syntax' versions).
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  

     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Mar 01 17:07:36 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Mar 01 17:09:42 2010 +0100
     2.3 @@ -357,32 +357,47 @@
     2.4  *}
     2.5  
     2.6  
     2.7 -section {* Explicit term notation *}
     2.8 +section {* Explicit notation *}
     2.9  
    2.10  text {*
    2.11    \begin{matharray}{rcll}
    2.12 +    @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.13 +    @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.14      @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.15      @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.16    \end{matharray}
    2.17  
    2.18    \begin{rail}
    2.19 +    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
    2.20 +    ;
    2.21      ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
    2.22      ;
    2.23    \end{rail}
    2.24  
    2.25    \begin{description}
    2.26  
    2.27 +  \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
    2.28 +  syntax with an existing type constructor.  The arity of the
    2.29 +  constructor is retrieved from the context.
    2.30 +  
    2.31 +  \item @{command "no_type_notation"} is similar to @{command
    2.32 +  "type_notation"}, but removes the specified syntax annotation from
    2.33 +  the present context.
    2.34 +
    2.35    \item @{command "notation"}~@{text "c (mx)"} associates mixfix
    2.36 -  syntax with an existing constant or fixed variable.  This is a
    2.37 -  robust interface to the underlying @{command "syntax"} primitive
    2.38 -  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
    2.39 -  representation of the given entity is retrieved from the context.
    2.40 +  syntax with an existing constant or fixed variable.  The type
    2.41 +  declaration of the given entity is retrieved from the context.
    2.42    
    2.43    \item @{command "no_notation"} is similar to @{command "notation"},
    2.44    but removes the specified syntax annotation from the present
    2.45    context.
    2.46  
    2.47    \end{description}
    2.48 +
    2.49 +  Compared to the underlying @{command "syntax"} and @{command
    2.50 +  "no_syntax"} primitives (\secref{sec:syn-trans}), the above commands
    2.51 +  provide explicit checking wrt.\ the logical context, and work within
    2.52 +  general local theory targets, not just the global theory.
    2.53  *}
    2.54  
    2.55  

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Mar 01 17:07:36 2010 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 01 17:09:42 2010 +0100
     3.3 @@ -226,6 +226,16 @@
     3.4      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
     3.5  
     3.6  val _ =
     3.7 +  OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl
     3.8 +    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     3.9 +    >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
    3.10 +
    3.11 +val _ =
    3.12 +  OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl
    3.13 +    (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
    3.14 +    >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
    3.15 +
    3.16 +val _ =
    3.17    OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl
    3.18      (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
    3.19      >> (fn (mode, args) => Specification.notation_cmd true mode args));

     4.1 --- a/src/Pure/Isar/specification.ML	Mon Mar 01 17:07:36 2010 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Mon Mar 01 17:09:42 2010 +0100
     4.3 @@ -42,6 +42,8 @@
     4.4      local_theory -> local_theory
     4.5    val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
     4.6      local_theory -> local_theory
     4.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     4.8 +  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     4.9    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    4.10    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    4.11    val theorems: string ->
    4.12 @@ -255,12 +257,24 @@
    4.13  
    4.14  (* notation *)
    4.15  
    4.16 +local
    4.17 +
    4.18 +fun gen_type_notation prep_type add mode args lthy =
    4.19 +  lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
    4.20 +
    4.21  fun gen_notation prep_const add mode args lthy =
    4.22    lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
    4.23  
    4.24 +in
    4.25 +
    4.26 +val type_notation = gen_type_notation (K I);
    4.27 +val type_notation_cmd = gen_type_notation (fn ctxt => ProofContext.read_type_name ctxt false);
    4.28 +
    4.29  val notation = gen_notation (K I);
    4.30  val notation_cmd = gen_notation (fn ctxt => ProofContext.read_const ctxt false);
    4.31  
    4.32 +end;
    4.33 +
    4.34  
    4.35  (* fact statements *)
    4.36