matitaB/matita/applyTransformation.ml

   1 (* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 (***************************************************************************)
  27 (*                                                                         *)
  28 (*                               PROJECT HELM                              *)
  29 (*                                                                         *)
  30 (*                   Andrea Asperti <asperti@cs.unibo.it>                  *)
  31 (*                                21/11/2003                               *)
  32 (*                                                                         *)
  33 (*                                                                         *)
  34 (***************************************************************************)
  35
  36 (* $Id$ *)
  37
  38
  39 let use_high_level_pretty_printer = ref true;;
  40
  41 (*
  42 let to_text to_content to_pres lowlevel ~map_unicode_to_tex size status t =
  43  if !use_high_level_pretty_printer then
  44   let content,ids_to_nrefs = to_content status t in
  45   let pres = to_pres status ~ids_to_nrefs content in
  46   let pres = CicNotationPres.mpres_of_box pres in
  47    BoxPp.render_to_string ~map_unicode_to_tex
  48     (function x::_ -> x | _ -> assert false) size pres
  49  else
  50   [],lowlevel t *)
  51
  52 (* let ntxt_of_cic_sequent ~metasenv ~subst =
  53  to_text (Interpretations.nmap_sequent ~metasenv ~subst)
  54   Content2pres.nsequent2pres
  55   (fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq]) *)
  56
  57 let ntxt_of_cic_sequent ~metasenv ~subst
  58     ~map_unicode_to_tex size status m =
  59   let cseq = Interpretations.nmap_sequent status ~metasenv ~subst m in
  60   let markup = CicNotationPres.render_sequent status cseq in
  61   BoxPp.render_to_string ~map_unicode_to_tex (List.hd) size markup
  62
  63 let ntxt_of_cic_object ~map_unicode_to_tex _ _ _ = [],"TO DO"
  64 (*
  65  to_text Interpretations.nmap_obj Content2pres.nobj2pres ~map_unicode_to_tex
  66   (new NCicPp.status)#ppobj *)
  67
  68 (*
  69 let ntxt_of_cic_term ~metasenv ~subst ~context =
  70  to_text (Interpretations.nmap_term ~metasenv ~subst ~context)
  71   (Content2pres.nterm2pres ?prec:None)
  72   ((new NCicPp.status)#ppterm ~metasenv ~subst ~context)
  73
  74 let ntxt_of_cic_context ~metasenv ~subst =
  75  to_text (Interpretations.nmap_context ~metasenv ~subst)
  76   Content2pres.ncontext2pres
  77   ((new NCicPp.status)#ppcontext ~metasenv ~subst)
  78
  79 let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst =
  80  [],
  81  "<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
  82   (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
  83 *)
  84
  85
  86 class status uid =
  87  object(self)
  88   inherit Interpretations.status uid
  89   inherit TermContentPres.status uid
  90   inherit NCicPp.status uid
  91 (*
  92   method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
  93     NCicPp.ppterm ~metasenv ~subst ~context t
  94
  95   method ppcontext ?sep ~subst ~metasenv context =
  96     NCicPp.ppcontext self ~metasenv ~subst context
  97
  98   method ppsubst ~metasenv ?use_subst subst =
  99     NCicPp.ppcontext self ~metasenv subst *)
 100
 101   method ppmetasenv ~subst metasenv =
 102    String.concat "\n"
 103     (List.map
 104       (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 50 self
 105         ~metasenv ~subst m) metasenv)
 106 (*
 107   method ppobj obj =
 108    snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj) *)
 109  end
 110
 111 let ntxt_of_cic_sequent ~metasenv ~subst
 112     ~map_unicode_to_tex size status m =
 113 [], ntxt_of_cic_sequent ~metasenv ~subst
 114     ~map_unicode_to_tex size status m