src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36478 1aba777a367f
parent 36402 1b20805974c7
child 36486 c2d7e2dff59e
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 14:55:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 16:00:20 2010 +0200
@@ -14,6 +14,8 @@
   val timestamp : unit -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
+  val unyxml : string -> string
+  val maybe_quote : string -> string
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -72,4 +74,16 @@
         SOME (Time.fromMilliseconds msecs)
     end
 
+fun plain_string_from_xml_tree t =
+  Buffer.empty |> XML.add_content t |> Buffer.content
+val unyxml = plain_string_from_xml_tree o YXML.parse
+
+val is_long_identifier = forall Syntax.is_identifier o space_explode "."
+fun maybe_quote y =
+  let val s = unyxml y in
+    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
+           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
+           OuterKeyword.is_keyword s) ? quote
+  end
+
 end;