helm/gTopLevel/texTermEditor.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 let debug = true
  27 let debug_print s = if debug then prerr_endline s
  28
  29 (******************************************************************************)
  30 (*                                                                            *)
  31 (*                               PROJECT HELM                                 *)
  32 (*                                                                            *)
  33 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  34 (*                                 06/01/2002                                 *)
  35 (*                                                                            *)
  36 (*                                                                            *)
  37 (******************************************************************************)
  38
  39 (* A WIDGET TO ENTER CIC TERMS *)
  40
  41 class type term_editor =
  42  object
  43    method coerce : GObj.widget
  44    (* get_as_string returns the unquoted string *)
  45    method get_as_string : string
  46    method get_metasenv_and_term :
  47      context:Cic.context ->
  48      metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
  49    method reset : unit
  50    (* The input of set_term is unquoted *)
  51    method set_term : string -> unit
  52    method environment : DisambiguatingParser.EnvironmentP3.t ref
  53  end
  54 ;;
  55
  56 module Make(C:DisambiguateTypes.Callbacks) =
  57   struct
  58
  59    module Disambiguate' = DisambiguatingParser.Make(C);;
  60
  61    class term_editor_impl
  62     mqi_handle
  63     ?packing ?width ?height
  64     ?isnotempty_callback ?share_environment_with () : term_editor
  65    =
  66     let mmlwidget =
  67      GMathViewAux.single_selection_math_view
  68       ?packing ?width ?height () in
  69 (*
  70     let drawing_area = mmlwidget#get_drawing_area in
  71     let _ = drawing_area#misc#set_can_focus true in
  72     let _ = drawing_area#misc#grab_focus () in
  73 *)
  74     let logger =
  75      fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in
  76     let tex_editor =
  77      Mathml_editor.create
  78       ~alt_lexer:true
  79       ~dictionary_uri:"dictionary-cic.xml"
  80       ~mml_uri:Mathml_editor.default_mathml_stylesheet_path
  81 (*CSC: togliere il path assoluto
  82       ~tml_uri:Mathml_editor.default_tex_stylesheet_path
  83 *)
  84       ~tml_uri:"/usr/share/editex/tml-litex.xsl"
  85       ~log:logger
  86     in
  87 (*
  88     let _ =
  89      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press
  90       ~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in
  91 *)
  92     let _ =
  93 (*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in *)
  94      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_in
  95        ~callback:
  96          (fun _ ->
  97            mmlwidget#freeze ;
  98            Mathml_editor.cursor_show ~editor:tex_editor ;
  99            mmlwidget#thaw ;
 100            true) in
 101     let _ =
 102 (*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out *)
 103      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_out
 104        ~callback:
 105          (fun _ ->
 106            mmlwidget#freeze ;
 107            Mathml_editor.cursor_hide ~editor:tex_editor ;
 108            mmlwidget#thaw ;
 109            true) in
 110     let _ = Mathml_editor.push tex_editor '$' in
 111     let dom_tree = Mathml_editor.get_mml tex_editor in
 112     let _ = mmlwidget#load_root dom_tree#get_documentElement in
 113     let _ =
 114 (*      drawing_area#event#connect#key_press *)
 115      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#key_press
 116       (function e ->
 117         let key = GdkEvent.Key.keyval e in
 118          mmlwidget#freeze ;
 119          if
 120           key >= 32 && key < 256 &&
 121            (GdkEvent.Key.state e = [] || GdkEvent.Key.state e = [`SHIFT])
 122          then
 123           Mathml_editor.push tex_editor (Char.chr key)
 124          else if key = GdkKeysyms._u then
 125           begin
 126            mmlwidget#freeze ;
 127            ignore (Mathml_editor.freeze tex_editor) ;
 128            Mathml_editor.reset tex_editor ;
 129            Mathml_editor.push tex_editor '$' ;
 130            ignore (Mathml_editor.thaw tex_editor) ;
 131            mmlwidget#thaw
 132           end
 133          else if key = GdkKeysyms._BackSpace then
 134           Mathml_editor.drop tex_editor
 135            (List.mem `CONTROL (GdkEvent.Key.state e))
 136          else if key = GdkKeysyms._v then
 137            ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
 138          let hadj, _ = mmlwidget#get_adjustments in
 139           mmlwidget#thaw ;
 140           hadj#set_value hadj#upper ;
 141           false) in
 142     let environment =
 143      match share_environment_with with
 144         None ->
 145          ref
 146           (DisambiguatingParser.EnvironmentP3.of_string
 147             DisambiguatingParser.EnvironmentP3.empty)
 148       | Some obj -> obj#environment
 149     in
 150     let _ =
 151      match isnotempty_callback with
 152         None -> ()
 153       | Some callback ->
 154          (* This approximation of the test that checks if the tree is empty *)
 155          (* is utterly unprecise. We assume a tree to look as an empty tree *)
 156          (* iff it is made of just one node m:mtext (which should be the    *)
 157          (* cursor).                                                        *)
 158          let is_empty_tree () =
 159           let root = dom_tree#get_documentElement in
 160            match root#get_firstChild with
 161               None -> true
 162             | Some n -> n#get_nodeName#to_string = "m:mtext"
 163          in
 164           dom_tree#addEventListener
 165            ~typ:(Gdome.domString "DOMSubtreeModified")
 166            ~listener:
 167              (Gdome.eventListener
 168                (function _ -> callback (not (is_empty_tree ()))))
 169            ~useCapture:false
 170     in
 171      object(self)
 172
 173       initializer
 174         ignore (mmlwidget#misc#connect#selection_received
 175           ~callback: (fun selection_data ~time ->
 176             let input = try selection_data#data with Gpointer.Null -> "" in
 177             mmlwidget#freeze ;
 178             ignore (Mathml_editor.freeze tex_editor) ;
 179             for i = 0 to String.length input - 1 do
 180              Mathml_editor.push tex_editor input.[i]
 181             done;
 182             ignore (Mathml_editor.thaw tex_editor) ;
 183             mmlwidget#thaw))
 184
 185       method coerce = mmlwidget#coerce
 186       method reset =
 187        mmlwidget#freeze ;
 188        ignore (Mathml_editor.freeze tex_editor) ;
 189        Mathml_editor.reset tex_editor ;
 190        Mathml_editor.push tex_editor '$' ;
 191        ignore (Mathml_editor.thaw tex_editor) ;
 192        mmlwidget#thaw
 193
 194       (* The input of set_term is unquoted *)
 195       method set_term txt =
 196        mmlwidget#freeze ;
 197        ignore (Mathml_editor.freeze tex_editor) ;
 198        self#reset ;
 199        let txt' = Str.global_replace (Str.regexp "_") "\\_" txt in
 200         String.iter (fun ch -> Mathml_editor.push tex_editor ch) txt' ;
 201         ignore (Mathml_editor.thaw tex_editor) ;
 202         mmlwidget#thaw
 203
 204       (* get_as_string returns the unquoted string *)
 205       method get_as_string =
 206        let term = Mathml_editor.get_tex tex_editor in
 207         Str.global_replace (Str.regexp "^\\$\\$?") ""
 208          (Str.global_replace (Str.regexp "\\$\\$?$") ""
 209            (Str.global_replace (Str.regexp "\\\\_") "_" term))
 210
 211       method get_metasenv_and_term ~context ~metasenv =
 212        let name_context =
 213         List.map
 214          (function
 215              Some (n,_) -> Some n
 216            | None -> None
 217          ) context
 218        in
 219         debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
 220         let environment',metasenv,expr =
 221          match
 222           Disambiguate'.disambiguate_term mqi_handle
 223            context metasenv (Mathml_editor.get_tex tex_editor) !environment
 224          with
 225             [environment',metasenv,expr] -> environment',metasenv,expr
 226           | _ -> assert false
 227         in
 228          environment := environment' ;
 229          metasenv,expr
 230
 231       method environment = environment
 232    end
 233
 234    let term_editor = new term_editor_impl
 235
 236 end
 237 ;;