# HG changeset patch # User Christian Urban # Date 1276003110 -7200 # Node ID d9a223c023f64a6116cd40ce00be873a21a58171 # Parent e2b351efd6f3489f28b3d164ba0085546906676c updated to new Isabelle diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Wed Jun 02 10:08:16 2010 +0200 +++ b/ProgTutorial/Base.thy Tue Jun 08 15:18:30 2010 +0200 @@ -104,20 +104,23 @@ (fn (txt, pos) => Toplevel.generic_theory (ML_Context.exec - (fn () => ML_Context.eval true pos txt) + (fn () => ML_Context.eval_text true pos txt) #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) - +*} +ML {* val _ = Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag "TutorialML" Keyword.prf_decl) (Parse.ML_source >> (fn (txt, pos) => Toplevel.proof (Proof.map_context (Context.proof_map - (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) + (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf))) +*} +ML {* val _ = Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag "TutorialML" Keyword.diag) - (Parse.ML_source >> IsarCmd.ml_diag true) + (Parse.ML_source >> Isar_Cmd.ml_diag true) *} ML {* @@ -125,7 +128,7 @@ Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl) (Parse.ML_source >> (fn (txt, pos) => - (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) + (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) *} ML {* @@ -133,7 +136,7 @@ Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl) (Parse.ML_source >> (fn (txt, pos) => - IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); + Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); *} ML {* diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Wed Jun 02 10:08:16 2010 +0200 +++ b/ProgTutorial/Recipes/Antiquotes.thy Tue Jun 08 15:18:30 2010 +0200 @@ -35,7 +35,7 @@ The code is checked by sending the ML-expression @{text [quotes] "val _ = a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML - "ML_Context.eval_in"} in Line 4 below). The complete code of the + "ML_Context.eval_text_in"} in Line 4 below). The complete code of the document antiquotation is as follows: *} @@ -43,10 +43,10 @@ ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt fun output_ml {context = ctxt, ...} code_txt = - (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); - ThyOutput.output (map Pretty.str (space_explode "\n" 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))) -val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} +val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} text {* The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this @@ -55,13 +55,13 @@ function @{ML ml_val}, which constructs the appropriate ML-expression, and using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is ``approved'' by the compiler, then the output function @{ML "output" in - ThyOutput} in the next line pretty prints the code. This function expects + Thy_Output} in the next line pretty prints the code. This function expects that the code is a list of (pretty)strings where each string correspond to a line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" for txt} which produces such a list according to linebreaks. There are a number of options for antiquotations that are observed by the function - @{ML "output" in ThyOutput} when printing the code (including @{text "[display]"} - and @{text "[quotes]"}). The function @{ML "antiquotation" in ThyOutput} in + @{ML "output" in Thy_Output} when printing the code (including @{text "[display]"} + and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in Line 7 sets up the new document antiquotation. \begin{readmore} @@ -74,10 +74,10 @@ *} ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = - (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); - ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) + (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); + Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) -val _ = ThyOutput.antiquotation "ML_checked" +val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift (Parse.position Args.name)) output_ml *} text {* @@ -128,15 +128,15 @@ *} ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = - (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); + (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); let val code_output = space_explode "\n" code_txt val resp_output = add_resp (space_explode "\n" pat) in - ThyOutput.output (map Pretty.str (code_output @ resp_output)) + Thy_Output.output (map Pretty.str (code_output @ resp_output)) end) -val _ = ThyOutput.antiquotation "ML_resp" +val _ = Thy_Output.antiquotation "ML_resp" (Scan.lift (Parse.position (Args.name -- Args.name))) output_ml_resp*} diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Wed Jun 02 10:08:16 2010 +0200 +++ b/ProgTutorial/antiquote_setup.ML Tue Jun 08 15:18:30 2010 +0200 @@ -33,7 +33,7 @@ (* eval function *) fun eval_fn ctxt exp = - ML_Context.eval_in (SOME ctxt) false Position.none exp + ML_Context.eval_text_in (SOME ctxt) false Position.none exp (* checks and prints a possibly open expressions, no index *) fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = @@ -98,17 +98,17 @@ val two_args = Scan.lift (Args.name -- Args.name) val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) -val _ = ThyOutput.antiquotation "ML" parser_ml output_ml -val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind -val _ = ThyOutput.antiquotation "ML_type" single_arg output_type -val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind -val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct -val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind -val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct -val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind -val _ = ThyOutput.antiquotation "ML_response" two_args output_response -val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake -val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both +val _ = Thy_Output.antiquotation "ML" parser_ml output_ml +val _ = Thy_Output.antiquotation "ML_ind" parser_ml_ind output_ml_ind +val _ = Thy_Output.antiquotation "ML_type" single_arg output_type +val _ = Thy_Output.antiquotation "ML_type_ind" single_arg output_type_ind +val _ = Thy_Output.antiquotation "ML_struct" single_arg output_struct +val _ = Thy_Output.antiquotation "ML_struct_ind" single_arg output_struct_ind +val _ = Thy_Output.antiquotation "ML_funct" single_arg output_funct +val _ = Thy_Output.antiquotation "ML_funct_ind" single_arg output_funct_ind +val _ = Thy_Output.antiquotation "ML_response" two_args output_response +val _ = Thy_Output.antiquotation "ML_response_fake" two_args output_response_fake +val _ = Thy_Output.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both (* FIXME: experimental *) fun ml_eq (lhs, pat, eq) = @@ -120,7 +120,7 @@ | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); output ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) -val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq +val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq (* checks whether a file exists in the Isabelle distribution *) fun href_link txt = @@ -136,7 +136,7 @@ then output [href_link txt] else error (implode ["Source file ", quote txt, " does not exist."])) -val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists +val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists (* replaces the official subgoal antiquotation with one *) @@ -161,7 +161,7 @@ 0 => [goals] | n => [Pretty.str (subgoals n), goals]) in - ThyOutput.output output + Thy_Output.output output end fun output_raw_goal_state {state = node, context = ctxt, ...} _ = @@ -173,10 +173,10 @@ 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 - ThyOutput.output output + Thy_Output.output output end -val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals -val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state +val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals +val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state end; diff -r e2b351efd6f3 -r d9a223c023f6 ProgTutorial/output_tutorial.ML --- a/ProgTutorial/output_tutorial.ML Wed Jun 02 10:08:16 2010 +0200 +++ b/ProgTutorial/output_tutorial.ML Tue Jun 08 15:18:30 2010 +0200 @@ -2,7 +2,7 @@ structure OutputTutorial = struct -(* rebuilding the output function from ThyOutput in order to *) +(* rebuilding the output function from Thy_Output in order to *) (* enable the options [gray, linenos] *) val gray = Unsynchronized.ref false @@ -14,15 +14,15 @@ val prts = map Pretty.str txt in prts - |> (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)) + |> (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)) #> 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 ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) + map (Output.output o (if ! Thy_Output.break then Pretty.string_of else Pretty.str_of)) #> space_implode "\\isasep\\isanewline%\n" #> enclose "\\isa{" "}") end @@ -84,7 +84,7 @@ | boolean "false" = false | boolean s = error ("Bad boolean value: " ^ quote s); -val _ = ThyOutput.add_options +val _ = Thy_Output.add_options [("gray", Library.setmp_CRITICAL gray o boolean), ("linenos", Library.setmp_CRITICAL linenos o boolean)] diff -r e2b351efd6f3 -r d9a223c023f6 progtutorial.pdf Binary file progtutorial.pdf has changed