author | berghofe |
Tue, 16 Dec 2008 17:37:39 +0100 | |
changeset 57 | 065f472c09ab |
parent 54 | 1783211b3494 |
child 72 | 7b8c4fe235aa |
permissions | -rw-r--r-- |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Auxiliary antiquotations for the Cookbook. *) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
structure AntiquoteSetup: sig end = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
struct |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
fun ml_val_open (ys, xs) txt = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
let fun ml_val_open_aux ys txt = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
"fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
in |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
(case xs of |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
[] => ml_val_open_aux ys txt |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
| _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end")) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
end; |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
fun ml_val txt = ml_val_open ([],[]) txt; |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
fun ml_pat (rhs, pat) = |
51
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
18 |
let |
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
19 |
val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
20 |
in "val " ^ pat' ^ " = " ^ rhs end; |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
|
57
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
25 |
val transform_cmts_str = |
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
26 |
Source.of_string #> ML_Lex.source #> Source.exhaust #> |
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
27 |
Chunks.transform_cmts #> implode; |
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
28 |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
29 |
fun output_ml ml src ctxt ((txt,ovars),pos) = |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
(ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
57
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
31 |
txt |> transform_cmts_str |> space_explode "\n" |> |
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
32 |
ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
34 |
fun output_ml_aux ml src ctxt (txt,pos) = |
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
35 |
output_ml (K ml) src ctxt ((txt,()),pos) |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
fun add_response_indicator txt = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
map (fn s => "> " ^ s) (space_explode "\n" txt) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
(ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
51
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
42 |
let |
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
43 |
val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
(ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
|
54
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
51 |
fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
52 |
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
53 |
in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
54 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
fun check_file_exists ctxt txt = |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
else error ("Source file " ^ quote txt ^ " does not exist.") |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
val _ = ThyOutput.add_commands |
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
60 |
[("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
62 |
Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
63 |
(output_ml ml_val_open)), |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
("ML_file", ThyOutput.args (Scan.lift Args.name) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
(ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
("ML_text", ThyOutput.args (Scan.lift Args.name) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
(ThyOutput.output (fn _ => fn s => Pretty.str s))), |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
(output_ml_response ml_pat)), |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
(output_ml_response_fake ml_val)), |
54
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
72 |
("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
73 |
(output_ml_response_fake_both ml_val)), |
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
74 |
("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
75 |
("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; |
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
end; |