src/Pure/General/long_name.ML
changeset 59916 f673ce6b1e2b
parent 59888 27e4d0ab0948
child 65358 e345e9420109
--- a/src/Pure/General/long_name.ML	Thu Apr 02 20:46:44 2015 +0200
+++ b/src/Pure/General/long_name.ML	Fri Apr 03 18:36:19 2015 +0200
@@ -9,6 +9,7 @@
   val separator: string
   val is_qualified: string -> bool
   val hidden: string -> string
+  val is_hidden: string -> bool
   val dest_hidden: string -> string option
   val localN: string
   val dest_local: string -> string option
@@ -29,8 +30,10 @@
 
 val is_qualified = exists_string (fn s => s = separator);
 
-val hidden = prefix "??.";
-val dest_hidden = try (unprefix "??.");
+val hidden_prefix = "??."
+val hidden = prefix hidden_prefix;
+val is_hidden = String.isPrefix hidden_prefix;
+val dest_hidden = try (unprefix hidden_prefix);
 
 val localN = "local";
 val dest_local = try (unprefix "local.");