src/Pure/General/long_name.ML
changeset 59916 f673ce6b1e2b
parent 59888 27e4d0ab0948
child 65358 e345e9420109
equal deleted inserted replaced
59915:7d5b2f4c621c 59916:f673ce6b1e2b
     7 signature LONG_NAME =
     7 signature LONG_NAME =
     8 sig
     8 sig
     9   val separator: string
     9   val separator: string
    10   val is_qualified: string -> bool
    10   val is_qualified: string -> bool
    11   val hidden: string -> string
    11   val hidden: string -> string
       
    12   val is_hidden: string -> bool
    12   val dest_hidden: string -> string option
    13   val dest_hidden: string -> string option
    13   val localN: string
    14   val localN: string
    14   val dest_local: string -> string option
    15   val dest_local: string -> string option
    15   val implode: string list -> string
    16   val implode: string list -> string
    16   val explode: string -> string list
    17   val explode: string -> string list
    27 
    28 
    28 val separator = ".";
    29 val separator = ".";
    29 
    30 
    30 val is_qualified = exists_string (fn s => s = separator);
    31 val is_qualified = exists_string (fn s => s = separator);
    31 
    32 
    32 val hidden = prefix "??.";
    33 val hidden_prefix = "??."
    33 val dest_hidden = try (unprefix "??.");
    34 val hidden = prefix hidden_prefix;
       
    35 val is_hidden = String.isPrefix hidden_prefix;
       
    36 val dest_hidden = try (unprefix hidden_prefix);
    34 
    37 
    35 val localN = "local";
    38 val localN = "local";
    36 val dest_local = try (unprefix "local.");
    39 val dest_local = try (unprefix "local.");
    37 
    40 
    38 val implode = space_implode separator;
    41 val implode = space_implode separator;