equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Nitpick/nitpick_util.ML |
1 (* Title: HOL/Tools/Nitpick/nitpick_util.ML |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2008, 2009 |
3 Copyright 2008, 2009, 2010 |
4 |
4 |
5 General-purpose functions used by the Nitpick modules. |
5 General-purpose functions used by the Nitpick modules. |
6 *) |
6 *) |
7 |
7 |
8 signature NITPICK_UTIL = |
8 signature NITPICK_UTIL = |
56 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b |
56 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b |
57 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic |
57 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic |
58 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b |
58 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b |
59 val indent_size : int |
59 val indent_size : int |
60 val pstrs : string -> Pretty.T list |
60 val pstrs : string -> Pretty.T list |
61 val plain_string_from_yxml : string -> string |
61 val unyxml : string -> string |
62 val maybe_quote : string -> string |
62 val maybe_quote : string -> string |
63 end |
63 end |
64 |
64 |
65 structure Nitpick_Util : NITPICK_UTIL = |
65 structure Nitpick_Util : NITPICK_UTIL = |
66 struct |
66 struct |
276 |
276 |
277 (* XML.tree -> string *) |
277 (* XML.tree -> string *) |
278 fun plain_string_from_xml_tree t = |
278 fun plain_string_from_xml_tree t = |
279 Buffer.empty |> XML.add_content t |> Buffer.content |
279 Buffer.empty |> XML.add_content t |> Buffer.content |
280 (* string -> string *) |
280 (* string -> string *) |
281 val plain_string_from_yxml = plain_string_from_xml_tree o YXML.parse |
281 val unyxml = plain_string_from_xml_tree o YXML.parse |
282 |
282 |
283 (* string -> bool *) |
283 (* string -> bool *) |
284 val is_long_identifier = forall Syntax.is_identifier o space_explode "." |
284 val is_long_identifier = forall Syntax.is_identifier o space_explode "." |
285 (* string -> string *) |
285 (* string -> string *) |
286 fun maybe_quote y = |
286 fun maybe_quote y = |
287 let val s = plain_string_from_yxml y in |
287 let val s = unyxml y in |
288 y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse |
288 y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse |
289 OuterKeyword.is_keyword s) ? quote |
289 OuterKeyword.is_keyword s) ? quote |
290 end |
290 end |
291 |
291 |
292 end; |
292 end; |