# HG changeset patch # User Christian Urban # Date 1309249320 -3600 # Node ID f65b9f14d5dead2e486a7aae18df7b3541d7b8bd # Parent 817ecad4cf722614b424d8f94c744040c16df213 updated to new Isabelle diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/Advanced.thy Tue Jun 28 09:22:00 2011 +0100 @@ -287,7 +287,6 @@ *} text {* - @{ML_ind "Binding.str_of"} returns the string with markup; @{ML_ind "Binding.name_of"} returns the string without markup @{ML_ind "Binding.conceal"} diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/Base.thy Tue Jun 28 09:22:00 2011 +0100 @@ -150,5 +150,7 @@ use "output_tutorial.ML" use "antiquote_setup.ML" +setup {* OutputTutorial.setup *} +setup {* AntiquoteSetup.setup *} end \ No newline at end of file diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/First_Steps.thy Tue Jun 28 09:22:00 2011 +0100 @@ -852,7 +852,8 @@ for the antiquotation @{text "term_pat"} is as follows. *} -ML %linenosgray{*let +ML %linenosgray{*val term_pat_setup = +let val parser = Args.context -- Scan.lift Args.name_source fun term_pat (ctxt, str) = @@ -860,9 +861,11 @@ |> ML_Syntax.print_term |> ML_Syntax.atomic in - ML_Antiquote.inline "term_pat" (parser >> term_pat) + ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat) end*} +setup{* term_pat_setup *} + text {* The parser in Line 2 provides us with a context and a string; this string is transformed into a term using the function @{ML_ind read_term_pattern in @@ -878,7 +881,8 @@ we can write an antiquotation for type patterns. *} -ML{*let +ML{*val type_pat_setup = +let val parser = Args.context -- Scan.lift Args.name_source fun typ_pat (ctxt, str) = @@ -886,9 +890,11 @@ |> ML_Syntax.print_typ |> ML_Syntax.atomic in - ML_Antiquote.inline "typ_pat" (parser >> typ_pat) + ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat) end*} +setup{* type_pat_setup *} + text {* \begin{readmore} The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/Recipes/Antiquotes.thy Tue Jun 28 09:22:00 2011 +0100 @@ -46,7 +46,9 @@ (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) -val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} +val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*} + +setup {* ml_checked_setup *} text {* The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this @@ -77,16 +79,18 @@ (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) -val _ = Thy_Output.antiquotation "ML_checked" +val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} (Scan.lift (Parse.position Args.name)) output_ml *} +setup {* ml_checked_setup2 *} + text {* where in Lines 1 and 2 the positional information is properly treated. The parser @{ML Parse.position} encodes the positional information in the result. - We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to - obtain @{ML_checked "2 + 3"} and be sure that this code compiles until + We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to + obtain @{ML_checked2 "2 + 3"} and be sure that this code compiles until somebody changes the definition of addition. @@ -102,7 +106,7 @@ give a partial specification by using ellipses. For example @{text "(\, \)"} for specifying a pair. In order to check consistency between the pattern and the output of the code, we have to change the ML-expression that is sent - to the compiler: in @{text "ML_checked"} we sent the expression @{text [quotes] + to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes] "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"} must be be replaced by the given pattern. However, we have to remove all ellipses from it and replace them by @{text [quotes] "_"}. The following @@ -136,12 +140,14 @@ Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) end) -val _ = Thy_Output.antiquotation "ML_resp" +val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} (Scan.lift (Parse.position (Args.name -- Args.name))) output_ml_resp*} +setup {* ml_resp_setup *} + text {* - In comparison with @{text "ML_checked"}, we only changed the line about + In comparison with @{text "ML_checked2"}, we only changed the line about the compiler (Line~2), the lines about the output (Lines 4 to 7) and the parser in the setup (Line 11). Now you can write diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/antiquote_setup.ML Tue Jun 28 09:22:00 2011 +0100 @@ -98,17 +98,18 @@ val two_args = Scan.lift (Args.name -- Args.name) val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) -val _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml -val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind -val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type -val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind -val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct -val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind -val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct -val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind -val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response -val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake -val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both +val ml_setup = + Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml + #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind + #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type + #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind + #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct + #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind + #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct + #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind + #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response + #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake + #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both (* FIXME: experimental *) fun ml_eq (lhs, pat, eq) = @@ -120,7 +121,8 @@ | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) -val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq +val ml_response_setup = + Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq (* checks whether a file exists in the Isabelle distribution *) fun href_link txt = @@ -136,7 +138,7 @@ then output ctxt [href_link txt] else error (implode ["Source file ", quote txt, " does not exist."])) -val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists +val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists (* replaces the official subgoal antiquotation with one *) @@ -176,7 +178,16 @@ Thy_Output.output ctxt output end -val _ = Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals -val _ = Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state +val subgoals_setup = + Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals +val raw_goal_state_setup = + Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state + +val setup = + ml_setup #> + ml_response_setup #> + ml_file_setup #> + subgoals_setup #> + raw_goal_state_setup end; diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/output_tutorial.ML --- a/ProgTutorial/output_tutorial.ML Tue Jun 28 08:44:34 2011 +0100 +++ b/ProgTutorial/output_tutorial.ML Tue Jun 28 09:22:00 2011 +0100 @@ -84,9 +84,13 @@ | boolean "false" = false | boolean s = error ("Bad boolean value: " ^ quote s); -val _ = Thy_Output.add_option @{binding "gray"} +val gray_setup = Thy_Output.add_option @{binding "gray"} (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) -val _ = Thy_Output.add_option @{binding "linenos"} +val linenos_setup = Thy_Output.add_option @{binding "linenos"} (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) +val setup = + gray_setup #> + linenos_setup + end \ No newline at end of file diff -r 817ecad4cf72 -r f65b9f14d5de progtutorial.pdf Binary file progtutorial.pdf has changed