logger added

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index e6a5cbbc26e2fe24ee11575800fffae2aea2352a..96b2f9186fcc7ebfcec7714e9a35f6d1fe66df0a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -11,6 +11,14 @@
 
 (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
 
+(* web interface stuff *)
+
+let logger = 
+  ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
@@ -1124,13 +1132,12 @@ and returns_a_coinductive ~subst context ty =
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
-and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
-(* ALIAS typecheck *)
-(*
-  let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
-       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
-     | CicEnvironment.UncheckedObj uobj ->
+and type_of_constant ref = 
+assert false        (*
+  let cobj =
+   match E.get_obj uri with
+   | true, cobj -> cobj
+   | false, uobj ->
          logger#log (`Start_type_checking uri) ;
          let ugraph1_dust =
           typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 51aa6458d11845d67f75dcccadf77ff65211483a..c333430b91c02db578deaa9a959bbf06ae7fac76 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -34,3 +34,6 @@ val typeof:
   NCic.context -> NCic.term -> 
     NCic.term
 
+val set_logger: 
+  ([ `Start_type_checking of NUri.uri 
+   | `Type_checking_completed of NUri.uri ] -> unit) -> unit