144 |
144 |
145 local |
145 local |
146 |
146 |
147 fun no_check _ _ = true; |
147 fun no_check _ _ = true; |
148 |
148 |
149 fun thy_check intern defined ctxt = |
149 fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt)); |
150 let val thy = Proof_Context.theory_of ctxt |
150 |
151 in defined thy o intern thy end; |
151 fun check_tool (name, pos) = |
152 |
152 let |
153 fun check_tool name = |
153 (* FIXME ISABELLE_TOOLS !? *) |
154 let val tool_dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"] |
154 val dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"]; |
155 in exists (fn dir => File.exists (Path.append dir (Path.basic name))) tool_dirs end; |
155 fun tool dir = |
|
156 let val path = Path.append dir (Path.basic name) |
|
157 in if File.exists path then SOME path else NONE end; |
|
158 in |
|
159 (case get_first tool dirs of |
|
160 NONE => false |
|
161 | SOME path => (Position.report pos (Markup.path (Path.implode path)); true)) |
|
162 end; |
156 |
163 |
157 val arg = enclose "{" "}" o clean_string; |
164 val arg = enclose "{" "}" o clean_string; |
158 |
165 |
159 fun entity check markup kind index = |
166 fun entity check markup kind index = |
160 Thy_Output.antiquotation |
167 Thy_Output.antiquotation |
161 (Binding.name (translate (fn " " => "_" | c => c) kind ^ |
168 (Binding.name (translate (fn " " => "_" | c => c) kind ^ |
162 (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
169 (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
163 (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) |
170 (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
164 (fn {context = ctxt, ...} => fn (logic, name) => |
171 (fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
165 let |
172 let |
166 val hyper_name = |
173 val hyper_name = |
167 "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
174 "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
168 val hyper = |
175 val hyper = |
169 enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
176 enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
172 (case index of |
179 (case index of |
173 NONE => "" |
180 NONE => "" |
174 | SOME is_def => |
181 | SOME is_def => |
175 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
182 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
176 in |
183 in |
177 if check ctxt name then |
184 if check ctxt (name, pos) then |
178 idx ^ |
185 idx ^ |
179 (Output.output name |
186 (Output.output name |
180 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
187 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
181 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
188 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
182 |> (if Config.get ctxt Thy_Output.display |
189 |> (if Config.get ctxt Thy_Output.display |
183 then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
190 then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
184 else hyper o enclose "\\mbox{\\isa{" "}}")) |
191 else hyper o enclose "\\mbox{\\isa{" "}}")) |
185 else error ("Bad " ^ kind ^ " " ^ quote name) |
192 else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
186 end); |
193 end); |
187 |
194 |
188 fun entity_antiqs check markup kind = |
195 fun entity_antiqs check markup kind = |
189 entity check markup kind NONE #> |
196 entity check markup kind NONE #> |
190 entity check markup kind (SOME true) #> |
197 entity check markup kind (SOME true) #> |
192 |
199 |
193 in |
200 in |
194 |
201 |
195 val entity_setup = |
202 val entity_setup = |
196 entity_antiqs no_check "" "syntax" #> |
203 entity_antiqs no_check "" "syntax" #> |
197 entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command" #> |
204 entity_antiqs (K (is_some o Keyword.command_keyword o #1)) "isacommand" "command" #> |
198 entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword" #> |
205 entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #> |
199 entity_antiqs (K Keyword.is_keyword) "isakeyword" "element" #> |
206 entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #> |
200 entity_antiqs (thy_check Method.intern Method.defined) "" "method" #> |
207 entity_antiqs (thy_check Method.check) "" "method" #> |
201 entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" #> |
208 entity_antiqs (thy_check Attrib.check) "" "attribute" #> |
202 entity_antiqs no_check "" "fact" #> |
209 entity_antiqs no_check "" "fact" #> |
203 entity_antiqs no_check "" "variable" #> |
210 entity_antiqs no_check "" "variable" #> |
204 entity_antiqs no_check "" "case" #> |
211 entity_antiqs no_check "" "case" #> |
205 entity_antiqs (thy_check Thy_Output.intern_command Thy_Output.defined_command) |
212 entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #> |
206 "" "antiquotation" #> |
213 entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #> |
207 entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option) |
|
208 "" "antiquotation option" #> |
|
209 entity_antiqs no_check "isatt" "setting" #> |
214 entity_antiqs no_check "isatt" "setting" #> |
210 entity_antiqs no_check "isatt" "system option" #> |
215 entity_antiqs no_check "isatt" "system option" #> |
211 entity_antiqs no_check "" "inference" #> |
216 entity_antiqs no_check "" "inference" #> |
212 entity_antiqs no_check "isatt" "executable" #> |
217 entity_antiqs no_check "isatt" "executable" #> |
213 entity_antiqs (K check_tool) "isatool" "tool" #> |
218 entity_antiqs (K check_tool) "isatool" "tool" #> |
214 entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) |
219 entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN; |
215 "" Markup.ML_antiquotationN; |
|
216 |
220 |
217 end; |
221 end; |
218 |
222 |
219 |
223 |
220 (* theory setup *) |
224 (* theory setup *) |