diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,16 +2,6 @@
 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
 begin
 
-(*<*)
-setup {*
-open_file_with_prelude 
-"Parsing_Code.thy"
-["theory Parsing", 
- "imports Base \"Package/Simple_Inductive_Package\"", 
- "begin"]
-*}
-(*>*)
-
 chapter {* Parsing\label{chp:parsing} *}
 
 text {*
@@ -253,7 +243,7 @@
   of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
 *}
 
-ML{*fun p_followed_by_q p q r =
+ML %grayML{*fun p_followed_by_q p q r =
 let 
   val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
@@ -389,7 +379,7 @@
   datatype:
 *}
 
-ML{*datatype tree = 
+ML %grayML{*datatype tree = 
     Lf of string 
   | Br of tree * tree*}
 
@@ -399,7 +389,7 @@
   leaf---you might implement the following parser.
 *}
 
-ML{*fun parse_basic s = 
+ML %grayML{*fun parse_basic s = 
   $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"  
 
 and parse_tree s = 
@@ -434,7 +424,7 @@
   as follows.
 *}
 
-ML{*fun parse_basic s xs = 
+ML %grayML{*fun parse_basic s xs = 
   ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs 
 
 and parse_tree s xs = 
@@ -472,7 +462,7 @@
   tokens, not strings.  These token parsers have the type:
 *}
   
-ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
+ML %grayML{*type 'a parser = Token.T list -> 'a * Token.T list*}
 
 text {*
   {\bf REDO!!}
@@ -512,7 +502,7 @@
   @{ML_ind define in Keyword}. For example calling it with 
 *}
 
-ML{*val _ = Keyword.define ("hello", NONE) *}
+ML %grayML{*val _ = Keyword.define ("hello", NONE) *}
 
 text {*
   then lexing @{text [quotes] "hello world"} will produce
@@ -538,7 +528,7 @@
   For convenience we define the function:
 *}
 
-ML{*fun filtered_input str = 
+ML %grayML{*fun filtered_input str = 
   filter Token.is_proper (Outer_Syntax.scan Position.none str) *}
 
 text {* 
@@ -630,7 +620,7 @@
   The following function will help to run examples.
 *}
 
-ML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
+ML %grayML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
 
 text {*
   The function @{ML_ind "!!!" in Parse} can be used to force termination
@@ -665,7 +655,7 @@
   modify the function @{ML filtered_input}, described earlier, as follows 
 *}
 
-ML{*fun filtered_input' str = 
+ML %grayML{*fun filtered_input' str = 
        filter Token.is_proper (Outer_Syntax.scan (Position.line 7) str) *}
 
 text {*
@@ -959,7 +949,7 @@
   defined as:
 *}
 
-ML{*let
+ML %grayML{*let
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
   val kind = Keyword.thy_decl
 in
@@ -1104,7 +1094,7 @@
   the function @{ML_ind define in Keyword}. For example:
 *}
 
-ML{*val _ = Keyword.define ("blink", NONE) *}
+ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
 
 text {*
   At the moment the command \isacommand{foobar} is not very useful. Let us
@@ -1121,7 +1111,7 @@
   finally does nothing. For this you can write:
 *}
 
-ML{*let
+ML %grayML{*let
   fun trace_prop str = 
      Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 
@@ -1214,7 +1204,7 @@
 val result_cookie = (Result.get, Result.put, "Result.put")
 *}
 
-ML{*let
+ML %grayML{*let
    fun after_qed thm_name thms lthy =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd