diff -r 6e97c1766500 -r 4612c450b59c src/Pure/General/long_name.ML --- 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;