+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+let debug = true
+let ignore_exc = false
+let rank_all_dependencies = false
+let trust_environment = false
+let print_object = true
+
+let indent = ref 0;;
+
+let load_graph, get_graph =
+ let oldg = ref CicUniv.empty_ugraph in
+ (function uri ->
+ let _,g = CicEnvironment.get_obj !oldg uri in
+ oldg := g),
+ (function _ -> !oldg)
+;;
+
+let logger =
+ let do_indent () = String.make !indent ' ' in
+ (function
+ | `Start_type_checking s ->
+ if debug then
+ prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s);
+ incr indent
+ | `Type_checking_completed s ->
+ decr indent;
+ if debug then
+ prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+ | `Type_checking_interrupted s ->
+ decr indent;
+ if debug then
+ prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
+ | `Type_checking_failed s ->
+ decr indent;
+ if debug then
+ prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
+ | `Trust_obj s ->
+ if debug then
+ prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
+;;
+
+let mk_type n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+;;
+let mk_cprop n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+;;
+
+
+let _ =
+ let do_old_logging = ref true in
+ HelmLogger.register_log_callback
+ (fun ?append_NL html_msg ->
+ if !do_old_logging then
+ prerr_endline (HelmLogger.string_of_html_msg html_msg));
+ CicParser.impredicative_set := false;
+ NCicTypeChecker.set_logger logger;