# HG changeset patch
# User wenzelm
# Date 1113670528 -7200
# Node ID daa84ebbdf94124666d2dd0e8667e3ee2ab3ce56
# Parent  814eed210b82780ff8b80a9b9c95a2763a775491
Pure: command 'no_syntax' removes grammar declarations;

diff -r 814eed210b82 -r daa84ebbdf94 NEWS
--- a/NEWS	Sat Apr 16 18:54:44 2005 +0200
+++ b/NEWS	Sat Apr 16 18:55:28 2005 +0200
@@ -17,10 +17,9 @@
   means that function like Library.hd and Library.tl are gone, as the
   standard hd and tl functions suffice.
 
-  A number of functions, specifically those in the LIBRARY_CLOSED
-  signature, are now no longer exported to the top ML level, as they
-  are variants of standard functions.  The following suggests how
-  one can translate existing code:
+  A number of basic functions are now no longer exported to the top ML
+  level, as they are variants of standard functions.  The following
+  suggests how one can translate existing code:
 
     the x = valOf x
     if_none x y = getOpt(x,y)
@@ -108,6 +107,10 @@
   'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
   object-logic specifications.
 
+* Pure: command 'no_syntax' removes grammar declarations (and
+  translations) resulting from the given syntax specification, which
+  is interpreted in the same manner as for the 'syntax' command.
+
 * Pure: print_tac now outputs the goal through the trace channel.
 
 * Pure: reference Namespace.unique_names included.  If true the
diff -r 814eed210b82 -r daa84ebbdf94 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Apr 16 18:54:44 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Sat Apr 16 18:55:28 2005 +0200
@@ -295,9 +295,10 @@
 
 \subsection{Syntax and translations}\label{sec:syn-trans}
 
-\indexisarcmd{syntax}\indexisarcmd{translations}
+\indexisarcmd{syntax}\indexisarcmd{no-syntax}\indexisarcmd{translations}
 \begin{matharray}{rcl}
   \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
+  \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\
   \isarcmd{translations} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
@@ -310,11 +311,17 @@
 \railalias{leftharpoondown}{\isasymleftharpoondown}
 \railterm{leftharpoondown}
 
+\railalias{nosyntax}{no\_syntax}
+\railterm{nosyntax}
+
 \begin{rail}
-  'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
+  ('syntax' | nosyntax) mode? (constdecl +)
   ;
   'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   ;
+
+  mode: ('(' ( name | 'output' | name 'output' ) ')')
+  ;
   transpat: ('(' nameref ')')? string
   ;
 \end{rail}
@@ -329,6 +336,10 @@
   $\isarkeyword{output}$ indicator is given, all productions are added both to
   the input and output grammar.
   
+\item [$\isarkeyword{no_syntax}~(mode)~decls$] removes grammar declarations
+  (and translations) resulting from $decls$, which are interpreted in the same
+  manner as for $\isarkeyword{syntax}$ above.
+  
 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
   rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
   rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).