--- 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;