X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;fp=helm%2FgTopLevel%2FtexTermEditor.ml;h=0000000000000000000000000000000000000000;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hp=3cf09934972746fd9de3692b2b188449a71f0f26;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml deleted file mode 100644 index 3cf099349..000000000 --- a/helm/gTopLevel/texTermEditor.ml +++ /dev/null @@ -1,211 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) - -(* A WIDGET TO ENTER CIC TERMS *) - -class type term_editor = - object - method coerce : GObj.widget - (* get_as_string returns the unquoted string *) - method get_as_string : string - method get_metasenv_and_term : - context:Cic.context -> - metasenv:Cic.metasenv -> Cic.metasenv * Cic.term - method reset : unit - (* The input of set_term is unquoted *) - method set_term : string -> unit - method id_to_uris : Disambiguate.domain_and_interpretation ref - end -;; - -let empty_id_to_uris = ([],function _ -> None);; - -module Make(C:Disambiguate.Callbacks) = - struct - - module Disambiguate' = Disambiguate.Make(C);; - - class term_editor_impl - mqi_handle - ?packing ?width ?height - ?isnotempty_callback ?share_id_to_uris_with () : term_editor - = - let mmlwidget = - GMathViewAux.single_selection_math_view - ?packing ?width ?height () in - let drawing_area = mmlwidget#get_drawing_area in - let _ = drawing_area#misc#set_can_focus true in - let _ = drawing_area#misc#grab_focus () in - let logger = - fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in - let tex_editor = - Mathml_editor.create - ~alt_lexer:true - ~dictionary_uri:"dictionary-cic.xml" - ~mml_uri:Mathml_editor.default_mathml_stylesheet_path -(*CSC: togliere il path assoluto - ~tml_uri:Mathml_editor.default_tex_stylesheet_path -*) - ~tml_uri:"/usr/share/editex/tml-litex.xsl" - ~log:logger - in - let _ = - (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press - ~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in - let _ = - (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in - ~callback: - (fun _ -> - mmlwidget#freeze ; - Mathml_editor.cursor_show ~editor:tex_editor ; - mmlwidget#thaw ; - true) in - let _ = - (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out - ~callback: - (fun _ -> - mmlwidget#freeze ; - Mathml_editor.cursor_hide ~editor:tex_editor ; - mmlwidget#thaw ; - true) in - let _ = Mathml_editor.push tex_editor '$' in - let dom_tree = Mathml_editor.get_mml tex_editor in - let _ = mmlwidget#load_doc dom_tree in - let _ = - drawing_area#event#connect#key_press - (function e -> - let key = GdkEvent.Key.keyval e in - mmlwidget#freeze ; - if - key >= 32 && key < 256 && - (GdkEvent.Key.state e = [] || GdkEvent.Key.state e = [`SHIFT]) - then - Mathml_editor.push tex_editor (Char.chr key) - else if key = GdkKeysyms._u then - begin - mmlwidget#freeze ; - ignore (Mathml_editor.freeze tex_editor) ; - Mathml_editor.reset tex_editor ; - Mathml_editor.push tex_editor '$' ; - ignore (Mathml_editor.thaw tex_editor) ; - mmlwidget#thaw - end - else if key = GdkKeysyms._BackSpace then - Mathml_editor.drop tex_editor - (List.mem `CONTROL (GdkEvent.Key.state e)) ; - let adj = mmlwidget#get_hadjustment in - mmlwidget#thaw ; - adj#set_value adj#upper ; - false) in - let id_to_uris = - match share_id_to_uris_with with - None -> ref empty_id_to_uris - | Some obj -> obj#id_to_uris - in - let _ = - match isnotempty_callback with - None -> () - | Some callback -> - (* This approximation of the test that checks if the tree is empty *) - (* is utterly unprecise. We assume a tree to look as an empty tree *) - (* iff it is made of just one node m:mtext (which should be the *) - (* cursor). *) - let is_empty_tree () = - let root = dom_tree#get_documentElement in - match root#get_firstChild with - None -> true - | Some n -> n#get_nodeName#to_string = "m:mtext" - in - dom_tree#addEventListener - ~typ:(Gdome.domString "DOMSubtreeModified") - ~listener: - (Gdome.eventListener - (function _ -> callback (not (is_empty_tree ())))) - ~useCapture:false - in - object(self) - method coerce = mmlwidget#coerce - method reset = - mmlwidget#freeze ; - ignore (Mathml_editor.freeze tex_editor) ; - Mathml_editor.reset tex_editor ; - Mathml_editor.push tex_editor '$' ; - ignore (Mathml_editor.thaw tex_editor) ; - mmlwidget#thaw - - (* The input of set_term is unquoted *) - method set_term txt = - mmlwidget#freeze ; - ignore (Mathml_editor.freeze tex_editor) ; - self#reset ; - let txt' = Str.global_replace (Str.regexp "_") "\\_" txt in - String.iter (fun ch -> Mathml_editor.push tex_editor ch) txt' ; - ignore (Mathml_editor.thaw tex_editor) ; - mmlwidget#thaw - - (* get_as_string returns the unquoted string *) - method get_as_string = - let term = Mathml_editor.get_tex tex_editor in - Str.global_replace (Str.regexp "^\\$\\$?") "" - (Str.global_replace (Str.regexp "\\$\\$?$") "" - (Str.global_replace (Str.regexp "\\\\_") "_" term)) - - method get_metasenv_and_term ~context ~metasenv = - let name_context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context - in -prerr_endline ("###CSC: " ^ (Mathml_editor.get_tex tex_editor)) ; - let lexbuf = Lexing.from_string (Mathml_editor.get_tex tex_editor) in - let dom,mk_metasenv_and_expr = - TexCicTextualParserContext.main - ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf - in - let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris - in - id_to_uris := id_to_uris' ; - metasenv,expr - method id_to_uris = id_to_uris - end - - let term_editor = new term_editor_impl - -end -;;