Pure: command 'no_syntax' removes grammar declarations;
authorwenzelm
Sat Apr 16 18:55:28 2005 +0200 (2005-04-16)
changeset 15744daa84ebbdf94
parent 15743 814eed210b82
child 15745 33bb955b2e73
Pure: command 'no_syntax' removes grammar declarations;
NEWS
doc-src/IsarRef/pure.tex
     1.1 --- a/NEWS	Sat Apr 16 18:54:44 2005 +0200
     1.2 +++ b/NEWS	Sat Apr 16 18:55:28 2005 +0200
     1.3 @@ -17,10 +17,9 @@
     1.4    means that function like Library.hd and Library.tl are gone, as the
     1.5    standard hd and tl functions suffice.
     1.6  
     1.7 -  A number of functions, specifically those in the LIBRARY_CLOSED
     1.8 -  signature, are now no longer exported to the top ML level, as they
     1.9 -  are variants of standard functions.  The following suggests how
    1.10 -  one can translate existing code:
    1.11 +  A number of basic functions are now no longer exported to the top ML
    1.12 +  level, as they are variants of standard functions.  The following
    1.13 +  suggests how one can translate existing code:
    1.14  
    1.15      the x = valOf x
    1.16      if_none x y = getOpt(x,y)
    1.17 @@ -108,6 +107,10 @@
    1.18    'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
    1.19    object-logic specifications.
    1.20  
    1.21 +* Pure: command 'no_syntax' removes grammar declarations (and
    1.22 +  translations) resulting from the given syntax specification, which
    1.23 +  is interpreted in the same manner as for the 'syntax' command.
    1.24 +
    1.25  * Pure: print_tac now outputs the goal through the trace channel.
    1.26  
    1.27  * Pure: reference Namespace.unique_names included.  If true the
     2.1 --- a/doc-src/IsarRef/pure.tex	Sat Apr 16 18:54:44 2005 +0200
     2.2 +++ b/doc-src/IsarRef/pure.tex	Sat Apr 16 18:55:28 2005 +0200
     2.3 @@ -295,9 +295,10 @@
     2.4  
     2.5  \subsection{Syntax and translations}\label{sec:syn-trans}
     2.6  
     2.7 -\indexisarcmd{syntax}\indexisarcmd{translations}
     2.8 +\indexisarcmd{syntax}\indexisarcmd{no-syntax}\indexisarcmd{translations}
     2.9  \begin{matharray}{rcl}
    2.10    \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
    2.11 +  \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\
    2.12    \isarcmd{translations} & : & \isartrans{theory}{theory} \\
    2.13  \end{matharray}
    2.14  
    2.15 @@ -310,11 +311,17 @@
    2.16  \railalias{leftharpoondown}{\isasymleftharpoondown}
    2.17  \railterm{leftharpoondown}
    2.18  
    2.19 +\railalias{nosyntax}{no\_syntax}
    2.20 +\railterm{nosyntax}
    2.21 +
    2.22  \begin{rail}
    2.23 -  'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
    2.24 +  ('syntax' | nosyntax) mode? (constdecl +)
    2.25    ;
    2.26    'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    2.27    ;
    2.28 +
    2.29 +  mode: ('(' ( name | 'output' | name 'output' ) ')')
    2.30 +  ;
    2.31    transpat: ('(' nameref ')')? string
    2.32    ;
    2.33  \end{rail}
    2.34 @@ -329,6 +336,10 @@
    2.35    $\isarkeyword{output}$ indicator is given, all productions are added both to
    2.36    the input and output grammar.
    2.37    
    2.38 +\item [$\isarkeyword{no_syntax}~(mode)~decls$] removes grammar declarations
    2.39 +  (and translations) resulting from $decls$, which are interpreted in the same
    2.40 +  manner as for $\isarkeyword{syntax}$ above.
    2.41 +  
    2.42  \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
    2.43    rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
    2.44    rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).