equal
deleted
inserted
replaced
1 (* Auxiliary antiquotations for the Cookbook. *) |
1 (* Auxiliary antiquotations for the Cookbook. *) |
2 |
2 |
3 structure AntiquoteSetup: sig end = |
3 structure AntiquoteSetup: sig end = |
4 struct |
4 struct |
5 |
|
6 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
|
7 |
5 |
8 fun ml_val_open (ys, xs) txt = |
6 fun ml_val_open (ys, xs) txt = |
9 let fun ml_val_open_aux ys txt = |
7 let fun ml_val_open_aux ys txt = |
10 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
8 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
11 in |
9 in |
15 end; |
13 end; |
16 |
14 |
17 fun ml_val txt = ml_val_open ([],[]) txt; |
15 fun ml_val txt = ml_val_open ([],[]) txt; |
18 |
16 |
19 fun ml_pat (rhs, pat) = |
17 fun ml_pat (rhs, pat) = |
20 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
18 let |
21 in |
19 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
22 "val " ^ pat' ^ " = " ^ rhs |
20 in "val " ^ pat' ^ " = " ^ rhs end; |
23 end; |
|
24 |
21 |
25 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
22 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
26 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
23 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
27 |
24 |
28 fun output_ml_open ml src ctxt ((txt,ovars),pos) = |
25 fun output_ml_open ml src ctxt ((txt,ovars),pos) = |
35 fun add_response_indicator txt = |
32 fun add_response_indicator txt = |
36 map (fn s => "> " ^ s) (space_explode "\n" txt) |
33 map (fn s => "> " ^ s) (space_explode "\n" txt) |
37 |
34 |
38 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
35 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
39 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
36 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
40 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
37 let |
|
38 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
41 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
39 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
42 |
40 |
43 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
41 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
44 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
45 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
43 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |