equal
deleted
inserted
replaced
1 (* Title: Doc/antiquote_setup.ML |
1 (* Title: Doc/antiquote_setup.ML |
2 ID: $Id: antiquote_setup.ML,v 1.27 2008/08/09 20:43:46 wenzelm Exp $ |
2 ID: $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm 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 |
141 val _ = O.add_commands |
141 val _ = O.add_commands |
142 [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => |
142 [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => |
143 (ThyLoad.check_thy Path.current name; Pretty.str name))))]; |
143 (ThyLoad.check_thy Path.current name; Pretty.str name))))]; |
144 |
144 |
145 |
145 |
146 (* Isar entities (with index) *) |
146 (* Isabelle entities (with index) *) |
147 |
147 |
148 local |
148 local |
149 |
149 |
150 fun no_check _ _ = true; |
150 fun no_check _ _ = true; |
151 |
151 |
152 fun thy_check intern defined ctxt = |
152 fun thy_check intern defined ctxt = |
153 let val thy = ProofContext.theory_of ctxt |
153 let val thy = ProofContext.theory_of ctxt |
154 in defined thy o intern thy end; |
154 in defined thy o intern thy end; |
|
155 |
|
156 fun check_tool name = |
|
157 File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name)); |
155 |
158 |
156 val arg = enclose "{" "}" o clean_string; |
159 val arg = enclose "{" "}" o clean_string; |
157 |
160 |
158 fun output_entity check markup index kind ctxt (logic, name) = |
161 fun output_entity check markup index kind ctxt (logic, name) = |
159 let |
162 let |
172 (Output.output name |
175 (Output.output name |
173 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
176 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
174 |> (if ! O.quotes then quote else I) |
177 |> (if ! O.quotes then quote else I) |
175 |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
178 |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
176 else hyper o enclose "\\mbox{\\isa{" "}}")) |
179 else hyper o enclose "\\mbox{\\isa{" "}}")) |
177 else error ("Undefined " ^ kind ^ " " ^ quote name) |
180 else error ("Bad " ^ kind ^ " " ^ quote name) |
178 end; |
181 end; |
179 |
182 |
180 fun entity check markup index kind = |
183 fun entity check markup index kind = |
181 O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
184 O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
182 (K (output_entity check markup index kind)); |
185 (K (output_entity check markup index kind)); |
196 entity_antiqs (thy_check Method.intern Method.defined) "" "method" @ |
199 entity_antiqs (thy_check Method.intern Method.defined) "" "method" @ |
197 entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @ |
200 entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @ |
198 entity_antiqs no_check "" "fact" @ |
201 entity_antiqs no_check "" "fact" @ |
199 entity_antiqs no_check "" "variable" @ |
202 entity_antiqs no_check "" "variable" @ |
200 entity_antiqs no_check "" "case" @ |
203 entity_antiqs no_check "" "case" @ |
201 entity_antiqs (K ThyOutput.defined_command) "" "antiquotation"); |
204 entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @ |
202 |
205 entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @ |
203 end; |
206 entity_antiqs no_check "isatt" "executable" @ |
204 |
207 entity_antiqs (K check_tool) "isatt" "tool" @ |
205 end; |
208 entity_antiqs (K (File.exists o Path.explode)) "isatt" "file"); |
|
209 |
|
210 end; |
|
211 |
|
212 end; |