--- a/CookBook/FirstSteps.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/FirstSteps.thy Wed Jan 14 23:44:14 2009 +0000
@@ -68,14 +68,14 @@
in your code. This can be done in a ``quick-and-dirty'' fashion using
the function @{ML "warning"}. For example
- @{ML_response_fake [display] "warning \"any string\"" "\"any string\""}
+ @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
will print out @{text [quotes] "any string"} inside the response buffer
of Isabelle. This function expects a string as argument. If you develop under PolyML,
then there is a convenient, though again ``quick-and-dirty'', method for
converting values into strings, namely @{ML makestring}:
- @{ML_response_fake [display] "warning (makestring 1)" "\"1\""}
+ @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
However @{ML makestring} only works if the type of what is converted is monomorphic
and is not a function.
@@ -86,7 +86,7 @@
function @{ML tracing} is more appropriate. This function writes all output into
a separate tracing buffer. For example
- @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""}
+ @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
It is also possible to redirect the ``channel'' where the string @{text "foo"} is
printed to a separate file, e.g. to prevent ProofGeneral from choking on massive
@@ -107,10 +107,8 @@
TextIO.flushOut stream)) *}
text {*
-
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{text "foo.bar"}.
-
*}
@@ -124,7 +122,7 @@
theory by typing
- @{ML_response [display] "Context.theory_name @{theory}" "\"FirstSteps\""}
+ @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
where @{text "@{theory}"} is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
@@ -149,8 +147,8 @@
In a similar way you can use antiquotations to refer to theorems or simpsets:
- @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
- @{ML_response_fake [display]
+ @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+ @{ML_response_fake [display,gray]
"let
val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
in
@@ -186,7 +184,7 @@
One way to construct terms of Isabelle on the ML-level is by using the antiquotation
\mbox{@{text "@{term \<dots>}"}}. For example
- @{ML_response [display]
+ @{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
@@ -223,27 +221,27 @@
may omit parts of it by default. If you want to see all of it, you
can use the following ML function to set the limit to a value high
enough:
- \end{exercise}
@{ML [display] "print_depth 50"}
+ \end{exercise}
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
Consider for example the pairs
- @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
+ @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
where an coercion is inserted in the second component and
- @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
+ @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
- where it is not (since it is already constructed using the meta-implication).
+ where it is not (since it is already constructed by a meta-implication).
Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
- @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+ @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
@@ -283,7 +281,7 @@
to both functions. With @{ML make_imp} we obtain the correct term involving
@{term "S"}, @{text "T"} and @{text "@{typ nat}"}
- @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}"
+ @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
"Const \<dots> $
Abs (\"x\", Type (\"nat\",[]),
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
@@ -292,7 +290,7 @@
With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"}
and @{text "Q"} from the antiquotation.
- @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}"
+ @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
"Const \<dots> $
Abs (\"x\", \<dots>,
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
@@ -314,7 +312,7 @@
antiquotation @{text "@{const_name \<dots>}"} which does the expansion
automatically, for example:
- @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
+ @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
@@ -377,19 +375,19 @@
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
For example we can write
- @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+ @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
or use the antiquotation
- @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
+ @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
Attempting
- @{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+ @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
yields an error. A slightly more elaborate example is
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val natT = @{typ \"nat\"}
val zero = @{term \"0::nat\"}
@@ -426,7 +424,7 @@
application. This combinator, and several variants are defined in
@{ML_file "Pure/General/basics.ML"}.}
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val thy = @{theory}
@@ -497,6 +495,7 @@
Tactics are functions that map a goal state to a (lazy)
sequence of successor states, hence the type of a tactic is
+
@{ML_type[display] "thm -> thm Seq.seq"}
\begin{readmore}
@@ -531,7 +530,7 @@
goal is proved. The @{text "tac"} is the tactic which proves the goal and which
can make use of the local assumptions (there are none in this example).
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val ctxt = @{context}
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
@@ -552,7 +551,7 @@
An alternative way to transcribe this proof is as follows
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val ctxt = @{context}
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
--- a/CookBook/Parsing.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Parsing.thy Wed Jan 14 23:44:14 2009 +0000
@@ -42,13 +42,14 @@
return a pair consisting of this string and the rest of the input list.
For example:
- @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
- @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+ @{ML_response [display,gray] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+
+ @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
This function will either succeed (as in the two examples above) or raise the exception
@{text "FAIL"} if no string can be consumed. For example trying to parse
- @{ML_response_fake [display] "($$ \"x\") (explode \"world\")"
+ @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")"
"Exception FAIL raised"}
will raise the exception @{text "FAIL"}.
@@ -73,7 +74,7 @@
[quotes] "w"}:
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
val input1 = (explode \"hello\")
@@ -87,7 +88,7 @@
For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this
sequence can be achieved by
- @{ML_response [display] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
+ @{ML_response [display,gray] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
"(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
Note how the result of consumed strings builds up on the left as nested pairs.
@@ -95,7 +96,7 @@
If, as in the previous example, one wants to parse a particular string,
then one should use the function @{ML Scan.this_string}:
- @{ML_response [display] "Scan.this_string \"hell\" (explode \"hello\")"
+ @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")"
"(\"hell\", [\"o\"])"}
Parsers that explore alternatives can be constructed using the function @{ML
@@ -104,7 +105,7 @@
result of @{text "q"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val hw = ($$ \"h\") || ($$ \"w\")
val input1 = (explode \"hello\")
@@ -118,7 +119,7 @@
for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val just_e = ($$ \"h\") |-- ($$ \"e\")
val just_h = ($$ \"h\") --| ($$ \"e\")
@@ -132,7 +133,7 @@
@{text "p"}, if it succeeds; otherwise it returns
the default value @{text "x"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val p = Scan.optional ($$ \"h\") \"x\"
val input1 = (explode \"hello\")
@@ -145,7 +146,7 @@
The function @{ML Scan.option} works similarly, except no default value can
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val p = Scan.option ($$ \"h\")
val input1 = (explode \"hello\")
@@ -159,7 +160,7 @@
followed by @{text q}, or start a completely different parser @{text r},
one might write
- @{ML [display] "(p -- q) || r" for p q r}
+ @{ML [display,gray] "(p -- q) || r" for p q r}
However, this parser is problematic for producing an appropriate error message, in case
the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information
@@ -174,24 +175,24 @@
can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of
parsing in case of a failure and prints an error message. For example if we invoke the parser
- @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
+ @{ML [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
on @{text [quotes] "hello"}, the parsing succeeds
- @{ML_response [display]
+ @{ML_response [display,gray]
"(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")"
"(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
but if we invoke it on @{text [quotes] "world"}
- @{ML_response_fake [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
+ @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
"Exception ABORT raised"}
then the parsing aborts and the error message @{text "foo"} is printed out. In order to
see the error message properly, we need to prefix the parser with the function
@{ML "Scan.error"}. For example
- @{ML_response_fake [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
+ @{ML_response_fake [display,gray] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
"Exception Error \"foo\" raised"}
This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"}
@@ -214,12 +215,12 @@
Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and
the input @{text [quotes] "holle"}
- @{ML_response_fake [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
+ @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
"Exception ERROR \"h is not followed by e\" raised"}
produces the correct error message. Running it with
- @{ML_response [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")"
+ @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")"
"((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
yields the expected parsing.
@@ -227,7 +228,7 @@
The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as
often as it succeeds. For example
- @{ML_response [display] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")"
+ @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function
@@ -239,7 +240,7 @@
the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With
them we can write
- @{ML_response [display] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
+ @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
@{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;
@@ -249,7 +250,7 @@
The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any
string as in
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof)
val input = (explode \"foo bar foo\")
@@ -264,12 +265,12 @@
The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
- @{ML_response_fake_both [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
+ @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
"Exception FAIL raised"}
fails, while
- @{ML_response [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"world\")"
+ @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"world\")"
"(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
succeeds.
@@ -278,7 +279,7 @@
input until a certain marker symbol is reached. In the example below the marker
symbol is a @{text [quotes] "*"}.
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
val input1 = (explode \"fooooo\")
@@ -295,7 +296,7 @@
first the parser @{text p} and upon successful completion applies the
function @{text f} to the result. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
fun double (x,y) = (x^x,y^y)
in
@@ -305,7 +306,7 @@
doubles the two parsed input strings. Or
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
val input = (explode \"foo bar foo\")
@@ -330,7 +331,7 @@
the given parser to the second component of the pair and leaves the first component
untouched. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
@@ -365,7 +366,7 @@
generating precise error messages. The following
-@{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\""
+@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
"[Token (\<dots>,(Ident, \"hello\"),\<dots>),
Token (\<dots>,(Space, \" \"),\<dots>),
Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
@@ -381,7 +382,7 @@
functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val input = OuterSyntax.scan Position.none \"hello world\"
in
@@ -400,7 +401,7 @@
If we parse
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"filtered_input \"inductive | for\""
"[Token (\<dots>,(Command, \"inductive\"),\<dots>),
Token (\<dots>,(Keyword, \"|\"),\<dots>),
@@ -411,7 +412,7 @@
the following (you might have to adjust the @{ML print_depth} in order to
see the complete list):
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val (keywords, commands) = OuterKeyword.get_lexicons ()
in
@@ -421,7 +422,7 @@
Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input1 = filtered_input \"where for\"
val input2 = filtered_input \"| in\"
@@ -432,7 +433,7 @@
Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"| in\"
in
@@ -444,7 +445,7 @@
list of items recognised by the parser @{text p}, where the items being parsed
are separated by the string @{text s}. For example
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"in | in | in foo\"
in
@@ -460,7 +461,7 @@
Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
OuterLex.stopper}. We can write
-@{ML_response [display]
+@{ML_response [display,gray]
"let
val input = filtered_input \"in | in | in\"
in
@@ -482,7 +483,7 @@
except that the error message is fixed to be @{text [quotes] "Outer syntax error"}
with a relatively precise description of the failure. For example:
-@{ML_response_fake [display]
+@{ML_response_fake [display,gray]
"let
val input = filtered_input \"in |\"
val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
@@ -728,7 +729,7 @@
text {*
Now we can type for example
- @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
+ @{ML_response_fake_both [display,gray] "foobar \"True \<and> False\"" "True \<and> False"}
and see the proposition in the tracing buffer.
@@ -774,13 +775,13 @@
If we now type @{text "foobar \"True \<and> True\""}, we obtain the following
proof state:
- @{ML_response_fake_both [display] "foobar \"True \<and> True\""
+ @{ML_response_fake_both [display,gray] "foobar \"True \<and> True\""
"goal (1 subgoal):
1. True \<and> True"}
and we can build the proof
- @{text [display] "foobar \"True \<and> True\"
+ @{text [display,gray] "foobar \"True \<and> True\"
apply(rule conjI)
apply(rule TrueI)+
done"}
--- a/CookBook/Recipes/Antiquotes.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy Wed Jan 14 23:44:14 2009 +0000
@@ -4,8 +4,6 @@
begin
-
-
section {* Useful Document Antiquotations *}
text {*
@@ -90,7 +88,7 @@
hints what the result of the ML-code should be and to check the consistency of
the actual result with these hints. For this we are going to implement the
antiquotation
- @{text "@{ML_response \"expr\" \"pat\"}"}
+ @{text "@{ML_resp \"expr\" \"pat\"}"}
whose first argument is the ML-code and the second is a pattern specifying
the result. To add some convenience and allow dealing with large outputs,
the user can give a partial specification including abbreviations
@@ -117,41 +115,43 @@
*}
-ML{*fun add_response_indicator pat =
+ML{*fun add_resp_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_resp 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)
+ val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
in
ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output
end)
val _ = ThyOutput.add_commands
- [("ML_response",
+ [("ML_resp",
ThyOutput.args
(Scan.lift (OuterParse.position (Args.name -- Args.name)))
- output_ml_response)]*}
+ output_ml_resp)]*}
text {*
- This extended antiquotation allows us to write
- @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"}
+ This extended antiquotation allows us to write
+
+ @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
+
to obtain
-@{ML_response [display] "true andalso false" "false"}
+ @{ML_resp [display] "true andalso false" "false"}
or
-@{text [display] "@{ML_response [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"}
+ @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"}
to obtain
-@{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"}
+ @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"}
In both cases, the check by the compiler ensures that code and result match. A limitation
of this antiquotation is that the hints can only be given for results that can actually
--- a/CookBook/Recipes/Config.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/Config.thy Wed Jan 14 23:44:14 2009 +0000
@@ -43,13 +43,13 @@
On the ML-level these values can be retrieved using the
function @{ML Config.get}:
- @{ML_response [display] "Config.get @{context} bval" "true"}
+ @{ML_response [display,gray] "Config.get @{context} bval" "true"}
- @{ML_response [display] "Config.get @{context} ival" "3"}
+ @{ML_response [display,gray] "Config.get @{context} ival" "3"}
The function @{ML Config.put} manipulates the values. For example
- @{ML_response [display] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
+ @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
The same can be achived using the command \isacommand{setup}.
*}
@@ -59,12 +59,12 @@
text {*
The retrival of this value yields now
- @{ML_response [display] "Config.get @{context} sval" "\"bar\""}
+ @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
We can apply a function to a value using @{ML Config.map}. For example incrementing
@{ML ival} can be done by
- @{ML_response [display]
+ @{ML_response [display,gray]
"let
val ctxt = Config.map ival (fn i => i + 1) @{context}
in
--- a/CookBook/Recipes/NamedThms.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy Wed Jan 14 23:44:14 2009 +0000
@@ -48,14 +48,14 @@
text {* and query the remaining ones with:
-@{ML_response_fake_both [display] "thm foo"
+@{ML_response_fake_both [display,gray] "thm foo"
"?C
?B"}
On the ML-level the rules marked with @{text "foo"} an be retrieved
using the function @{ML FooRules.get}:
- @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
+ @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
\begin{readmore}
For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
--- a/CookBook/Recipes/StoringData.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy Wed Jan 14 23:44:14 2009 +0000
@@ -34,7 +34,7 @@
text {*
- @{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"}
+ @{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"}
*}
--- a/CookBook/Recipes/TimeLimit.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy Wed Jan 14 23:44:14 2009 +0000
@@ -23,12 +23,12 @@
Now the call
- @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
+ @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
takes a bit of time before it finishes. To avoid this, the call can be encapsulated
in a time limit of five seconds. For this you have to write:
-@{ML_response [display]
+@{ML_response [display,gray]
"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12)
handle TimeOut => ~1"
"~1"}
--- a/CookBook/Solutions.thy Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Solutions.thy Wed Jan 14 23:44:14 2009 +0000
@@ -41,9 +41,9 @@
@{ML scan_all} retruns a string, instead of the pair a parser would
normally return. For example:
- @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""}
+ @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""}
- @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")"
+ @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")"
"\"foo (**test**) bar (**test**)\""}
*}
--- a/CookBook/antiquote_setup.ML Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/antiquote_setup.ML Wed Jan 14 23:44:14 2009 +0000
@@ -3,6 +3,36 @@
structure AntiquoteSetup: sig end =
struct
+(* rebuilding the output_list function from ThyOutput in order to *)
+(* enable the option [gray] *)
+
+val gray = ref false;
+
+fun boolean "" = true
+ | boolean "true" = true
+ | boolean "false" = false
+ | boolean s = error ("Bad boolean value: " ^ quote s);
+
+fun output_list pretty src ctxt xs =
+ map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
+ |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I)
+ |> (if ! ThyOutput.quotes then map Pretty.quote else I)
+ |> (if ! ThyOutput.display then
+ map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
+ #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else
+ (*map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))*)
+ map (Output.output o Pretty.str_of)
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> enclose "\\isa{" "}");
+
+val _ = ThyOutput.add_options
+ [("gray", Library.setmp gray o boolean)]
+
+
+(* main body *)
fun ml_val_open (ys, xs) txt =
let fun ml_val_open_aux ys txt =
"fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
@@ -29,7 +59,7 @@
fun output_ml ml src ctxt ((txt,ovars),pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
txt |> transform_cmts_str |> space_explode "\n" |>
- ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt)
+ output_list (fn _ => fn s => Pretty.str s) src ctxt)
fun output_ml_aux ml src ctxt (txt,pos) =
output_ml (K ml) src ctxt ((txt,()),pos)
@@ -41,16 +71,16 @@
(ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
let
val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
- in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+ in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml lhs);
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
- in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+ in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) =
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
- in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+ in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
fun check_file_exists ctxt txt =
if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
--- a/CookBook/document/root.tex Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/document/root.tex Wed Jan 14 23:44:14 2009 +0000
@@ -35,7 +35,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% sane default for proof documents
-\parindent 0pt\parskip 0.7ex
+\parindent 0pt\parskip 0.6ex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hyphenation{Isabelle}
@@ -59,7 +59,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% this is to draw a gray box around code
\makeatletter\newenvironment{graybox}{%
- \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
+ \begin{lrbox}{\@tempboxa}\begin{minipage}{0.985\textwidth}}{\end{minipage}\end{lrbox}%
\colorbox{gray!10}{\usebox{\@tempboxa}}
}\makeatother
@@ -72,19 +72,22 @@
\renewcommand{\isacharverbatimclose}{}}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for code
\isakeeptag{CookBookML}
-\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
-\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
+\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{isabelle}\begin{graybox}}
+\renewcommand{\endisatagCookBookML}{\end{graybox}\end{isabelle}\end{vanishML}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% for line numbers
+% for code that has line numbers
\isakeeptag{linenumbers}
\renewcommand{\isataglinenumbers}
-{\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
+{\begin{vanishML}\begin{isabelle}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{isabelle}\end{vanishML}}
-
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\small\item\relax}
+{\end{isabellebody}\end{trivlist}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
Binary file cookbook.pdf has changed