more direct Long_Name.qualification;
authorwenzelm
Mon Mar 10 10:04:26 2014 +0100 (2014-03-10)
changeset 56023f252a315c26e
parent 56022 8c9ab5d91d5a
child 56024 0921c1dc344c
more direct Long_Name.qualification;
src/Pure/General/long_name.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/General/long_name.ML	Mon Mar 10 09:54:01 2014 +0100
     1.2 +++ b/src/Pure/General/long_name.ML	Mon Mar 10 10:04:26 2014 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val implode: string list -> string
     1.5    val explode: string -> string list
     1.6    val append: string -> string -> string
     1.7 +  val qualification: string -> int
     1.8    val qualify: string -> string -> string
     1.9    val qualifier: string -> string
    1.10    val base_name: string -> string
    1.11 @@ -35,6 +36,9 @@
    1.12    | append "" name2 = name2
    1.13    | append name1 name2 = name1 ^ separator ^ name2;
    1.14  
    1.15 +fun qualification "" = 0
    1.16 +  | qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1;
    1.17 +
    1.18  fun qualify qual name =
    1.19    if qual = "" orelse name = "" then name
    1.20    else qual ^ separator ^ name;
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Mar 10 09:54:01 2014 +0100
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Mar 10 10:04:26 2014 +0100
     2.3 @@ -330,7 +330,7 @@
     2.4  
     2.5  val index_ord = option_ord (K EQUAL);
     2.6  val hidden_ord = bool_ord o pairself Long_Name.is_hidden;
     2.7 -val qual_ord = int_ord o pairself (length o Long_Name.explode);
     2.8 +val qual_ord = int_ord o pairself Long_Name.qualification;
     2.9  val txt_ord = int_ord o pairself size;
    2.10  
    2.11  fun nicer_name (x, i) (y, j) =