# HG changeset patch # User Christian Urban # Date 1231976654 0 # Node ID 7b8c4fe235aad717ea39e8ec619da181f95bf2fd # Parent 14c3dd5ee2ad8091b679834e5d03bf235edfe9af added an antiquotation option [gray] for gray boxes around displays diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/FirstSteps.thy --- 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}" "(\x. ?P x) \ \x. ?P x"} - @{ML_response_fake [display] + @{ML_response_fake [display,gray] "@{thm allI}" "(\x. ?P x) \ \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 \}"}}. For example - @{ML_response [display] + @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} @@ -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 \}"} 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\", \) $ Free (\"x\", \), + @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} where an coercion is inserted in the second component and - @{ML_response [display] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" + @{ML_response [display,gray] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" "(Const (\"==>\", \) $ \ $ \, Const (\"==>\", \) $ \ $ \)"} - 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 \}"}. For example - @{ML_response_fake [display] "@{typ \"bool \ nat\"}" "bool \ nat"} + @{ML_response_fake [display,gray] "@{typ \"bool \ nat\"}" "bool \ 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 \ $ Abs (\"x\", Type (\"nat\",[]), Const \ $ (Free (\"S\",\) $ \) $ @@ -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 \ $ Abs (\"x\", \, Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ @@ -314,7 +312,7 @@ antiquotation @{text "@{const_name \}"} 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 \"} + @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \"} 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 \ Q \ Q \ 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 \ Q \ Q \ P\"} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Parsing.thy --- 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 (\,(Ident, \"hello\"),\), Token (\,(Space, \" \"),\), Token (\,(Ident, \"world\"),\)]"} @@ -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 (\,(Command, \"inductive\"),\), Token (\,(Keyword, \"|\"),\), @@ -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 \ False\"" "True \ False"} + @{ML_response_fake_both [display,gray] "foobar \"True \ False\"" "True \ False"} and see the proposition in the tracing buffer. @@ -774,13 +775,13 @@ If we now type @{text "foobar \"True \ True\""}, we obtain the following proof state: - @{ML_response_fake_both [display] "foobar \"True \ True\"" + @{ML_response_fake_both [display,gray] "foobar \"True \ True\"" "goal (1 subgoal): 1. True \ True"} and we can build the proof - @{text [display] "foobar \"True \ True\" + @{text [display,gray] "foobar \"True \ True\" apply(rule conjI) apply(rule TrueI)+ done"} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/Antiquotes.thy --- 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,\)\"}"} + @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\)\"}"} to obtain -@{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\)"} + @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\)"} 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 diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/Config.thy --- 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 diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/NamedThms.thy --- 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 diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/StoringData.thy --- 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"} *} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/TimeLimit.thy --- 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)" "\"} + @{ML_response_fake [display,gray] "ackermann (4, 12)" "\"} 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"} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Solutions.thy --- 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**)\""} *} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/antiquote_setup.ML --- 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 () diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/document/root.tex --- 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} diff -r 14c3dd5ee2ad -r 7b8c4fe235aa cookbook.pdf Binary file cookbook.pdf has changed