--- a/CookBook/Parsing.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -202,14 +202,12 @@
   we have to write:
 *}
 
-ML {* 
-fun p_followed_by_q p q r =
+ML{*fun p_followed_by_q p q r =
   let 
      val err_msg = (fn _ => p ^ " is not followed by " ^ q)
   in
     ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
-  end
-*}
+  end *}
 
 
 text {*
@@ -395,10 +393,8 @@
 
 *}
 
-ML {* 
-fun filtered_input str = 
-       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
-*}
+ML{*fun filtered_input str = 
+       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
 
 text {*
 
@@ -477,9 +473,7 @@
 
 *}
 
-ML {*
-fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
-*}
+ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *}
 
 text {*
 
@@ -520,14 +514,14 @@
 
 *}
 
-ML {*
+ML{*
   OuterParse.position
 *}
 
 
 section {* Parsing Inner Syntax *}
 
-ML {*
+ML{*
 let 
   val input = OuterSyntax.scan Position.none "0"
 in 
@@ -536,13 +530,13 @@
 
 *}
 
-ML {*
+ML{*
   OuterParse.opt_target
 *}
 
 text {* (FIXME funny output for a proposition) *}
 
-ML {*
+ML{*
   OuterParse.opt_target --
   OuterParse.fixes -- 
   OuterParse.for_fixes --
@@ -551,7 +545,7 @@
 
 *}
 
-ML {* OuterSyntax.command *}
+ML{* OuterSyntax.command *}
 
 section {* New Commands and Creating Keyword Files *}
 
@@ -566,14 +560,12 @@
   To keep things simple this command does nothing at all. On the ML-level it can be defined as
 *}
 
-ML {* 
-let
+ML{*let
   val do_nothing = Scan.succeed (Toplevel.theory I)
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.command "foobar" "description of foobar" kind do_nothing
-end 
-*}
+end *}
 
 text {*
   The function @{ML OuterSyntax.command} expects a name for the command, a
@@ -600,7 +592,7 @@
 
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{figure}[t]
-  \begin{boxedminipage}{\textwidth}\small
+  \begin{graybox}\small
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
@@ -614,7 +606,7 @@
 end"}\\
   \isa{\isacharverbatimclose}\\
   \isacommand{end}
-  \end{boxedminipage}
+  \end{graybox}
   \caption{The file @{text "Command.thy"} is necessary for generating a log 
   file. This log file enables Isabelle to generate a keyword file containing 
   the command \isacommand{foobar}.\label{fig:commandtheory}}
@@ -698,14 +690,12 @@
   If we now run the original code
 *}
 
-ML {*
-let
+ML{*let
   val do_nothing = Scan.succeed (Toplevel.theory I)
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.command "foobar" "description of foobar" kind do_nothing
-end 
-*}
+end *}
 
 text {*
   then we can make use of \isacommand{foobar}! Similarly with any other new command. 
@@ -727,15 +717,13 @@
   the tracing information and finally does nothing. For this we can write
 *}
 
-ML {* 
-let
+ML{*let
   val trace_prop = 
          OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
-end 
-*}
+end *}
 
 text {*
   Now we can type for example
@@ -759,7 +747,7 @@
   below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 
-ML %linenumbers {*let
+ML%linenumbers{*let
   fun set_up_thm str ctxt =
     let
       val prop = Syntax.read_prop ctxt str
@@ -774,8 +762,7 @@
   val kind = OuterKeyword.thy_goal
 in
   OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
-end 
-*}
+end *}
 
 text {*
   The function @{text set_up_thm} takes a string (the proposition) and a context.
@@ -1034,32 +1021,32 @@
 
 
 
-ML {*
+ML{*
   val toks = OuterSyntax.scan Position.none
    "theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ;
 *}
 
-ML {*
+ML{*
   print_depth 20 ;
 *}
 
-ML {*
+ML{*
   map OuterLex.text_of toks ;
 *}
 
-ML {*
+ML{*
   val proper_toks = filter OuterLex.is_proper toks ;
 *}  
 
-ML {*
+ML{*
   map OuterLex.kind_of proper_toks 
 *}
 
-ML {*
+ML{*
   map OuterLex.unparse proper_toks ;
 *}
 
-ML {*
+ML{*
   OuterLex.stopper
 *}