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
module Disambiguate' = Disambiguate.Make(C);;
class term_editor_impl
+ mqi_handle
?packing ?width ?height
?isnotempty_callback ?share_id_to_uris_with () : term_editor
=
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
+ Mathml_editor.create
+ Mathml_editor.default_dictionary_path
+ Mathml_editor.default_mathml_stylesheet_path
+ Mathml_editor.default_tex_stylesheet_path
+ logger
+ in
let _ =
(new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press
~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in
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
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 ;
- (* we need to remove the initial and final '$' *)
- let txt' = String.sub txt 1 (String.length txt - 2) in
+ 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 =
- Mathml_editor.get_tex tex_editor
+ 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 =
| None -> None
) context
in
- let lexbuf = Lexing.from_string self#get_as_string in
+ 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
+ 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' ;