]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/texTermEditor.ml
removed uri parameter from load_proof
[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 -> 
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 ;;