# HG changeset patch
# User wenzelm
# Date 1290957331 -3600
# Node ID 177e8cea3e099142cc252ac2860cb95e62f69d06
# Parent  21f7e8d66a393d2b1ef83f51a45d94282659619c
added 'syntax_declaration' command;

diff -r 21f7e8d66a39 -r 177e8cea3e09 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 15:34:35 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 16:15:31 2010 +0100
@@ -253,11 +253,12 @@
 
   \begin{matharray}{rcl}
     @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   \begin{rail}
-    'declaration' ('(pervasive)')? target? text
+    ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
     ;
     'declare' target? (thmrefs + 'and')
     ;
@@ -275,6 +276,10 @@
   declaration is applied to all possible contexts involved, including
   the global background theory.
 
+  \item @{command "syntax_declaration"} is similar to @{command
+  "declaration"}, but is meant to affect only ``syntactic'' tools by
+  convention (such as notation and type-checking information).
+
   \item @{command "declare"}~@{text thms} declares theorems to the
   current local theory context.  No theorem binding is involved here,
   unlike @{command "theorems"} or @{command "lemmas"} (cf.\
diff -r 21f7e8d66a39 -r 177e8cea3e09 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 15:34:35 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 28 16:15:31 2010 +0100
@@ -273,11 +273,12 @@
 
   \begin{matharray}{rcl}
     \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
   \end{matharray}
 
   \begin{rail}
-    'declaration' ('(pervasive)')? target? text
+    ('declaration' | 'syntax_declaration') ('(pervasive)')? target? text
     ;
     'declare' target? (thmrefs + 'and')
     ;
@@ -295,6 +296,9 @@
   declaration is applied to all possible contexts involved, including
   the global background theory.
 
+  \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by
+  convention (such as notation and type-checking information).
+
   \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
   current local theory context.  No theorem binding is involved here,
   unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
diff -r 21f7e8d66a39 -r 177e8cea3e09 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Nov 28 15:34:35 2010 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Nov 28 16:15:31 2010 +0100
@@ -172,6 +172,7 @@
     "subsubsect"
     "subsubsection"
     "syntax"
+    "syntax_declaration"
     "term"
     "text"
     "text_raw"
@@ -395,6 +396,7 @@
     "setup"
     "simproc_setup"
     "syntax"
+    "syntax_declaration"
     "text"
     "text_raw"
     "theorems"
diff -r 21f7e8d66a39 -r 177e8cea3e09 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Nov 28 15:34:35 2010 +0100
+++ b/etc/isar-keywords.el	Sun Nov 28 16:15:31 2010 +0100
@@ -230,6 +230,7 @@
     "subsubsect"
     "subsubsection"
     "syntax"
+    "syntax_declaration"
     "term"
     "termination"
     "text"
@@ -508,6 +509,7 @@
     "sledgehammer_params"
     "statespace"
     "syntax"
+    "syntax_declaration"
     "text"
     "text_raw"
     "theorems"
diff -r 21f7e8d66a39 -r 177e8cea3e09 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 28 15:34:35 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 28 16:15:31 2010 +0100
@@ -16,7 +16,8 @@
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
-  val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
+  val declaration: {syntax: bool, pervasive: bool} ->
+    Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
   val hide_class: bool -> xstring list -> theory -> theory
@@ -180,11 +181,13 @@
 
 (* declarations *)
 
-fun declaration pervasive (txt, pos) =
+fun declaration {syntax, pervasive} (txt, pos) =
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
-    ("Context.map_proof (Local_Theory.declaration " ^ Bool.toString pervasive ^ " declaration)")
+    ("Context.map_proof (Local_Theory." ^
+      (if syntax then "syntax_declaration" else "declaration") ^ " " ^
+      Bool.toString pervasive ^ " declaration)")
   |> Context.proof_map;
 
 
diff -r 21f7e8d66a39 -r 177e8cea3e09 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 28 15:34:35 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 28 16:15:31 2010 +0100
@@ -325,8 +325,16 @@
       >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
-  Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
+  Outer_Syntax.local_theory "declaration" "generic ML declaration"
+    (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.opt_keyword "pervasive" -- Parse.ML_source
+      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
+
+val _ =
+  Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
+    (Keyword.tag_ml Keyword.thy_decl)
+    (Parse.opt_keyword "pervasive" -- Parse.ML_source
+      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
 
 val _ =
   Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)