helm/gTopLevel/helmGtkLogger.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 class html_logger ?width ?height ?packing ?show () =
  27  let scrolled_window = GBin.scrolled_window ?packing ?show () in
  28  let vadj = scrolled_window#vadjustment in
  29  let tv =
  30    GText.view ~editable:false ~cursor_visible:false
  31     ?width ?height ~packing:(scrolled_window#add) ()
  32  in
  33  let colors = Hashtbl.create 13 in
  34  let get_color color =
  35    try
  36      Hashtbl.find colors color
  37    with Not_found ->
  38      let tag =
  39        tv#buffer#create_tag
  40         [`FOREGROUND_SET true ;
  41          `FOREGROUND_GDK
  42           (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME color))]
  43      in
  44      Hashtbl.add colors color tag;
  45      tag
  46  in
  47   let log ?(append_NL = true) msg =
  48     let rec aux color indent =
  49       let indent_str = String.make indent ' ' in
  50       function
  51       | `T s -> tv#buffer#insert ~tags:[ get_color color ] s
  52       | `L tags ->
  53           List.iter
  54             (fun tag -> aux color indent tag; tv#buffer#insert indent_str)
  55             tags
  56       | `BR -> tv#buffer#insert ("\n" ^ indent_str)
  57       | `DIV (local_indent, new_color, tag) ->
  58           tv#buffer#insert ("\n" ^ indent_str);
  59           aux
  60             (match new_color with None -> color | Some new_color -> new_color)
  61             (indent + local_indent) tag
  62     in
  63     (match msg with
  64     | `Error tag -> aux "red" 0 tag
  65     | `Msg tag -> aux "black" 0 tag);
  66     if append_NL then tv#buffer#insert "\n"
  67   in
  68   object (self)
  69     initializer HelmLogger.register_log_callback log
  70   end
  71