diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Fri Jun 03 15:15:17 2016 +0100 +++ b/ProgTutorial/antiquote_setup.ML Tue May 14 11:10:53 2019 +0200 @@ -31,16 +31,13 @@ fun ml_type txt = implode ["val _ = NONE : (", txt, ") option"]; -fun ml_out txt = - implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""] - (* eval function *) fun eval_fn ctxt exp = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags - {delimited = false, text = exp, pos = Position.none} + (Input.source false exp Position.no_range) (* checks and prints a possibly open expressions, no index *) -fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = +fun output_ml ctxt (txt, (vs, stru)) = (eval_fn ctxt (ml_val vs stru txt); output ctxt (split_lines txt)) @@ -49,10 +46,10 @@ Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) (* checks and prints a single ML-item and produces an index entry *) -fun output_ml_ind {context = ctxt, ...} (txt, stru) = +fun output_ml_ind 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 ctxt {main = Code txt, minor = NoString} (split_lines txt) + (NONE, _, "") => 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)) @@ -64,126 +61,130 @@ (eval_fn ctxt (ml_struct txt); outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) -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 +fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt +fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt (* prints functors; no checks *) fun gen_output_funct outfn txt = (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) -fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt)) -fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt) +fun output_funct ctxt = gen_output_funct (K (output ctxt)) +fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) (* checks and prints types *) fun gen_output_type outfn ctxt txt = (eval_fn ctxt (ml_type txt); outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) -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 +fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt +fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt (* checks and expression agains a result pattern *) -fun output_response {context = ctxt, ...} (lhs, pat) = +fun output_response ctxt (lhs, pat) = (eval_fn ctxt (ml_pat (lhs, pat)); - eval_fn ctxt (ml_out lhs); + (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) 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) = +fun output_response_fake ctxt (lhs, pat) = (eval_fn ctxt (ml_val [] NONE lhs); - eval_fn ctxt (ml_out lhs); + (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) 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 {context = ctxt, ...} (lhs, pat) = +fun ouput_response_fake_both 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) val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) + + + 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 + Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml + #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind + #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type + #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind + #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct + #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind + #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct + #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind + #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response + #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake + #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both (* FIXME: experimental *) fun ml_eq (lhs, pat, eq) = implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] -fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = +fun output_response_eq ctxt ((lhs, pat), eq) = (case eq of NONE => eval_fn ctxt (ml_pat (lhs, pat)) | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) val ml_response_setup = - Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq + Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq (* checks whether a file exists in the Isabelle distribution *) fun href_link txt = let - val raw = Symbol.encode_raw + val raw = I (* FIXME: Symbol.encode_raw *) val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/" in - implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"] + implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] end -fun check_file_exists {context = ctxt, ...} txt = +fun check_file_exists _ txt = (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) - then output ctxt [href_link txt] + then Latex.string (href_link txt) else error (implode ["Source file ", quote txt, " does not exist."])) -val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists +val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists (* replaces the official subgoal antiquotation with one *) (* that is closer to the actual output *) + fun proof_state state = (case try (Proof.goal o Toplevel.proof_of) state of SOME {goal, ...} => goal | _ => error "No proof state"); -fun output_goals {state = node, context = ctxt, ...} _ = +fun output_goals ctxt _ = let fun subgoals 0 = "" | subgoals 1 = "goal (1 subgoal):" | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" - val state = proof_state node + val state = proof_state (Toplevel.presentation_state ctxt) val goals = Goal_Display.pretty_goal ctxt state - val {prop, ...} = rep_thm state; + val prop = Thm.prop_of state; val (As, _) = Logic.strip_horn prop; - val output = (case (length As) of - 0 => [goals] - | n => [Pretty.str (subgoals n), goals]) + val out = (case (length As) of + 0 => goals + | n => Pretty.big_list (subgoals n) [goals]) (* FIXME: improve printing? *) in - Thy_Output.output ctxt output + output ctxt [Pretty.string_of out] end -fun output_raw_goal_state {state, context = ctxt, ...} _ = +fun output_raw_goal_state ctxt _ = let - val goals = proof_state state - val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))] + val goals = proof_state (Toplevel.presentation_state ctxt) + val out = Syntax.string_of_term ctxt (Thm.prop_of goals) in - Thy_Output.output ctxt output + output ctxt [out] end val subgoals_setup = - Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals + Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals val raw_goal_state_setup = - Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state + Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state val setup = ml_setup #>