From 98295941bee765a0cb4070eb3f2df553228c11c8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 11 Feb 2004 12:04:16 +0000 Subject: [PATCH] new logger --- helm/gTopLevel/helmGtkLogger.ml | 71 +++++++++++++++++++ helm/gTopLevel/helmGtkLogger.mli | 31 ++++++++ helm/ocaml/cic_proof_checking/Makefile | 6 +- .../cic_proof_checking/cicEnvironment.ml | 8 +-- helm/ocaml/cic_proof_checking/cicLogger.ml | 36 ++-------- helm/ocaml/cic_proof_checking/cicLogger.mli | 9 +-- 6 files changed, 118 insertions(+), 43 deletions(-) create mode 100644 helm/gTopLevel/helmGtkLogger.ml create mode 100644 helm/gTopLevel/helmGtkLogger.mli diff --git a/helm/gTopLevel/helmGtkLogger.ml b/helm/gTopLevel/helmGtkLogger.ml new file mode 100644 index 000000000..cfb2c487a --- /dev/null +++ b/helm/gTopLevel/helmGtkLogger.ml @@ -0,0 +1,71 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class html_logger ?width ?height ?packing ?show () = + let scrolled_window = GBin.scrolled_window ?packing ?show () in + let vadj = scrolled_window#vadjustment in + let tv = + GText.view ~editable:false ~cursor_visible:false + ?width ?height ~packing:(scrolled_window#add) () + in + let colors = Hashtbl.create 13 in + let get_color color = + try + Hashtbl.find colors color + with Not_found -> + let tag = + tv#buffer#create_tag + [`FOREGROUND_SET true ; + `FOREGROUND_GDK + (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME color))] + in + Hashtbl.add colors color tag; + tag + in + let log ?(append_NL = true) msg = + let rec aux color indent = + let indent_str = String.make indent ' ' in + function + | `T s -> tv#buffer#insert ~tags:[ get_color color ] s + | `L tags -> + List.iter + (fun tag -> aux color indent tag; tv#buffer#insert indent_str) + tags + | `BR -> tv#buffer#insert ("\n" ^ indent_str) + | `DIV (local_indent, new_color, tag) -> + tv#buffer#insert ("\n" ^ indent_str); + aux + (match new_color with None -> color | Some new_color -> new_color) + (indent + local_indent) tag + in + (match msg with + | `Error tag -> aux "red" 0 tag + | `Msg tag -> aux "black" 0 tag); + if append_NL then tv#buffer#insert "\n" + in + object (self) + initializer HelmLogger.register_log_callback log + end + diff --git a/helm/gTopLevel/helmGtkLogger.mli b/helm/gTopLevel/helmGtkLogger.mli new file mode 100644 index 000000000..06206dd3d --- /dev/null +++ b/helm/gTopLevel/helmGtkLogger.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class html_logger: + ?width:int -> ?height:int -> ?packing:(GObj.widget -> unit) -> ?show:bool -> + unit -> + object + end + diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 96ac166b5..61d7d5002 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -1,11 +1,13 @@ + PACKAGE = cic_proof_checking -REQUIRES = helm-cic +REQUIRES = helm-cic helm-logger helm-getter PREDICATES = REDUCTION_IMPLEMENTATION = cicReductionMachine.ml INTERFACE_FILES = \ - cicLogger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ + cicLogger.mli \ + cicEnvironment.mli cicPp.mli cicSubstitution.mli \ cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ cicTypeChecker.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 22138dde8..45c0dba5a 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -303,17 +303,17 @@ let find_or_add_unchecked_to_cache uri = Cache.find_or_add_unchecked uri ~get_object_to_add: (function () -> - let filename = Getter.getxml uri in + let filename = Http_getter.getxml' uri in let bodyfilename = match UriManager.bodyuri_of_uri uri with None -> None | Some bodyuri -> try - ignore (Getter.resolve bodyuri) ; + ignore (Http_getter.resolve' bodyuri) ; (* The body exists ==> it is not an axiom *) - Some (Getter.getxml bodyuri) + Some (Http_getter.getxml' bodyuri) with - Getter.Unresolved -> + Http_getter_types.Unresolvable_URI _ -> (* The body does not exist ==> we consider it an axiom *) None in diff --git a/helm/ocaml/cic_proof_checking/cicLogger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml index 9fc983fc7..6867b8b92 100644 --- a/helm/ocaml/cic_proof_checking/cicLogger.ml +++ b/helm/ocaml/cic_proof_checking/cicLogger.ml @@ -28,39 +28,17 @@ type msg = | `Type_checking_completed of UriManager.uri | `Trusting of UriManager.uri ] -;; -let log_to_html ~print_and_flush = +let log = let module U = UriManager in - let indent = ref 0 in - let mkindent () = - String.make !indent ' ' - in function | `Start_type_checking uri -> - print_and_flush ( - mkindent () ^ - "
" ^ - "Type-Checking of " ^ (U.string_of_uri uri) ^ " started
\n" - ) ; - incr indent + HelmLogger.log (`Msg (`DIV (1, None, `T + ("Type-Checking of " ^ (U.string_of_uri uri) ^ " started")))) | `Type_checking_completed uri -> - decr indent ; - print_and_flush ( - mkindent () ^ - "
" ^ - "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.
\n" - ) + HelmLogger.log (`Msg (`DIV (1, Some "green", `T + ("Type-Checking of " ^ (U.string_of_uri uri) ^ " completed")))) | `Trusting uri -> - print_and_flush ( - mkindent () ^ - "
" ^ - (U.string_of_uri uri) ^ " is trusted.
\n" - ) -;; + HelmLogger.log (`Msg (`DIV (1, Some "blue", `T + ((U.string_of_uri uri) ^ " is trusted.")))) -let log_callback = ref (function (_:msg) -> ()) -let log msg = !log_callback msg;; diff --git a/helm/ocaml/cic_proof_checking/cicLogger.mli b/helm/ocaml/cic_proof_checking/cicLogger.mli index 781abdef6..848b30573 100644 --- a/helm/ocaml/cic_proof_checking/cicLogger.mli +++ b/helm/ocaml/cic_proof_checking/cicLogger.mli @@ -28,13 +28,6 @@ type msg = | `Type_checking_completed of UriManager.uri | `Trusting of UriManager.uri ] -;; -(* A callback that can be used to log to html *) -val log_to_html : print_and_flush:(string -> unit) -> msg -> unit +val log: msg -> unit -(* The log function used. The default does nothing. *) -val log_callback : (msg -> unit) ref - -(* Log something via log_callback *) -val log : msg -> unit -- 2.39.2