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 (* rebuilding the output_list function from ThyOutput in order to *) |
|
7 (* enable the option [gray] *) |
|
8 |
|
9 val gray = ref false; |
|
10 |
|
11 fun boolean "" = true |
|
12 | boolean "true" = true |
|
13 | boolean "false" = false |
|
14 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
15 |
|
16 fun output_list pretty src ctxt xs = |
|
17 map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) |
|
18 |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
|
19 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
20 |> (if ! ThyOutput.display then |
|
21 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
22 #> space_implode "\\isasep\\isanewline%\n" |
|
23 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
24 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
25 else |
|
26 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
|
27 #> space_implode "\\isasep\\isanewline%\n" |
|
28 #> enclose "\\isa{" "}"); |
|
29 |
|
30 val _ = ThyOutput.add_options |
|
31 [("gray", Library.setmp gray o boolean)] |
|
32 |
|
33 |
5 |
34 (* main body *) |
6 (* main body *) |
35 fun ml_val_open (ys, xs) txt = |
7 fun ml_val_open (ys, xs) txt = |
36 let fun ml_val_open_aux ys txt = |
8 let fun ml_val_open_aux ys txt = |
37 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
9 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
56 Chunks.transform_cmts #> implode; |
28 Chunks.transform_cmts #> implode; |
57 |
29 |
58 fun output_ml ml src ctxt ((txt,ovars),pos) = |
30 fun output_ml ml src ctxt ((txt,ovars),pos) = |
59 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
31 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
60 txt |> transform_cmts_str |> space_explode "\n" |> |
32 txt |> transform_cmts_str |> space_explode "\n" |> |
61 output_list (fn _ => fn s => Pretty.str s) src ctxt) |
33 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
62 |
34 |
63 fun output_ml_aux ml src ctxt (txt,pos) = |
35 fun output_ml_aux ml src ctxt (txt,pos) = |
64 output_ml (K ml) src ctxt ((txt,()),pos) |
36 output_ml (K ml) src ctxt ((txt,()),pos) |
65 |
37 |
66 fun add_response_indicator txt = |
38 fun add_response_indicator txt = |
68 |
40 |
69 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
41 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
70 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
71 let |
43 let |
72 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
44 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
73 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
45 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
74 |
46 |
75 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
47 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
76 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
48 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
77 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
49 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
78 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
50 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
79 |
51 |
80 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
52 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
81 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
53 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
82 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
54 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
83 |
55 |
84 fun check_file_exists ctxt txt = |
56 fun check_file_exists ctxt txt = |
85 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
57 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
86 else error ("Source file " ^ quote txt ^ " does not exist.") |
58 else error ("Source file " ^ quote txt ^ " does not exist.") |
87 |
59 |