* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 06/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(*****************************************************************************)
open Printf
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 mqi_handle ?packing ?width ?height
+ class term_editor_impl ~(dbd:Mysql.dbd) ?packing ?width ?height
?isnotempty_callback ?share_environment_with () : term_editor
=
let environment =
match share_environment_with with
- None -> ref
+ None -> ref (*DisambiguateTypes.empty_environment*)
(DisambiguatingParser.EnvironmentP3.of_string
DisambiguatingParser.EnvironmentP3.empty)
| Some obj -> obj#environment
| None -> None
) context
in
- let environment',metasenv,expr =
- Disambiguate'.disambiguate_term mqi_handle context metasenv
- (input#buffer#get_text ()) !environment
+ let environment',metasenv,expr,ugraph =
+ match
+ Disambiguate'.disambiguate_term ~dbd context metasenv
+ (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph
+ !environment
+ with
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
+ | _ -> assert false
in
environment := environment';
- (metasenv, expr)
+ (metasenv, expr,ugraph)
+ (* TASSI: FIXME ?are we sure we have to keep this? *)
method environment = environment
end