--- 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 {*
--- 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
*}
--- 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
--- 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
--- 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
--- 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) *}
--- 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 {*
--- 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
--- 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}
Binary file cookbook.pdf has changed