X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FhelmGtkLogger.ml;fp=helm%2FgTopLevel%2FhelmGtkLogger.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=cfb2c487a0c73403e6b90d0c9cbaae4c8b8f5f49;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/gTopLevel/helmGtkLogger.ml b/helm/gTopLevel/helmGtkLogger.ml deleted file mode 100644 index cfb2c487a..000000000 --- a/helm/gTopLevel/helmGtkLogger.ml +++ /dev/null @@ -1,71 +0,0 @@ -(* 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 -