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 ?packing ?width ?height ?isnotempty_callback
+ class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback
?share_id_to_uris_with () : term_editor
=
let id_to_uris =
self#reset ;
ignore ((input#insert_text txt) ~pos:0)
(* CSC: this method should disappear *)
+ (* get_as_string returns the unquoted string *)
method get_as_string =
input#get_chars 0 input#length
method get_metasenv_and_term ~context ~metasenv =
~context:name_context ~metasenv CicTextualLexer.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' ;