--- 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.\
--- 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.\
--- 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"
--- 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"
--- 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;
--- 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)