1.1 --- a/doc-src/antiquote_setup.ML Wed Apr 23 12:13:08 2008 +0200
1.2 +++ b/doc-src/antiquote_setup.ML Wed Apr 23 15:04:14 2008 +0200
1.3 @@ -2,15 +2,41 @@
1.4 ID: $Id$
1.5 Author: Makarius
1.6
1.7 -Auxiliary antiquotations for Isabelle manuals.
1.8 +Auxiliary antiquotations for the Isabelle manuals.
1.9 *)
1.10
1.11 -local
1.12 +structure AntiquoteSetup: sig end =
1.13 +struct
1.14
1.15 structure O = ThyOutput;
1.16
1.17 +
1.18 +(* misc utils *)
1.19 +
1.20 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
1.21
1.22 +fun tweak_line s =
1.23 + if ! O.display then s else Symbol.strip_blanks s;
1.24 +
1.25 +val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
1.26 +
1.27 +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
1.28 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
1.29 +
1.30 +
1.31 +(* verbatim text *)
1.32 +
1.33 +val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
1.34 +
1.35 +val _ = O.add_commands
1.36 + [("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ =>
1.37 + split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))];
1.38 +
1.39 +
1.40 +(* ML text *)
1.41 +
1.42 +local
1.43 +
1.44 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
1.45 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");";
1.46
1.47 @@ -24,15 +50,11 @@
1.48
1.49 fun ml_functor _ = "val _ = ();"; (*no check!*)
1.50
1.51 -val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
1.52 -
1.53 fun index_ml kind ml src ctxt (txt1, txt2) =
1.54 let
1.55 val txt = if txt2 = "" then txt1 else
1.56 - if kind = "type"
1.57 - then txt1 ^ " = " ^ txt2
1.58 - else if kind = "exception"
1.59 - then txt1 ^ " of " ^ txt2
1.60 + if kind = "type" then txt1 ^ " = " ^ txt2
1.61 + else if kind = "exception" then txt1 ^ " of " ^ txt2
1.62 else txt1 ^ ": " ^ txt2;
1.63 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.64 val _ = writeln (ml (txt1, txt2));
1.65 @@ -48,27 +70,33 @@
1.66
1.67 fun output_ml ctxt src =
1.68 if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.69 - else
1.70 + else
1.71 split_lines
1.72 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
1.73 #> space_implode "\\isasep\\isanewline%\n";
1.74
1.75 -fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
1.76 +fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
1.77
1.78 -fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
1.79 +in
1.80
1.81 -fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name);
1.82 +val _ = O.add_commands
1.83 + [("index_ML", ml_args (index_ml "" ml_val)),
1.84 + ("index_ML_type", ml_args (index_ml "type" ml_type)),
1.85 + ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
1.86 + ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
1.87 + ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
1.88 + ("ML_functor", O.args (Scan.lift Args.name) output_ml),
1.89 + ("ML_text", O.args (Scan.lift Args.name) output_ml)];
1.90 +
1.91 +end;
1.92
1.93
1.94 (* theorems with names *)
1.95
1.96 -fun tweak_line s =
1.97 - if ! O.display then s else Symbol.strip_blanks s;
1.98 +local
1.99
1.100 -val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
1.101 -
1.102 -fun output_named_list pretty src ctxt xs =
1.103 - map (apfst (pretty ctxt)) xs (*always pretty in order to exhibit errors!*)
1.104 +fun output_named_thms src ctxt xs =
1.105 + map (apfst (pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*)
1.106 |> (if ! O.quotes then map (apfst Pretty.quote) else I)
1.107 |> (if ! O.display then
1.108 map (fn (p, name) =>
1.109 @@ -83,23 +111,19 @@
1.110 #> space_implode "\\par\\smallskip%\n"
1.111 #> enclose "\\isa{" "}");
1.112
1.113 -fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
1.114 -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
1.115 -
1.116 in
1.117
1.118 val _ = O.add_commands
1.119 - [("index_ML", arguments (index_ml "" ml_val)),
1.120 - ("index_ML_type", arguments (index_ml "type" ml_type)),
1.121 - ("index_ML_exn", arguments (index_ml "exception" ml_exn)),
1.122 - ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
1.123 - ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
1.124 - ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
1.125 - ("verbatim", O.args (Scan.lift Args.name) output_verbatim),
1.126 - ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))),
1.127 - ("named_thms", O.args (Scan.repeat (Attrib.thm --
1.128 - Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")")))
1.129 - (output_named_list pretty_thm)),
1.130 - ("ML_text", O.args (Scan.lift Args.name) output_ml)];
1.131 + [("named_thms", O.args (Scan.repeat (Attrib.thm --
1.132 + Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) output_named_thms)];
1.133
1.134 end;
1.135 +
1.136 +
1.137 +(* theory files *)
1.138 +
1.139 +val _ = O.add_commands
1.140 + [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
1.141 + (ThyLoad.check_thy Path.current name; Pretty.str name))))];
1.142 +
1.143 +end;