From: Luca Padovani Date: Wed, 29 Oct 2003 09:18:47 +0000 (+0000) Subject: * GEdit -> GText X-Git-Tag: V_0_2_2~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77ac22e3c4577116027e142607713585329c6771;p=helm.git * GEdit -> GText --- diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 310efd176..d4f040a9a 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -65,26 +65,26 @@ module Make(C:Disambiguate.Callbacks) = None -> ref empty_id_to_uris | Some obj -> obj#id_to_uris in - let input = GEdit.text ~editable:true ?width ?height ?packing () in + let input = GText.view ~editable:true ?width ?height ?packing () in let _ = match isnotempty_callback with None -> () | Some callback -> - ignore(input#connect#changed - (function () -> callback (input#length > 0))) + ignore(input#buffer#connect#changed + (function () -> callback (input#buffer#char_count > 0))) in object(self) method coerce = input#coerce method reset = - input#delete_text 0 input#length + input#buffer#delete input#buffer#start_iter input#buffer#end_iter (* CSC: txt is now a string, but should be of type Cic.term *) method set_term txt = self#reset ; - ignore ((input#insert_text txt) ~pos:0) + ignore (input#buffer#insert txt) (* CSC: this method should disappear *) (* get_as_string returns the unquoted string *) method get_as_string = - input#get_chars 0 input#length + input#buffer#get_text () method get_metasenv_and_term ~context ~metasenv = let name_context = List.map @@ -93,7 +93,7 @@ module Make(C:Disambiguate.Callbacks) = | None -> None ) context in - let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in + let lexbuf = Lexing.from_string (input#buffer#get_text ()) in let dom,mk_metasenv_and_expr = CicTextualParserContext.main ~context:name_context ~metasenv CicTextualLexer.token lexbuf