# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257175563 -3600
# Node ID e6f5833667797d17e2e47b5f009b5c5b64783b1a
# Parent  2494b5b7a85df395dc7098470cdd8ed3e57d9635
solved problem with mixfix.

diff -r 2494b5b7a85d -r e6f583366779 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Nov 02 12:47:00 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Nov 02 16:26:03 2009 +0100
@@ -255,8 +255,7 @@
 
 text {*
   Sometimes you want to print out a term together with some type information.
-  This can be achieved by setting the reference 
-  @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} 
+  This can be achieved by setting the reference @{ML_ind show_types in Syntax} 
   to @{ML true}.
 *}
 
@@ -271,7 +270,7 @@
 
   where @{text 1} and @{text x} are displayed with their type.
   Even more type information can be printed by setting 
-  @{ML_ind show_all_types} to @{ML true}. We obtain
+  @{ML_ind show_all_types in Syntax} to @{ML true}. We obtain
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
@@ -280,8 +279,8 @@
   "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
-  Other references that influence printing are @{ML_ind show_brackets} 
-  and @{ML_ind show_sorts}. 
+  Other references that influence printing are @{ML_ind show_brackets in Syntax} 
+  and @{ML_ind show_sorts in Syntax}. 
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)
diff -r 2494b5b7a85d -r e6f583366779 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Nov 02 12:47:00 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Nov 02 16:26:03 2009 +0100
@@ -781,11 +781,11 @@
   on. Since types are part of the inner syntax they are strings with some
   encoded information (see previous section). If a mixfix-syntax is
   present for a variable, then it is stored in the 
-  @{ML Mixfix}\footnote{FIXME: access to Mixfix data structure} data structure;
-  no syntax translation is indicated by @{ML_ind NoSyn}.
+  @{ML Mixfix} data structure; no syntax translation is indicated by @{ML_ind NoSyn in Syntax}.
 
   \begin{readmore}
-  The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+  The data structure for mixfix annotations are implemented in 
+  @{ML_file "Pure/Syntax/mixfix.ML"} and @{ML_file "Pure/Syntax/syntax.ML"}.
   \end{readmore}
 
   Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
diff -r 2494b5b7a85d -r e6f583366779 progtutorial.pdf
Binary file progtutorial.pdf has changed