1 (* Title: Doc/antiquote_setup.ML |
1 (* Title: Doc/antiquote_setup.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Auxiliary antiquotations for Isabelle manuals. |
5 Auxiliary antiquotations for the Isabelle manuals. |
6 *) |
6 *) |
7 |
7 |
8 local |
8 structure AntiquoteSetup: sig end = |
|
9 struct |
9 |
10 |
10 structure O = ThyOutput; |
11 structure O = ThyOutput; |
11 |
12 |
|
13 |
|
14 (* misc utils *) |
|
15 |
12 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
16 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
|
17 |
|
18 fun tweak_line s = |
|
19 if ! O.display then s else Symbol.strip_blanks s; |
|
20 |
|
21 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
|
22 |
|
23 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
24 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
25 |
|
26 |
|
27 (* verbatim text *) |
|
28 |
|
29 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
30 |
|
31 val _ = O.add_commands |
|
32 [("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ => |
|
33 split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))]; |
|
34 |
|
35 |
|
36 (* ML text *) |
|
37 |
|
38 local |
13 |
39 |
14 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
40 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
15 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
41 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
16 |
42 |
17 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
43 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
22 |
48 |
23 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
49 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
24 |
50 |
25 fun ml_functor _ = "val _ = ();"; (*no check!*) |
51 fun ml_functor _ = "val _ = ();"; (*no check!*) |
26 |
52 |
27 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
28 |
|
29 fun index_ml kind ml src ctxt (txt1, txt2) = |
53 fun index_ml kind ml src ctxt (txt1, txt2) = |
30 let |
54 let |
31 val txt = if txt2 = "" then txt1 else |
55 val txt = if txt2 = "" then txt1 else |
32 if kind = "type" |
56 if kind = "type" then txt1 ^ " = " ^ txt2 |
33 then txt1 ^ " = " ^ txt2 |
57 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
34 else if kind = "exception" |
|
35 then txt1 ^ " of " ^ txt2 |
|
36 else txt1 ^ ": " ^ txt2; |
58 else txt1 ^ ": " ^ txt2; |
37 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
59 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
38 val _ = writeln (ml (txt1, txt2)); |
60 val _ = writeln (ml (txt1, txt2)); |
39 val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
61 val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
40 in |
62 in |
46 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
68 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
47 end; |
69 end; |
48 |
70 |
49 fun output_ml ctxt src = |
71 fun output_ml ctxt src = |
50 if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
72 if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
51 else |
73 else |
52 split_lines |
74 split_lines |
53 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
75 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
54 #> space_implode "\\isasep\\isanewline%\n"; |
76 #> space_implode "\\isasep\\isanewline%\n"; |
55 |
77 |
56 fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"; |
78 fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
57 |
79 |
58 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
80 in |
59 |
81 |
60 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name); |
82 val _ = O.add_commands |
|
83 [("index_ML", ml_args (index_ml "" ml_val)), |
|
84 ("index_ML_type", ml_args (index_ml "type" ml_type)), |
|
85 ("index_ML_exn", ml_args (index_ml "exception" ml_exn)), |
|
86 ("index_ML_structure", ml_args (index_ml "structure" ml_structure)), |
|
87 ("index_ML_functor", ml_args (index_ml "functor" ml_functor)), |
|
88 ("ML_functor", O.args (Scan.lift Args.name) output_ml), |
|
89 ("ML_text", O.args (Scan.lift Args.name) output_ml)]; |
|
90 |
|
91 end; |
61 |
92 |
62 |
93 |
63 (* theorems with names *) |
94 (* theorems with names *) |
64 |
95 |
65 fun tweak_line s = |
96 local |
66 if ! O.display then s else Symbol.strip_blanks s; |
|
67 |
97 |
68 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
98 fun output_named_thms src ctxt xs = |
69 |
99 map (apfst (pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*) |
70 fun output_named_list pretty src ctxt xs = |
|
71 map (apfst (pretty ctxt)) xs (*always pretty in order to exhibit errors!*) |
|
72 |> (if ! O.quotes then map (apfst Pretty.quote) else I) |
100 |> (if ! O.quotes then map (apfst Pretty.quote) else I) |
73 |> (if ! O.display then |
101 |> (if ! O.display then |
74 map (fn (p, name) => |
102 map (fn (p, name) => |
75 Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
103 Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
76 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
104 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
81 Output.output (Pretty.str_of p) ^ |
109 Output.output (Pretty.str_of p) ^ |
82 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
110 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
83 #> space_implode "\\par\\smallskip%\n" |
111 #> space_implode "\\par\\smallskip%\n" |
84 #> enclose "\\isa{" "}"); |
112 #> enclose "\\isa{" "}"); |
85 |
113 |
86 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
87 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
88 |
|
89 in |
114 in |
90 |
115 |
91 val _ = O.add_commands |
116 val _ = O.add_commands |
92 [("index_ML", arguments (index_ml "" ml_val)), |
117 [("named_thms", O.args (Scan.repeat (Attrib.thm -- |
93 ("index_ML_type", arguments (index_ml "type" ml_type)), |
118 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) output_named_thms)]; |
94 ("index_ML_exn", arguments (index_ml "exception" ml_exn)), |
|
95 ("index_ML_structure", arguments (index_ml "structure" ml_structure)), |
|
96 ("index_ML_functor", arguments (index_ml "functor" ml_functor)), |
|
97 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
|
98 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
|
99 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))), |
|
100 ("named_thms", O.args (Scan.repeat (Attrib.thm -- |
|
101 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) |
|
102 (output_named_list pretty_thm)), |
|
103 ("ML_text", O.args (Scan.lift Args.name) output_ml)]; |
|
104 |
119 |
105 end; |
120 end; |
|
121 |
|
122 |
|
123 (* theory files *) |
|
124 |
|
125 val _ = O.add_commands |
|
126 [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => |
|
127 (ThyLoad.check_thy Path.current name; Pretty.str name))))]; |
|
128 |
|
129 end; |