author | wenzelm |
Wed, 07 May 2008 13:05:13 +0200 | |
changeset 26843 | 612ca951afee |
parent 26785 | e77f9b8c7514 |
child 26853 | 52cb0e965041 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Doc/antiquote_setup.ML |
21375 | 2 |
ID: $Id$ |
3 |
Author: Makarius |
|
4 |
||
26742 | 5 |
Auxiliary antiquotations for the Isabelle manuals. |
21375 | 6 |
*) |
7 |
||
26742 | 8 |
structure AntiquoteSetup: sig end = |
9 |
struct |
|
21375 | 10 |
|
22094 | 11 |
structure O = ThyOutput; |
21375 | 12 |
|
26742 | 13 |
|
14 |
(* misc utils *) |
|
15 |
||
26768 | 16 |
val clean_string = translate_string |
17 |
(fn "_" => "-" |
|
18 |
| ">" => "$>$" |
|
19 |
| "#" => "\\#" |
|
20 |
| "{" => "\\{" |
|
21 |
| "}" => "\\}" |
|
22 |
| c => c); |
|
26751 | 23 |
|
21375 | 24 |
val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
25 |
||
26742 | 26 |
fun tweak_line s = |
27 |
if ! O.display then s else Symbol.strip_blanks s; |
|
28 |
||
29 |
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
|
30 |
||
31 |
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
|
32 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
33 |
||
34 |
||
35 |
(* verbatim text *) |
|
36 |
||
37 |
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
38 |
||
39 |
val _ = O.add_commands |
|
40 |
[("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ => |
|
41 |
split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))]; |
|
42 |
||
43 |
||
44 |
(* ML text *) |
|
45 |
||
46 |
local |
|
47 |
||
21375 | 48 |
fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
49 |
| ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
|
50 |
||
51 |
fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
|
52 |
| ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
|
22289 | 53 |
|
23651 | 54 |
fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);" |
55 |
| ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);"; |
|
22289 | 56 |
|
21375 | 57 |
fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
58 |
||
59 |
fun ml_functor _ = "val _ = ();"; (*no check!*) |
|
60 |
||
61 |
fun index_ml kind ml src ctxt (txt1, txt2) = |
|
62 |
let |
|
63 |
val txt = if txt2 = "" then txt1 else |
|
26742 | 64 |
if kind = "type" then txt1 ^ " = " ^ txt2 |
65 |
else if kind = "exception" then txt1 ^ " of " ^ txt2 |
|
22289 | 66 |
else txt1 ^ ": " ^ txt2; |
21375 | 67 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
22289 | 68 |
val _ = writeln (ml (txt1, txt2)); |
26455 | 69 |
val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
21375 | 70 |
in |
26751 | 71 |
"\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
21375 | 72 |
((if ! O.source then str_of_source src else txt') |
73 |
|> (if ! O.quotes then quote else I) |
|
74 |
|> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
26751 | 75 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
21375 | 76 |
end; |
77 |
||
26461 | 78 |
fun output_ml ctxt src = |
79 |
if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
26742 | 80 |
else |
26461 | 81 |
split_lines |
82 |
#> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
|
83 |
#> space_implode "\\isasep\\isanewline%\n"; |
|
84 |
||
26742 | 85 |
fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
86 |
||
87 |
in |
|
21375 | 88 |
|
26742 | 89 |
val _ = O.add_commands |
90 |
[("index_ML", ml_args (index_ml "" ml_val)), |
|
91 |
("index_ML_type", ml_args (index_ml "type" ml_type)), |
|
92 |
("index_ML_exn", ml_args (index_ml "exception" ml_exn)), |
|
93 |
("index_ML_structure", ml_args (index_ml "structure" ml_structure)), |
|
94 |
("index_ML_functor", ml_args (index_ml "functor" ml_functor)), |
|
95 |
("ML_functor", O.args (Scan.lift Args.name) output_ml), |
|
96 |
("ML_text", O.args (Scan.lift Args.name) output_ml)]; |
|
21375 | 97 |
|
26742 | 98 |
end; |
21375 | 99 |
|
23846 | 100 |
|
101 |
(* theorems with names *) |
|
102 |
||
26742 | 103 |
local |
23846 | 104 |
|
26742 | 105 |
fun output_named_thms src ctxt xs = |
106 |
map (apfst (pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*) |
|
23846 | 107 |
|> (if ! O.quotes then map (apfst Pretty.quote) else I) |
108 |
|> (if ! O.display then |
|
109 |
map (fn (p, name) => |
|
110 |
Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
|
111 |
"\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
112 |
#> space_implode "\\par\\smallskip%\n" |
|
113 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
114 |
else |
|
115 |
map (fn (p, name) => |
|
116 |
Output.output (Pretty.str_of p) ^ |
|
117 |
"\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
118 |
#> space_implode "\\par\\smallskip%\n" |
|
119 |
#> enclose "\\isa{" "}"); |
|
120 |
||
21375 | 121 |
in |
122 |
||
123 |
val _ = O.add_commands |
|
26742 | 124 |
[("named_thms", O.args (Scan.repeat (Attrib.thm -- |
26751 | 125 |
Scan.lift (Args.parens Args.name))) output_named_thms)]; |
21375 | 126 |
|
127 |
end; |
|
26742 | 128 |
|
129 |
||
130 |
(* theory files *) |
|
131 |
||
132 |
val _ = O.add_commands |
|
133 |
[("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => |
|
134 |
(ThyLoad.check_thy Path.current name; Pretty.str name))))]; |
|
135 |
||
26751 | 136 |
|
137 |
(* Isar entities (with index) *) |
|
138 |
||
139 |
local |
|
140 |
||
141 |
val arg = enclose "{" "}" o clean_string; |
|
142 |
||
26843 | 143 |
fun output_entity markup index kind ctxt (logic, name) = |
26751 | 144 |
(case index of |
145 |
NONE => "" |
|
146 |
| SOME is_def => |
|
147 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name) |
|
148 |
^ |
|
26843 | 149 |
(Output.output name |
26756 | 150 |
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
26751 | 151 |
|> (if ! O.quotes then quote else I) |
152 |
|> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
26774
e258050a3076
output_entity: added \mbox{} to prevent hyphenation;
wenzelm
parents:
26768
diff
changeset
|
153 |
else enclose "\\mbox{\\isa{" "}}")); |
26751 | 154 |
|
26756 | 155 |
fun entity markup index kind = |
26751 | 156 |
O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
26843 | 157 |
(K (output_entity markup index kind)); |
26751 | 158 |
|
26756 | 159 |
fun entity_antiqs markup kind = |
160 |
[(kind, entity markup NONE kind), |
|
161 |
(kind ^ "_def", entity markup (SOME true) kind), |
|
162 |
(kind ^ "_ref", entity markup (SOME false) kind)]; |
|
26751 | 163 |
|
164 |
in |
|
165 |
||
166 |
val _ = O.add_commands |
|
26756 | 167 |
(entity_antiqs "" "syntax" @ |
168 |
entity_antiqs "isacommand" "command" @ |
|
169 |
entity_antiqs "isakeyword" "keyword" @ |
|
26785 | 170 |
entity_antiqs "isakeyword" "element" @ |
26756 | 171 |
entity_antiqs "" "method" @ |
172 |
entity_antiqs "" "attribute" @ |
|
173 |
entity_antiqs "" "fact" @ |
|
174 |
entity_antiqs "" "variable" @ |
|
175 |
entity_antiqs "" "case" @ |
|
176 |
entity_antiqs "" "antiquotation"); |
|
26751 | 177 |
|
26742 | 178 |
end; |
26751 | 179 |
|
180 |
end; |