--- 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 \<Rightarrow> 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 {*
--- 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
--- 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 "\<verbopen>"}\\
@{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
--- 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"
--- 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 {*
--- 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
--- 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
Binary file progtutorial.pdf has changed