From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libobject.ml | 50 +++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index 504c1ffdd..95894294b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -25,7 +25,7 @@ let relax_flag = ref false;; let relax b = relax_flag := b;; -type 'a substitutivity = +type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a type 'a object_declaration = { @@ -46,12 +46,12 @@ let default_object s = { cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); - subst_function = (fun _ -> + subst_function = (fun _ -> yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x); - export_function = (fun _ -> None)} + export_function = (fun _ -> None)} (* The suggested object declaration is the following: @@ -59,7 +59,7 @@ let default_object s = { declare_object { (default_object "MY OBJECT") with cache_function = fun (sp,a) -> Mytbl.add sp a} - and the listed functions are only those which definitions accually + and the listed functions are only those which definitions accually differ from the default. This helps introducing new functions in objects. @@ -81,7 +81,7 @@ type dynamic_object_declaration = { let object_tag lobj = Dyn.tag lobj -let cache_tab = +let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object odecl = @@ -96,34 +96,34 @@ let declare_object odecl = and opener i (oname,lobj) = if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the openfun" - and substituter (oname,sub,lobj) = - if Dyn.tag lobj = na then + and substituter (oname,sub,lobj) = + if Dyn.tag lobj = na then infun (odecl.subst_function (oname,sub,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the substfun" - and classifier lobj = - if Dyn.tag lobj = na then + and classifier lobj = + if Dyn.tag lobj = na then match odecl.classify_function (outfun lobj) with | Dispose -> Dispose | Substitute obj -> Substitute (infun obj) | Keep obj -> Keep (infun obj) | Anticipate (obj) -> Anticipate (infun obj) - else + else anomaly "somehow we got the wrong dynamic object in the classifyfun" - and discharge (oname,lobj) = - if Dyn.tag lobj = na then + and discharge (oname,lobj) = + if Dyn.tag lobj = na then Option.map infun (odecl.discharge_function (oname,outfun lobj)) - else + else anomaly "somehow we got the wrong dynamic object in the dischargefun" - and rebuild lobj = + and rebuild lobj = if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" - and exporter lobj = - if Dyn.tag lobj = na then + and exporter lobj = + if Dyn.tag lobj = na then Option.map infun (odecl.export_function (outfun lobj)) - else + else anomaly "somehow we got the wrong dynamic object in the exportfun" - in + in Hashtbl.add cache_tab na { dyn_cache_function = cacher; dyn_load_function = loader; dyn_open_function = opener; @@ -144,13 +144,13 @@ let apply_dyn_fun deflt f lobj = let dodecl = try Hashtbl.find cache_tab tag - with Not_found -> + with Not_found -> if !relax_flag then failwith "local to_apply_dyn_fun" else error ("Cannot find library functions for an object with tag "^tag^ - " (maybe a plugin is missing)") in + " (maybe a plugin is missing)") in f dodecl with Failure "local to_apply_dyn_fun" -> deflt;; @@ -158,19 +158,19 @@ let apply_dyn_fun deflt f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj -let load_object i ((_,lobj) as node) = +let load_object i ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj -let open_object i ((_,lobj) as node) = +let open_object i ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj -let subst_object ((_,_,lobj) as node) = +let subst_object ((_,_,lobj) as node) = apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj -let classify_object lobj = +let classify_object lobj = apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj -let discharge_object ((_,lobj) as node) = +let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj let rebuild_object lobj = -- cgit v1.2.3