--- 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 #>