- preservation of arity assignment

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / hls.ml

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
index 9c12ae1c74ec42be84a07d4fa057dcd4ec35a6b5..01f59045d18adb38f6dd3652f8002996ac2f282d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
@@ -15,6 +15,19 @@ let rec read ich =
 
 let length l s = max l (String.length s)
 
+let split s =
+try 
+   let i = String.rindex s '.' in
+   if i = 0 then s, "" else
+   String.sub s 0 i, String.sub s i (String.length s - i)    
+with Not_found -> s, ""
+
+let compare s1 s2 =
+   let n1, e1 = split s1 in
+   let n2, e2 = split s2 in
+   let e = String.compare e1 e2 in
+   if e = 0 then String.compare n1 n2 else e
+
 let write l c s =
    let pre, post = if List.mem s !hl then color, normal else "", "" in
    let spc = String.make (l - String.length s) ' ' in
@@ -34,8 +47,8 @@ let help = ""
 let main =
    Arg.parse [] process help;
    let files = Sys.readdir "." in
-   Array.fast_sort String.compare files;
    let l = Array.fold_left length 0 files in
    if cols < l then failwith "window too small";
+   Array.fast_sort compare files;
    let c = Array.fold_left (write l) 0 files in
-   if 0 < c && c < cols then print_newline ()
+   if 0 < c && c < cols then print_newline ();