From 4566aebfc281e0ad37da2f0f60155d5d9185a7f2 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:53:07 +0000 Subject: [PATCH] ported to Dbi-disambiguation --- helm/gTopLevel/termEditor.ml | 4 ++-- helm/gTopLevel/termEditor.mli | 2 +- helm/gTopLevel/texTermEditor.ml | 4 ++-- helm/gTopLevel/texTermEditor.mli | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 3a74ef051..e7b50c266 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -56,7 +56,7 @@ module Make(C:DisambiguateTypes.Callbacks) = module Disambiguate' = DisambiguatingParser.Make(C);; - class term_editor_impl mqi_handle ?packing ?width ?height + class term_editor_impl ~(dbh:Dbi.connection) ?packing ?width ?height ?isnotempty_callback ?share_environment_with () : term_editor = let environment = @@ -100,7 +100,7 @@ module Make(C:DisambiguateTypes.Callbacks) = in let environment',metasenv,expr = match - Disambiguate'.disambiguate_term mqi_handle context metasenv + Disambiguate'.disambiguate_term ~dbh context metasenv (input#buffer#get_text ()) !environment with [environment',metasenv,expr] -> environment',metasenv,expr diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index b3fb94937..ecb40decd 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -39,7 +39,7 @@ class type term_editor = module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : - MQIConn.handle -> + dbh:Dbi.connection -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index 1ea429926..825b79e12 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -59,7 +59,7 @@ module Make(C:DisambiguateTypes.Callbacks) = module Disambiguate' = DisambiguatingParser.Make(C);; class term_editor_impl - mqi_handle + ~dbh ?packing ?width ?height ?isnotempty_callback ?share_environment_with () : term_editor = @@ -219,7 +219,7 @@ module Make(C:DisambiguateTypes.Callbacks) = debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ; let environment',metasenv,expr = match - Disambiguate'.disambiguate_term mqi_handle + Disambiguate'.disambiguate_term ~dbh context metasenv (Mathml_editor.get_tex tex_editor) !environment with [environment',metasenv,expr] -> environment',metasenv,expr diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index 8b040c983..c7709b532 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -40,7 +40,7 @@ class type term_editor = module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : - MQIConn.handle -> + dbh:Dbi.connection -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> -- 2.39.2