method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv ->
+ Cic.metasenv * Cic.term * CicUniv.universe_graph
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
module Disambiguate' = DisambiguatingParser.Make(C);;
class term_editor_impl
- ~dbh
+ ~dbd
?packing ?width ?height
?isnotempty_callback ?share_environment_with () : term_editor
=
) context
in
debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
- let environment',metasenv,expr =
+ let environment',metasenv,expr,ugraph =
match
- Disambiguate'.disambiguate_term ~dbh
- context metasenv (Mathml_editor.get_tex tex_editor) !environment
+ Disambiguate'.disambiguate_term ~dbd
+ ~context ~metasenv (Mathml_editor.get_tex tex_editor)
+ ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment
with
- [environment',metasenv,expr] -> environment',metasenv,expr
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
| _ -> assert false
in
environment := environment' ;
- metasenv,expr
+ metasenv,expr,ugraph
method environment = environment
end