# HG changeset patch
# User wenzelm
# Date 1138620006 -3600
# Node ID e79ba49737f259045de0b11c28bb5d3e684f3acb
# Parent  99124f3beccfb3922733b0d5a47ad82c2204a7b0
'setup': no list type, support implicit setup;
tuned;

diff -r 99124f3beccf -r e79ba49737f2 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Jan 30 12:20:05 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Mon Jan 30 12:20:06 2006 +0100
@@ -399,7 +399,7 @@
 \end{matharray}
 
 \begin{rail}
-  'hide' ('(' 'open' ')')? name (nameref + )
+  'hide' ('(open)')? name (nameref + )
   ;
 \end{rail}
 
@@ -456,7 +456,9 @@
 \begin{rail}
   'use' name
   ;
-  ('ML' | MLcommand | MLsetup | 'setup') text
+  ('ML' | MLcommand | MLsetup) text
+  ;
+  'setup' text?
   ;
   methodsetup name '=' text text
   ;
@@ -480,9 +482,10 @@
   
 \item [$\isarkeyword{setup}~text$] changes the current theory context by
   applying $text$, which refers to an ML expression of type
-  \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
+  \texttt{theory~->~theory)}.  The $\isarkeyword{setup}$ command is the
   canonical way to initialize any object-logic specific tools and packages
-  written in ML.
+  written in ML.  If the $text$ is omitted, the setup value is taken from the
+  implicit context maintained via \verb,Context.add_setup,.
   
 \item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
   method in the current theory.  The given $text$ has to be an ML expression
@@ -544,7 +547,7 @@
 
 \begin{rail}
   ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
-  printasttranslation ) ('(' 'advanced' ')')? text;
+  printasttranslation ) ('(advanced)')? text;
 
   tokentranslation text
 \end{rail}
@@ -566,24 +569,24 @@
 \end{ttbox}
 
 In case that the $(advanced)$ option is given, the corresponding translation
-functions may depend on the signature of the current theory context.  This
-allows to implement advanced syntax mechanisms, as translations functions may
-refer to specific theory declarations and auxiliary data.
+functions may depend on the current theory context.  This allows to implement
+advanced syntax mechanisms, as translations functions may refer to specific
+theory declarations and auxiliary data.
 
 See also \cite[\S8]{isabelle-ref} for more information on the general concept
 of syntax transformations in Isabelle.
 
 \begin{ttbox}
 val parse_ast_translation:
-  (string * (Sign.sg -> ast list -> ast)) list
+  (string * (theory -> ast list -> ast)) list
 val parse_translation:
-  (string * (Sign.sg -> term list -> term)) list
+  (string * (theory -> term list -> term)) list
 val print_translation:
-  (string * (Sign.sg -> term list -> term)) list
+  (string * (theory -> term list -> term)) list
 val typed_print_translation:
-  (string * (Sign.sg -> bool -> typ -> term list -> term)) list
+  (string * (theory -> bool -> typ -> term list -> term)) list
 val print_ast_translation:
-  (string * (Sign.sg -> ast list -> ast)) list
+  (string * (theory -> ast list -> ast)) list
 \end{ttbox}