src/Pure/General/long_name.ML
changeset 55669 4612c450b59c
parent 30359 3f9b3ff851ca
child 56023 f252a315c26e
--- a/src/Pure/General/long_name.ML	Sat Feb 22 16:16:21 2014 +0100
+++ b/src/Pure/General/long_name.ML	Sat Feb 22 16:58:02 2014 +0100
@@ -8,6 +8,8 @@
 sig
   val separator: string
   val is_qualified: string -> bool
+  val hidden: string -> string
+  val is_hidden: string -> bool
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
@@ -23,6 +25,9 @@
 val separator = ".";
 val is_qualified = exists_string (fn s => s = separator);
 
+fun hidden name = "??." ^ name;
+val is_hidden = String.isPrefix "??.";
+
 val implode = space_implode separator;
 val explode = space_explode separator;