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 |
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 map (Output.output o Pretty.str_of) |
|
28 #> space_implode "\\isasep\\isanewline%\n" |
|
29 #> enclose "\\isa{" "}"); |
|
30 |
|
31 val _ = ThyOutput.add_options |
|
32 [("gray", Library.setmp gray o boolean)] |
|
33 |
|
34 |
|
35 (* main body *) |
6 fun ml_val_open (ys, xs) txt = |
36 fun ml_val_open (ys, xs) txt = |
7 let fun ml_val_open_aux ys txt = |
37 let fun ml_val_open_aux ys txt = |
8 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
38 "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; |
9 in |
39 in |
10 (case xs of |
40 (case xs of |
27 Chunks.transform_cmts #> implode; |
57 Chunks.transform_cmts #> implode; |
28 |
58 |
29 fun output_ml ml src ctxt ((txt,ovars),pos) = |
59 fun output_ml ml src ctxt ((txt,ovars),pos) = |
30 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
60 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
31 txt |> transform_cmts_str |> space_explode "\n" |> |
61 txt |> transform_cmts_str |> space_explode "\n" |> |
32 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
62 output_list (fn _ => fn s => Pretty.str s) src ctxt) |
33 |
63 |
34 fun output_ml_aux ml src ctxt (txt,pos) = |
64 fun output_ml_aux ml src ctxt (txt,pos) = |
35 output_ml (K ml) src ctxt ((txt,()),pos) |
65 output_ml (K ml) src ctxt ((txt,()),pos) |
36 |
66 |
37 fun add_response_indicator txt = |
67 fun add_response_indicator txt = |
39 |
69 |
40 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
70 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
41 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
71 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
42 let |
72 let |
43 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
73 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
44 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
74 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
45 |
75 |
46 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
76 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
47 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
77 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
48 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
78 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
49 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
79 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
50 |
80 |
51 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
81 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
52 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
82 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
53 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
83 in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
54 |
84 |
55 fun check_file_exists ctxt txt = |
85 fun check_file_exists ctxt txt = |
56 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
86 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
57 else error ("Source file " ^ quote txt ^ " does not exist.") |
87 else error ("Source file " ^ quote txt ^ " does not exist.") |
58 |
88 |