]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/texTermEditor.ml
- bugfix: sequences like ".(" are now lexed, correctly, as
[helm.git] / 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 ;;