equal
deleted
inserted
replaced
1 (* Title: Doc/antiquote_setup.ML |
1 (* Title: Doc/antiquote_setup.ML |
2 ID: $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm Exp $ |
2 ID: $Id: antiquote_setup.ML,v 1.32 2008/09/29 10:31:56 haftmann Exp $ |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Auxiliary antiquotations for the Isabelle manuals. |
5 Auxiliary antiquotations for the Isabelle manuals. |
6 *) |
6 *) |
7 |
7 |
73 if kind = "type" then txt1 ^ " = " ^ txt2 |
73 if kind = "type" then txt1 ^ " = " ^ txt2 |
74 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
74 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
75 else txt1 ^ ": " ^ txt2; |
75 else txt1 ^ ": " ^ txt2; |
76 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
76 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
77 val _ = writeln (ml (txt1, txt2)); |
77 val _ = writeln (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2)); |
78 val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2)); |
79 in |
79 in |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
80 "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^ |
81 ((if ! O.source then str_of_source src else txt') |
81 ((if ! O.source then str_of_source src else txt') |
82 |> (if ! O.quotes then quote else I) |
82 |> (if ! O.quotes then quote else I) |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
83 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
203 entity_antiqs no_check "" "case" @ |
203 entity_antiqs no_check "" "case" @ |
204 entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @ |
204 entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @ |
205 entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @ |
205 entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @ |
206 entity_antiqs no_check "isatt" "executable" @ |
206 entity_antiqs no_check "isatt" "executable" @ |
207 entity_antiqs (K check_tool) "isatt" "tool" @ |
207 entity_antiqs (K check_tool) "isatt" "tool" @ |
208 entity_antiqs (K (File.exists o Path.explode)) "isatt" "file"); |
208 entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @ |
209 |
209 entity_antiqs (K ThyInfo.known_thy) "" "theory"); |
210 end; |
210 |
211 |
211 end; |
212 end; |
212 |
|
213 end; |