# HG changeset patch # User Christian Urban # Date 1282973236 -28800 # Node ID f952f2679a113407077fab32f84eae0f9255f32e # Parent 957f69b9b7df784a69c10fd1d81ed4a11ac0c7e5 updated to new isabelle diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/Essential.thy Sat Aug 28 13:27:16 2010 +0800 @@ -1438,14 +1438,14 @@ val assm2 = @{cprop "(P::nat \ bool) t"} val Pt_implies_Qt = - assume assm1 - |> forall_elim @{cterm "t::nat"} + Thm.assume assm1 + |> Thm.forall_elim @{cterm "t::nat"} - val Qt = implies_elim Pt_implies_Qt (assume assm2) + val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2) in Qt - |> implies_intr assm2 - |> implies_intr assm1 + |> Thm.implies_intr assm2 + |> Thm.implies_intr assm1 end*} text {* diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/Helper/Command/Command.thy Sat Aug 28 13:27:16 2010 +0800 @@ -4,7 +4,7 @@ ML {* let - val do_nothing = Scan.succeed (Local_Theory.theory I) + val do_nothing = Scan.succeed (Local_Theory.background_theory I) val kind = Keyword.thy_decl in Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing @@ -14,7 +14,7 @@ ML {* let fun trace_prop str = - Local_Theory.theory (fn lthy => (tracing str; lthy)) + Local_Theory.background_theory (fn lthy => (tracing str; lthy)) val trace_prop_parser = Parse.prop >> trace_prop val kind = Keyword.thy_decl in diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/Parsing.thy Sat Aug 28 13:27:16 2010 +0800 @@ -548,7 +548,7 @@ you obtain a list consisting of only one command and two keyword tokens. If you want to see which keywords and commands are currently known to Isabelle, - type: + use the function @{ML_ind get_lexicons in Keyword}: @{ML_response_fake [display,gray] "let @@ -956,7 +956,7 @@ *} ML{*let - val do_nothing = Scan.succeed (Local_Theory.theory I) + val do_nothing = Scan.succeed (Local_Theory.background_theory I) val kind = Keyword.thy_decl in Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing @@ -993,7 +993,7 @@ \isacommand{ML}~@{text "\"}\\ @{ML "let - val do_nothing = Scan.succeed (Local_Theory.theory I) + val do_nothing = Scan.succeed (Local_Theory.background_theory I) val kind = Keyword.thy_decl in Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing @@ -1110,7 +1110,7 @@ The crucial part of a command is the function that determines the behaviour of the command. In the code above we used a ``do-nothing''-function, which because of @{ML_ind succeed in Scan} does not parse any argument, but immediately - returns the simple function @{ML "Local_Theory.theory I"}. We can + returns the simple function @{ML "Local_Theory.background_theory I"}. We can replace this code by a function that first parses a proposition (using the parser @{ML Parse.prop}), then prints out the tracing information (using a new function @{text trace_prop}) and @@ -1119,7 +1119,7 @@ ML{*let fun trace_prop str = - Local_Theory.theory (fn ctxt => (tracing str; ctxt)) + Local_Theory.background_theory (fn ctxt => (tracing str; ctxt)) val kind = Keyword.thy_decl in diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/Recipes/Antiquotes.thy Sat Aug 28 13:27:16 2010 +0800 @@ -44,7 +44,7 @@ fun output_ml {context = ctxt, ...} code_txt = (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); - Thy_Output.output (map Pretty.str (space_explode "\n" 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*} @@ -75,7 +75,7 @@ ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); - Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) + Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift (Parse.position Args.name)) output_ml *} @@ -133,7 +133,7 @@ val code_output = space_explode "\n" code_txt val resp_output = add_resp (space_explode "\n" pat) in - Thy_Output.output (map Pretty.str (code_output @ resp_output)) + Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) end) val _ = Thy_Output.antiquotation "ML_resp" diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/Tactical.thy Sat Aug 28 13:27:16 2010 +0800 @@ -1912,7 +1912,7 @@ Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} (therefore we printing it out using the function @{ML pretty_term in Pretty}). We can turn this function into a proper simproc using the function - @{ML Simplifier.simproc_i}: + @{ML Simplifier.simproc_global_i}: *} @@ -1921,7 +1921,7 @@ val thy = @{theory} val pat = [@{term "Suc n"}] in - Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc') + Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc') end*} text {* @@ -1978,7 +1978,7 @@ val thy = @{theory} val pat = [@{term "Suc n"}] in - Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc) + Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc) end*} text {* @@ -2086,7 +2086,7 @@ val thy = @{theory} val pat = [@{term "Suc n"}] in - Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc) + Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) end*} text {* diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/antiquote_setup.ML Sat Aug 28 13:27:16 2010 +0800 @@ -38,7 +38,7 @@ (* checks and prints a possibly open expressions, no index *) fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = (eval_fn ctxt (ml_val vs stru txt); - output (split_lines txt)) + output ctxt (split_lines txt)) val parser_ml = Scan.lift (Args.name -- (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- @@ -48,51 +48,51 @@ fun output_ml_ind {context = ctxt, ...} (txt, stru) = (eval_fn ctxt (ml_val [] stru txt); case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of - (NONE, bn, "") => output_indexed {main = Code txt, minor = NoString} (split_lines txt) - | (NONE, bn, qn) => output_indexed {main = Code bn, minor = Struct qn} (split_lines txt) - | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt)) + (NONE, bn, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) + | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) + | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt)) val parser_ml_ind = Scan.lift (Args.name -- Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) (* checks and prints structures *) -fun gen_output_struct outfn {context = ctxt, ...} txt = +fun gen_output_struct outfn ctxt txt = (eval_fn ctxt (ml_struct txt); outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) -val output_struct = gen_output_struct (K output) -val output_struct_ind = gen_output_struct output_indexed +fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt +fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt (* prints functors; no checks *) -fun gen_output_funct outfn {context = ctxt, ...} txt = +fun gen_output_funct outfn txt = (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) -val output_funct = gen_output_funct (K output) -val output_funct_ind = gen_output_funct output_indexed +fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt)) +fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt) (* checks and prints types *) -fun gen_output_type outfn {context = ctxt, ...} txt = +fun gen_output_type outfn ctxt txt = (eval_fn ctxt (ml_type txt); outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) -val output_type = gen_output_type (K output) -val output_type_ind = gen_output_type output_indexed +fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt +fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt (* checks and expression agains a result pattern *) fun output_response {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_pat (lhs, pat)); write_file_ml_blk lhs (ProofContext.theory_of ctxt); - output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) + output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) fun output_response_fake {context = ctxt, ...} (lhs, pat) = (eval_fn ctxt (ml_val [] NONE lhs); write_file_ml_blk lhs (ProofContext.theory_of ctxt); - output ((split_lines lhs) @ (prefix_lines "> " pat))) + output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))) (* checks the expressions, but does not check it against a result pattern *) -fun ouput_response_fake_both _ (lhs, pat) = - output ((split_lines lhs) @ (prefix_lines "> " pat)) +fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = + output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)) val single_arg = Scan.lift (Args.name) val two_args = Scan.lift (Args.name -- Args.name) @@ -118,7 +118,7 @@ (case eq of NONE => eval_fn ctxt (ml_pat (lhs, pat)) | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); - output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) + output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq @@ -131,9 +131,9 @@ implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] end -fun check_file_exists _ txt = +fun check_file_exists {context = ctxt, ...} txt = (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) - then output [href_link txt] + then output ctxt [href_link txt] else error (implode ["Source file ", quote txt, " does not exist."])) val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists @@ -146,7 +146,7 @@ SOME prf => prf | _ => error "No proof state") -fun output_goals {state = node, ...} _ = +fun output_goals {state = node, context = ctxt, ...} _ = let fun subgoals 0 = "" | subgoals 1 = "goal (1 subgoal):" @@ -161,7 +161,7 @@ 0 => [goals] | n => [Pretty.str (subgoals n), goals]) in - Thy_Output.output output + Thy_Output.output ctxt output end fun output_raw_goal_state {state = node, context = ctxt, ...} _ = @@ -173,7 +173,7 @@ val _ = tracing (Syntax.string_of_term ctxt (prop_of goals)) val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals)))) in - Thy_Output.output output + Thy_Output.output ctxt output end val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/output_tutorial.ML --- a/ProgTutorial/output_tutorial.ML Sun Aug 22 22:56:52 2010 +0800 +++ b/ProgTutorial/output_tutorial.ML Sat Aug 28 13:27:16 2010 +0800 @@ -9,20 +9,20 @@ val linenos = Unsynchronized.ref false -fun output txt = +fun output ctxt txt = let val prts = map Pretty.str txt in prts - |> (if ! Thy_Output.quotes then map Pretty.quote else I) - |> (if ! Thy_Output.display then - map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.indent)) + |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I) + |> (if Config.get ctxt Thy_Output.display then + map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.indent)) #> space_implode "\\isasep\\isanewline%\n" #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) #> (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 ! Thy_Output.break then Pretty.string_of else Pretty.str_of)) + map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of)) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}") end @@ -74,8 +74,8 @@ Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"] | _ => "") -fun output_indexed ind txt = - txt |> output +fun output_indexed ctxt ind txt = + txt |> output ctxt |> prefix (get_index ind) |> prefix (get_str_index ind) @@ -84,8 +84,9 @@ | boolean "false" = false | boolean s = error ("Bad boolean value: " ^ quote s); -val _ = Thy_Output.add_options - [("gray", Library.setmp_CRITICAL gray o boolean), - ("linenos", Library.setmp_CRITICAL linenos o boolean)] +val _ = Thy_Output.add_option "gray" + (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) +val _ = Thy_Output.add_option "linenos" + (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) end \ No newline at end of file diff -r 957f69b9b7df -r f952f2679a11 progtutorial.pdf Binary file progtutorial.pdf has changed