From 69789d216abc552d2538089fd62b53af6f75b8b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Mar 2003 18:56:37 +0000 Subject: [PATCH] First committed version that (may) use the MathML editor to enter formulas. --- helm/gTopLevel/.depend | 15 ++- helm/gTopLevel/Makefile | 30 +++-- helm/gTopLevel/disambiguate.ml | 101 ++++++++++----- helm/gTopLevel/disambiguate.mli | 14 ++- helm/gTopLevel/gTopLevel.ml | 63 ++++++---- helm/gTopLevel/termEditor.mli | 2 +- helm/gTopLevel/texTermEditor.ml | 205 +++++++++++++++++++++++++++++++ helm/gTopLevel/texTermEditor.mli | 49 ++++++++ 8 files changed, 401 insertions(+), 78 deletions(-) create mode 100644 helm/gTopLevel/texTermEditor.ml create mode 100644 helm/gTopLevel/texTermEditor.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 7d9361990..de8a83a5c 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -20,6 +20,9 @@ disambiguate.cmx: disambiguate.cmi termEditor.cmo: disambiguate.cmi termEditor.cmi termEditor.cmx: disambiguate.cmx termEditor.cmi termEditor.cmi: disambiguate.cmi +texTermEditor.cmo: disambiguate.cmi misc.cmi texTermEditor.cmi +texTermEditor.cmx: disambiguate.cmx misc.cmx texTermEditor.cmi +texTermEditor.cmi: disambiguate.cmi applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ applyStylesheets.cmi applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ @@ -38,9 +41,9 @@ invokeTactics.cmi: termEditor.cmi termViewer.cmi hbugs.cmo: invokeTactics.cmi misc.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx misc.cmx proofEngine.cmx hbugs.cmi hbugs.cmi: invokeTactics.cmi -gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi disambiguate.cmi \ - hbugs.cmi invokeTactics.cmi logicalOperations.cmi misc.cmi \ - proofEngine.cmi sequentPp.cmi termEditor.cmi termViewer.cmi -gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx disambiguate.cmx \ - hbugs.cmx invokeTactics.cmx logicalOperations.cmx misc.cmx \ - proofEngine.cmx sequentPp.cmx termEditor.cmx termViewer.cmx +gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi hbugs.cmi \ + invokeTactics.cmi logicalOperations.cmi misc.cmi proofEngine.cmi \ + sequentPp.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi +gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx hbugs.cmx \ + invokeTactics.cmx logicalOperations.cmx misc.cmx proofEngine.cmx \ + sequentPp.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 6c27ed3e6..271d204c8 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,9 +1,11 @@ BIN_DIR = /usr/local/bin -REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ - helm-xml gdome2-xslt helm-cic_unification helm-tactics helm-mathql \ - helm-mathql_interpreter helm-mquery_generator threads hbugs-client +REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ + helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ + helm-tactics helm-mathql helm-mathql_interpreter \ + helm-mquery_generator threads hbugs-client PREDICATES = "gnome,init,glade" -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o \ + -I /home/claudio/miohelm/helm/DEVEL/mathml_editor/ocaml OCAMLFIND = ocamlfind OCAMLC = $(OCAMLFIND) ocamlc -thread $(OCAMLOPTIONS) OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(OCAMLOPTIONS) @@ -19,26 +21,28 @@ DEPOBJS = \ xml2Gdome.ml xml2Gdome.mli proofEngine.ml proofEngine.mli \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml cic2acic.mli\ cic2Xml.ml cic2Xml.mli logicalOperations.ml logicalOperations.mli \ - sequentPp.ml sequentPp.mli misc.ml misc.mli \ - disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \ - applyStylesheets.ml applyStylesheets.mli termViewer.ml \ - termViewer.mli invokeTactics.ml invokeTactics.mli \ - hbugs.ml hbugs.mli gTopLevel.ml + sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \ + mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \ + disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \ + texTermEditor.ml texTermEditor.mli applyStylesheets.ml \ + applyStylesheets.mli termViewer.ml termViewer.mli invokeTactics.ml \ + invokeTactics.mli hbugs.ml hbugs.mli gTopLevel.ml TOPLEVELOBJS = \ xml2Gdome.cmo doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - proofEngine.cmo logicalOperations.cmo sequentPp.cmo misc.cmo \ - disambiguate.cmo termEditor.cmo applyStylesheets.cmo termViewer.cmo \ + proofEngine.cmo logicalOperations.cmo sequentPp.cmo \ + mQueryLevels2.cmo misc.cmo disambiguate.cmo \ + termEditor.cmo texTermEditor.cmo applyStylesheets.cmo termViewer.cmo \ invokeTactics.cmo hbugs.cmo gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS) + $(OCAMLC) -linkpkg -o gTopLevel /home/claudio/miohelm/helm/DEVEL/mathml_editor/src/.libs/libeditex.a mlmathml-editor.cma $(TOPLEVELOBJS) gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o gTopLevel.opt /home/claudio/miohelm/helm/DEVEL/mathml_editor/src/.libs/libeditex.a mlmathml-editor.cmxa $(TOPLEVELOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx .ml.cmo: diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index c0e1818e1..afa47790a 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -51,6 +51,12 @@ let get_last_query = module type Callbacks = sig + (* The following two functions are used to save/restore the metasenv *) + (* before/after the parsing. *) + (*CSC: This should be made functional sooner or later! *) + val get_metasenv : unit -> Cic.metasenv + val set_metasenv : Cic.metasenv -> unit + val output_html : string -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `EXTENDED] -> @@ -64,7 +70,8 @@ module type Callbacks = ;; type domain_and_interpretation = - string list * (string -> CicTextualParser0.uri option) + CicTextualParser0.interpretation_domain_item list * + CicTextualParser0.interpretation ;; module Make(C:Callbacks) = @@ -110,6 +117,10 @@ module Make(C:Callbacks) = | Ko | Uncertain + type ambiguous_choices = + Uris of CicTextualParser0.uri list + | Symbols of (CicTextualParser0.interpretation -> Cic.term) list + let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris= let known_ids,resolve_id = id_to_uris in let dom' = @@ -122,13 +133,29 @@ module Make(C:Callbacks) = filter dom in (* for each id in dom' we get the list of uris associated to it *) - let list_of_uris = List.map locate_one_id dom' in + let list_of_uris = + List.map + (function + CicTextualParser0.Id id -> Uris (locate_one_id id) + | CicTextualParser0.Symbol (descr,choices) -> + (* CSC: Implementare la funzione di filtraggio manuale *) + (* CSC: corrispondente alla locate_one_id *) + Symbols (List.map snd choices) + ) dom' in let tests_no = - List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris + List.fold_left + (fun i uris -> + let len = + match uris with + Uris l -> List.length l + | Symbols l -> List.length l + in + i * len + ) 1 list_of_uris in if tests_no > 1 then C.output_html - ("

Disambiguation phase started: " ^ + ("

Disambiguation phase started: up to " ^ string_of_int tests_no ^ " cases will be tried.") ; (* and now we compute the list of all possible assignments from *) (* id to uris that generate well-typed terms *) @@ -137,25 +164,19 @@ module Make(C:Callbacks) = let test resolve_id residual_dom = (* We put implicits in place of every identifier that is not *) (* resolved by resolve_id *) - let resolve_id'' = - let resolve_id' = - function id -> - match resolve_id id with - None -> None - | Some uri -> Some (CicTextualParser0.Uri uri) - in - List.fold_left - (fun f id -> - function id' -> - if id = id' then Some (CicTextualParser0.Implicit) else f id' - ) resolve_id' residual_dom + let resolve_id' = + List.fold_left + (fun f id -> + function id' -> + if id = id' then Some (CicTextualParser0.Implicit) else f id' + ) resolve_id residual_dom in (* and we try to refine the term *) - let saved_status = !CicTextualParser0.metasenv in - let metasenv',expr = mk_metasenv_and_expr resolve_id'' in + let saved_status = C.get_metasenv () in + let metasenv',expr = mk_metasenv_and_expr resolve_id' in (*CSC: Bug here: we do not try to typecheck also the metasenv' *) (* The parser is imperative ==> we must restore the old status ;-(( *) - CicTextualParser0.metasenv := saved_status ; + C.set_metasenv saved_status ; try let term,_,_,metasenv'' = CicRefine.type_of_aux' metasenv' context expr @@ -185,7 +206,7 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; let rec filter = function [] -> [] - | uri::uritl -> + | (uri : CicTextualParser0.interpretation_codomain_item)::uritl -> let resolve_id' = function id' -> if id = id' then Some uri else resolve_id id' in @@ -207,7 +228,14 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; filter uritl ) in - filter uris + (match uris with + Uris uris -> + filter + (List.map (function uri -> CicTextualParser0.Uri uri) uris) + | Symbols symbols -> + filter + (List.map + (function sym -> CicTextualParser0.Term sym) symbols)) | _,_ -> assert false in aux resolve_id dom' list_of_uris @@ -236,20 +264,27 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; (function (resolve,_,_) -> List.map (function id -> - id, + (match id with + CicTextualParser0.Id id -> id + | CicTextualParser0.Symbol (descr,_) -> descr + ), match resolve id with None -> assert false - | Some uri -> - match uri with - CicTextualParser0.ConUri uri - | CicTextualParser0.VarUri uri -> - UriManager.string_of_uri uri - | CicTextualParser0.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (tyno+1) ^ ")" - | CicTextualParser0.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")" + | Some (CicTextualParser0.Uri uri) -> + (match uri with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri -> + UriManager.string_of_uri uri + | CicTextualParser0.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ ")" + | CicTextualParser0.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")") + | Some (CicTextualParser0.Term term) -> + (* CSC: Implementare resa delle scelte *) + "To be implemented XXX01" + | Some CicTextualParser0.Implicit -> assert false ) dom ) resolve_ids in diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli index 2a03f58d9..40ad3ec2e 100644 --- a/helm/gTopLevel/disambiguate.mli +++ b/helm/gTopLevel/disambiguate.mli @@ -38,6 +38,12 @@ module type Callbacks = sig + (* The following two functions are used to save/restore the metasenv *) + (* before/after the parsing. *) + (*CSC: This should be made functional sooner or later! *) + val get_metasenv : unit -> Cic.metasenv + val set_metasenv : Cic.metasenv -> unit + val output_html : string -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `EXTENDED] -> @@ -50,7 +56,8 @@ module type Callbacks = end type domain_and_interpretation = - string list * (string -> CicTextualParser0.uri option) + CicTextualParser0.interpretation_domain_item list * + CicTextualParser0.interpretation module Make (C : Callbacks) : sig @@ -58,9 +65,8 @@ module Make (C : Callbacks) : val disambiguate_input : Cic.context -> Cic.metasenv -> - string list -> - ((string -> CicTextualParser0.interp_codomain option) -> - Cic.metasenv * Cic.term) -> + CicTextualParser0.interpretation_domain_item list -> + (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) -> id_to_uris:domain_and_interpretation -> domain_and_interpretation * Cic.metasenv * Cic.term end diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 82cabae04..3fb42b47d 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -764,10 +764,17 @@ let edit_aliases () = let uri = match resolve_id v with None -> assert false - | Some uri -> uri + | Some (CicTextualParser0.Uri uri) -> uri + | Some (CicTextualParser0.Term _) + | Some CicTextualParser0.Implicit -> assert false in - "alias " ^ v ^ " " ^ - (string_of_cic_textual_parser_uri uri) + "alias " ^ + (match v with + CicTextualParser0.Id id -> id + | CicTextualParser0.Symbol (descr,_) -> + (* CSC: To be implemented *) + assert false + )^ " " ^ (string_of_cic_textual_parser_uri uri) ) dom))) ; window#show () ; GtkThread.main (); @@ -787,7 +794,7 @@ let edit_aliases () = let rec aux n = try let n' = Str.search_forward regexpr inputtext n in - let id = Str.matched_group 2 inputtext in + let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in let uri = MQueryMisc.cic_textual_parser_uri_of_string ("cic:" ^ (Str.matched_group 5 inputtext)) @@ -797,7 +804,10 @@ let edit_aliases () = dom,resolve_id else id::dom, - (function id' -> if id = id' then Some uri else resolve_id id') + (function id' -> + if id = id' then + Some (CicTextualParser0.Uri uri) + else resolve_id id') with Not_found -> TermEditor.empty_id_to_uris in @@ -916,14 +926,17 @@ let let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in - let show_in_show_window_callback mmlwidget (n : Gdome.element) _ = - if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then - let uri = - (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string - in - show_in_show_window_uri (UriManager.uri_of_string uri) - else - ignore (mmlwidget#action_toggle n) + let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = + match n with + None -> () + | Some n' -> + if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then + let uri = + (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + in + show_in_show_window_uri (UriManager.uri_of_string uri) + else + ignore (mmlwidget#action_toggle n') in let _ = mmlwidget#connect#click (show_in_show_window_callback mmlwidget) @@ -1077,8 +1090,18 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) +module ChosenTermEditor = TexTermEditor;; +module ChosenTextualParser0 = TexCicTextualParser0;; +(* +module ChosenTermEditor = TermEditor;; +module ChosenTextualParser0 = CicTextualParser0;; +*) + module Callbacks = struct + let get_metasenv () = !ChosenTextualParser0.metasenv + let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv + let output_html msg = output_html (outputhtml ()) msg;; let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> @@ -1089,9 +1112,7 @@ module Callbacks = end ;; -module Disambiguate' = Disambiguate.Make(Callbacks);; - -module TermEditor' = TermEditor.Make(Callbacks);; +module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; (* OTHER FUNCTIONS *) @@ -1237,7 +1258,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TermEditor'.term_editor + TexTermEditor'.term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: @@ -1348,7 +1369,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TermEditor'.term_editor + TexTermEditor'.term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: @@ -1492,7 +1513,7 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add + TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: (function b -> @@ -2725,7 +2746,7 @@ class rendering_window output (notebook : notebook) = factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show in let insert_query_item = - factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U + factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y ~callback:insertQuery in (* hbugs menu *) let hbugs_menu = factory0#add_submenu "HBugs" in @@ -2763,7 +2784,7 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TermEditor'.term_editor + TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 23f657c64..44c543276 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -35,7 +35,7 @@ class type term_editor = method id_to_uris : Disambiguate.domain_and_interpretation ref end -val empty_id_to_uris : string list * (string -> CicTextualParser0.uri option) +val empty_id_to_uris : Disambiguate.domain_and_interpretation module Make (C : Disambiguate.Callbacks) : sig diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml new file mode 100644 index 000000000..fc4af3cde --- /dev/null +++ b/helm/gTopLevel/texTermEditor.ml @@ -0,0 +1,205 @@ +(* 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 + method get_as_string : string + method get_metasenv_and_term : + context:Cic.context -> + metasenv:Cic.metasenv -> Cic.metasenv * Cic.term + method reset : unit + 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 + ?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 dictionary = + Misc.domImpl#createDocumentFromURI + "/home/claudio/miohelm/helm/DEVEL/mathml_editor/dictionary-tex.xml" () in + let mml_style = + Misc.domImpl#createDocumentFromURI + "/home/claudio/miohelm/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl" () in + let tex_style = + Misc.domImpl#createDocumentFromURI + "/home/claudio/miohelm/helm/DEVEL/mathml_editor/xsl/tml-tex.xsl" () in + let logger = + fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in + let tex_editor = + Mathml_editor.create dictionary mml_style tex_style 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 ; +(*CSC: pre-lexer *) + if key = GdkKeysyms._space && GdkEvent.Key.state e = [] then + begin + ignore (Mathml_editor.freeze tex_editor) ; + Mathml_editor.push tex_editor '\\' ; + Mathml_editor.push tex_editor ';' ; + ignore (Mathml_editor.thaw tex_editor) + end +(*CSC: end of pre-lexer *) + else 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 ; + Mathml_editor.reset tex_editor ; + Mathml_editor.push tex_editor '$' ; + mmlwidget#thaw + end + else if key = GdkKeysyms._BackSpace then + Mathml_editor.drop tex_editor false ; + mmlwidget#thaw ; + 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 ; + Mathml_editor.reset tex_editor ; + Mathml_editor.push tex_editor '$' ; + mmlwidget#thaw + + method set_term txt = + mmlwidget#freeze ; + ignore (Mathml_editor.freeze tex_editor) ; + self#reset ; + (* we need to remove the initial and final '$' *) + let txt' = String.sub txt 1 (String.length txt - 2) in + String.iter (fun ch -> Mathml_editor.push tex_editor ch) txt' ; + ignore (Mathml_editor.thaw tex_editor) ; + mmlwidget#thaw + + method get_as_string = + Mathml_editor.get_tex tex_editor + + method get_metasenv_and_term ~context ~metasenv = + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string self#get_as_string 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 + 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 +;; diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli new file mode 100644 index 000000000..44c543276 --- /dev/null +++ b/helm/gTopLevel/texTermEditor.mli @@ -0,0 +1,49 @@ +(* 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/. + *) + +class type term_editor = + object + method coerce : GObj.widget + method get_as_string : string + method get_metasenv_and_term : + context:Cic.context -> + metasenv:Cic.metasenv -> Cic.metasenv * Cic.term + method reset : unit + method set_term : string -> unit + method id_to_uris : Disambiguate.domain_and_interpretation ref + end + +val empty_id_to_uris : Disambiguate.domain_and_interpretation + +module Make (C : Disambiguate.Callbacks) : + sig + val term_editor : + ?packing:(GObj.widget -> unit) -> + ?width:int -> + ?height:int -> + ?isnotempty_callback:(bool -> unit) -> + ?share_id_to_uris_with:term_editor -> + unit -> term_editor + end -- 2.39.2