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