96 |
96 |
97 val single_arg = Scan.lift (Args.name) |
97 val single_arg = Scan.lift (Args.name) |
98 val two_args = Scan.lift (Args.name -- Args.name) |
98 val two_args = Scan.lift (Args.name -- Args.name) |
99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
100 |
100 |
101 val _ = Thy_Output.antiquotation "ML" parser_ml output_ml |
101 val _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml |
102 val _ = Thy_Output.antiquotation "ML_ind" parser_ml_ind output_ml_ind |
102 val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind |
103 val _ = Thy_Output.antiquotation "ML_type" single_arg output_type |
103 val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type |
104 val _ = Thy_Output.antiquotation "ML_type_ind" single_arg output_type_ind |
104 val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind |
105 val _ = Thy_Output.antiquotation "ML_struct" single_arg output_struct |
105 val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct |
106 val _ = Thy_Output.antiquotation "ML_struct_ind" single_arg output_struct_ind |
106 val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind |
107 val _ = Thy_Output.antiquotation "ML_funct" single_arg output_funct |
107 val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct |
108 val _ = Thy_Output.antiquotation "ML_funct_ind" single_arg output_funct_ind |
108 val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind |
109 val _ = Thy_Output.antiquotation "ML_response" two_args output_response |
109 val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response |
110 val _ = Thy_Output.antiquotation "ML_response_fake" two_args output_response_fake |
110 val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake |
111 val _ = Thy_Output.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both |
111 val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both |
112 |
112 |
113 (* FIXME: experimental *) |
113 (* FIXME: experimental *) |
114 fun ml_eq (lhs, pat, eq) = |
114 fun ml_eq (lhs, pat, eq) = |
115 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
115 implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] |
116 |
116 |
118 (case eq of |
118 (case eq of |
119 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
119 NONE => eval_fn ctxt (ml_pat (lhs, pat)) |
120 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
120 | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e)); |
121 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
121 output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat))) |
122 |
122 |
123 val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq |
123 val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq |
124 |
124 |
125 (* checks whether a file exists in the Isabelle distribution *) |
125 (* checks whether a file exists in the Isabelle distribution *) |
126 fun href_link txt = |
126 fun href_link txt = |
127 let |
127 let |
128 val raw = Symbol.encode_raw |
128 val raw = Symbol.encode_raw |
134 fun check_file_exists {context = ctxt, ...} txt = |
134 fun check_file_exists {context = ctxt, ...} txt = |
135 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
135 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
136 then output ctxt [href_link txt] |
136 then output ctxt [href_link txt] |
137 else error (implode ["Source file ", quote txt, " does not exist."])) |
137 else error (implode ["Source file ", quote txt, " does not exist."])) |
138 |
138 |
139 val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists |
139 val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists |
140 |
140 |
141 |
141 |
142 (* replaces the official subgoal antiquotation with one *) |
142 (* replaces the official subgoal antiquotation with one *) |
143 (* that is closer to the actual output *) |
143 (* that is closer to the actual output *) |
144 fun proof_state state = |
144 fun proof_state state = |