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