doc-src/antiquote_setup.ML
changeset 26742 5a86bc79431c
parent 26710 f79aa228c582
child 26751 2b97ea3130c2
     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 +in
    1.79  
    1.80 -fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
    1.81 +val _ = O.add_commands
    1.82 + [("index_ML", ml_args (index_ml "" ml_val)),
    1.83 +  ("index_ML_type", ml_args (index_ml "type" ml_type)),
    1.84 +  ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
    1.85 +  ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
    1.86 +  ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
    1.87 +  ("ML_functor", O.args (Scan.lift Args.name) output_ml),
    1.88 +  ("ML_text", O.args (Scan.lift Args.name) output_ml)];
    1.89  
    1.90 -fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name);
    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;