# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1231955269 0
# Node ID 19106a9975c1eb51d18661bccbbac7b436353193
# Parent  e7519207c2b7adaf9ae4e750ce26e62b1aca7de2
highligted the background of ML-code

diff -r e7519207c2b7 -r 19106a9975c1 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -93,8 +93,7 @@
   amounts of trace output. This redirection can be achieved using the code
 *}
 
-ML{* 
-val strip_specials =
+ML{*val strip_specials =
 let
   fun strip ("\^A" :: _ :: cs) = strip cs
     | strip (c :: cs) = c :: strip cs
@@ -105,8 +104,7 @@
  Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
      TextIO.output (stream, "\n");
-     TextIO.flushOut stream)); 
-*}
+     TextIO.flushOut stream)) *}
 
 text {*
 
@@ -137,9 +135,7 @@
   determined at ``compile-time'', not ``run-time''. For example the function
 *}
 
-ML {*
-fun not_current_thyname () = Context.theory_name @{theory}
-*}
+ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 
 text {*
 
@@ -163,9 +159,7 @@
   avoid explicit bindings for theorems such as
 *}
 
-ML {*
-val allI = thm "allI"
-*}
+ML{*val allI = thm "allI" *}
 
 text {*
   These bindings were difficult to maintain and also could accidentally
@@ -261,13 +255,11 @@
   as arguments can only be written as
 *}
 
-ML {*
-fun make_imp P Q tau =
+ML{*fun make_imp P Q tau =
   let
     val x = Free ("x",tau)
   in Logic.all x (Logic.mk_implies (P $ x, Q $ x))
-  end
-*}
+  end *}
 
 text {*
 
@@ -275,9 +267,7 @@
   @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
 
-ML {*
-fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
-*}
+ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
 
 text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
@@ -323,17 +313,13 @@
 
 *} 
 
-ML {*
-fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
-*}
+ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
 
 text {*
   which can be equally written as 
 *}
 
-ML {*
-fun make_fun_type tau1 tau2 = tau1 --> tau2
-*}
+ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
 
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Parsing.thy
--- 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
 *}
 
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/Antiquotes.thy
--- a/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -32,7 +32,7 @@
 
 *}
 
-ML %linenumbers {*fun ml_val code_txt = "val _ = " ^ code_txt
+ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml src ctxt code_txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
@@ -40,8 +40,7 @@
                                             (space_explode "\n" code_txt))
 
 val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]
-*}
+ [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*}
 
 text {*
 
@@ -68,15 +67,14 @@
 
 *}
 
-ML %linenumbers {* fun output_ml src ctxt (code_txt,pos) =
+ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
                                             (space_explode "\n" code_txt))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args 
-       (Scan.lift (OuterParse.position Args.name)) output_ml)]
-*}
+       (Scan.lift (OuterParse.position Args.name)) output_ml)] *}
 
 text {*
   where in Lines 1 and 2 the positional information is properly treated.
@@ -107,31 +105,26 @@
 
 *}
 
-ML {* 
-fun ml_pat (code_txt, pat) =
+ML{*fun ml_pat (code_txt, pat) =
    let val pat' = 
          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
    in 
      "val " ^ pat' ^ " = " ^ code_txt 
-   end
-*}
+   end*}
 
 text {* 
   Next we like to add a response indicator to the result using:
 *}
 
 
-ML {*
-fun add_response_indicator pat =
-  map (fn s => "> " ^ s) (space_explode "\n" pat)
-*}
+ML{*fun add_response_indicator pat =
+  map (fn s => "> " ^ s) (space_explode "\n" pat) *}
 
 text {* 
   The rest of the code of the antiquotation is
   *}
 
-ML {*
-fun output_ml_response src ctxt ((code_txt,pat),pos) = 
+ML{*fun output_ml_response src ctxt ((code_txt,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat));
    let 
      val output = (space_explode "\n" code_txt) @ (add_response_indicator pat)
@@ -143,8 +136,7 @@
  [("ML_response", 
      ThyOutput.args 
       (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-        output_ml_response)]
-*}
+        output_ml_response)]*}
 
 text {*
   This extended antiquotation allows us to write 
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/Config.thy
--- a/CookBook/Recipes/Config.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -17,11 +17,9 @@
   containing a string. These values can be declared on the ML-level with
 *}
 
-ML {*
-val (bval, setup_bval) = Attrib.config_bool "bval" false
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
 val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string"
-*}
+val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
 
 text {* 
   where each value needs to be given a default. To enable these values, they need to 
@@ -33,9 +31,7 @@
 
 text {* or on the ML-level *}
 
-ML {*
-setup_sval @{theory} 
-*}
+ML{*setup_sval @{theory} *}
 
 text {*
   The user can now manipulate the values from within Isabelle with the command
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -17,11 +17,9 @@
 
   *}
 
-ML {*
-structure FooRules = NamedThmsFun (
+ML{*structure FooRules = NamedThmsFun (
   val name = "foo" 
-  val description = "Rules for foo");
-*}
+  val description = "Rules for foo"); *}
 
 text {*
   and the command
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/StoringData.thy
--- a/CookBook/Recipes/StoringData.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -16,8 +16,7 @@
 
   *}
 
-ML {* 
-local
+ML{*local
 
 structure Data = GenericDataFun
  ( type T = int Symtab.table
@@ -27,11 +26,8 @@
  )
 
 in
-
-val lookup = Symtab.lookup o Data.get
-
-fun update k v = Data.map (Symtab.update (k, v))
-
+ val lookup = Symtab.lookup o Data.get
+ fun update k v = Data.map (Symtab.update (k, v))
 end *}
 
 setup {* Context.theory_map (update "foo" 1) *}
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -15,11 +15,9 @@
 
   *}
 
-ML {* 
-fun ackermann (0, n) = n + 1
+ML{*fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
-  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))
-*}
+  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
 text {*
 
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -6,27 +6,22 @@
 
 text {* \solution{fun:revsum} *}
 
-ML {* 
-fun rev_sum t =
+ML{*fun rev_sum t =
 let
  fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
    | dest_sum u = [u]
  in
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
- end;
-*}
+ end *}
 
 text {* \solution{fun:makesum} *}
 
-ML {*
-fun make_sum t1 t2 =
-    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
-*}
+ML{*fun make_sum t1 t2 =
+    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 text {* \solution{ex:scancmts} *}
 
-ML {*
-val any = Scan.one (Symbol.not_eof);
+ML{*val any = Scan.one (Symbol.not_eof);
 
 val scan_cmt =
   let
@@ -39,8 +34,7 @@
 
 val scan_all =
   Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) 
-    >> implode #> fst 
-*}
+    >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function 
diff -r e7519207c2b7 -r 19106a9975c1 CookBook/document/root.tex
--- a/CookBook/document/root.tex	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/document/root.tex	Wed Jan 14 17:47:49 2009 +0000
@@ -12,6 +12,7 @@
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
 \usepackage{lineno}
 \usepackage{boxedminipage}
+\usepackage{xcolor}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
@@ -73,19 +74,26 @@
 \newenvironment{vanishML}{%
 \renewcommand{\isacommand}[1]{}%
 \renewcommand{\isacharverbatimopen}{}%
-\renewcommand{\isacharverbatimclose}{}%
-\hspace{-1.5mm}\mbox{}}{}
+\renewcommand{\isacharverbatimclose}{}}{}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\makeatletter\newenvironment{graybox}{%
+   \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
+   \colorbox{gray!5}{\usebox{\@tempboxa}}
+}\makeatother
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \isakeeptag{CookBookML}
-\renewcommand{\isatagCookBookML}{\begin{vanishML}}
-\renewcommand{\endisatagCookBookML}{\end{vanishML}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
+\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for line numbers
 \isakeeptag{linenumbers}
-\renewcommand{\isataglinenumbers}{\begin{vanishML}\begingroup\resetlinenumber\linenumbers}
-\renewcommand{\endisataglinenumbers}{\endgroup\end{vanishML}}
+\renewcommand{\isataglinenumbers}
+{\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{document}
diff -r e7519207c2b7 -r 19106a9975c1 cookbook.pdf
Binary file cookbook.pdf has changed