author | haftmann |
Tue, 22 Apr 2008 22:00:25 +0200 | |
changeset 26739 | 947b6013e863 |
parent 26710 | f79aa228c582 |
child 26742 | 5a86bc79431c |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Doc/antiquote_setup.ML |
21375 | 2 |
ID: $Id$ |
3 |
Author: Makarius |
|
4 |
||
5 |
Auxiliary antiquotations for Isabelle manuals. |
|
6 |
*) |
|
7 |
||
8 |
local |
|
9 |
||
22094 | 10 |
structure O = ThyOutput; |
21375 | 11 |
|
12 |
val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; |
|
13 |
||
14 |
fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
|
15 |
| ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
|
16 |
||
17 |
fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
|
18 |
| ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
|
22289 | 19 |
|
23651 | 20 |
fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);" |
21 |
| ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);"; |
|
22289 | 22 |
|
21375 | 23 |
fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
24 |
||
25 |
fun ml_functor _ = "val _ = ();"; (*no check!*) |
|
26 |
||
27 |
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
28 |
||
29 |
fun index_ml kind ml src ctxt (txt1, txt2) = |
|
30 |
let |
|
31 |
val txt = if txt2 = "" then txt1 else |
|
32 |
if kind = "type" |
|
33 |
then txt1 ^ " = " ^ txt2 |
|
22289 | 34 |
else if kind = "exception" |
35 |
then txt1 ^ " of " ^ txt2 |
|
36 |
else txt1 ^ ": " ^ txt2; |
|
21375 | 37 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
22289 | 38 |
val _ = writeln (ml (txt1, txt2)); |
26455 | 39 |
val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
21375 | 40 |
in |
41 |
"\\indexml" ^ kind ^ enclose "{" "}" |
|
22289 | 42 |
(translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^ |
21375 | 43 |
((if ! O.source then str_of_source src else txt') |
44 |
|> (if ! O.quotes then quote else I) |
|
45 |
|> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
46 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
|
47 |
end; |
|
48 |
||
26461 | 49 |
fun output_ml ctxt src = |
50 |
if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
51 |
else |
|
52 |
split_lines |
|
53 |
#> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
|
54 |
#> space_implode "\\isasep\\isanewline%\n"; |
|
55 |
||
21375 | 56 |
fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"; |
57 |
||
58 |
fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
|
59 |
||
24204 | 60 |
fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name); |
21375 | 61 |
|
23846 | 62 |
|
63 |
(* theorems with names *) |
|
64 |
||
65 |
fun tweak_line s = |
|
66 |
if ! O.display then s else Symbol.strip_blanks s; |
|
67 |
||
68 |
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
|
69 |
||
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) |
|
73 |
|> (if ! O.display then |
|
74 |
map (fn (p, name) => |
|
75 |
Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
|
76 |
"\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
77 |
#> space_implode "\\par\\smallskip%\n" |
|
78 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
79 |
else |
|
80 |
map (fn (p, name) => |
|
81 |
Output.output (Pretty.str_of p) ^ |
|
82 |
"\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
83 |
#> space_implode "\\par\\smallskip%\n" |
|
84 |
#> enclose "\\isa{" "}"); |
|
85 |
||
26710
f79aa228c582
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
wenzelm
parents:
26461
diff
changeset
|
86 |
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
23846 | 87 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
88 |
||
21375 | 89 |
in |
90 |
||
91 |
val _ = O.add_commands |
|
92 |
[("index_ML", arguments (index_ml "" ml_val)), |
|
93 |
("index_ML_type", arguments (index_ml "type" ml_type)), |
|
23651 | 94 |
("index_ML_exn", arguments (index_ml "exception" ml_exn)), |
21375 | 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), |
|
23846 | 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.$$$ ")"))) |
|
26461 | 102 |
(output_named_list pretty_thm)), |
103 |
("ML_text", O.args (Scan.lift Args.name) output_ml)]; |
|
21375 | 104 |
|
105 |
end; |