+++ /dev/null
-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 environment : DisambiguatingParser.EnvironmentP3.t ref
- method reset : unit
- method set_term : string -> unit
- end
-
-module Make :
- functor (C : DisambiguateTypes.Callbacks) ->
- sig
- val term_editor :
- MQIConn.handle ->
- ?packing:(GObj.widget -> unit) ->
- ?width:int ->
- ?height:int ->
- ?isnotempty_callback:(bool -> unit) ->
- ?share_environment_with:term_editor -> unit -> term_editor
- end