X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fground.ml;h=7eebedb7d13e8fa810c4dc0eb867aa038362e474;hb=05b047be6817f430c8c72fd9b0902df8bb9f579e;hp=022ab63f2466be39c1c41c874138d636a4137ab6;hpb=ea6b4322051d3eb1794bfca3928f6e1773f971ba;p=helm.git diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index 022ab63f2..7eebedb7d 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -17,16 +17,20 @@ exception Error of string (* interface functions ******************************************************) +let id x = x + +let id2 x y = x, y + let rec segments_of_string ss l s = match try Some (S.index s '/') with Not_found -> None with | None -> s :: ss | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1)) -let rec rev_concat sep r = function +let rec rev_map_concat map sep r = function | [] -> r | s :: ss -> - if r = "" then rev_concat sep s ss else - rev_concat sep (s ^ sep ^ r) ss + if r = "" then rev_map_concat map sep (map s) ss else + rev_map_concat map sep (map s ^ sep ^ r) ss let fold_string map a s = let l = S.length s in @@ -44,10 +48,21 @@ let rec foldi_left mapi i a = function | [] -> a | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl +let rec rev_mapi mapi i l = + let map i a hd = mapi i hd :: a in + foldi_left map i [] l + let rec rev_map_append map l r = match l with | [] -> r | hd :: tl -> rev_map_append map tl (map hd :: r) +let rec split_at x = function + | l when x <= 0 -> [], l + | [] -> [], [] + | hd :: tl -> + let l1, l2 = split_at (pred x) tl in + hd :: l1, l2 + let error s = raise (Error s) -let log s = P.eprintf "MaTeX: %s\n" s +let log s = P.eprintf "MaTeX: %s\n%!" s