helm/gTopLevel/chosenTermEditor.mli

   1 class type term_editor =
   2   object
   3     method coerce : GObj.widget
   4     method get_as_string : string
   5     method get_metasenv_and_term :
   6       context:Cic.context ->
   7       metasenv:Cic.metasenv -> Cic.metasenv * Cic.term * CicUniv.universe_graph
   8     method environment : DisambiguatingParser.EnvironmentP3.t ref
   9     method reset : unit
  10     method set_term : string -> unit
  11   end
  12
  13 module Make :
  14   functor (C : DisambiguateTypes.Callbacks) ->
  15     sig
  16       val term_editor :
  17         dbd:Mysql.dbd ->
  18         ?packing:(GObj.widget -> unit) ->
  19         ?width:int ->
  20         ?height:int ->
  21         ?isnotempty_callback:(bool -> unit) ->
  22         ?share_environment_with:term_editor -> unit -> term_editor
  23     end