* http://cs.unibo.it/helm/.
*)
+let debug = true
+let debug_print s = if debug then prerr_endline s
+
(******************************************************************************)
(* *)
(* PROJECT HELM *)
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
- method id_to_uris : Disambiguate.domain_and_interpretation ref
+ method environment : DisambiguatingParser.EnvironmentP3.t ref
end
;;
-let empty_id_to_uris = ([],function _ -> None);;
-
-module Make(C:Disambiguate.Callbacks) =
+module Make(C:DisambiguateTypes.Callbacks) =
struct
- module Disambiguate' = Disambiguate.Make(C);;
+ module Disambiguate' = DisambiguatingParser.Make(C);;
class term_editor_impl
- mqi_handle
+ ~dbd
?packing ?width ?height
- ?isnotempty_callback ?share_id_to_uris_with () : term_editor
+ ?isnotempty_callback ?share_environment_with () : term_editor
=
let mmlwidget =
GMathViewAux.single_selection_math_view
?packing ?width ?height () in
+(*
let drawing_area = mmlwidget#get_drawing_area in
let _ = drawing_area#misc#set_can_focus true in
let _ = drawing_area#misc#grab_focus () in
+*)
let logger =
fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in
let tex_editor =
~tml_uri:"/usr/share/editex/tml-litex.xsl"
~log:logger
in
+(*
let _ =
(new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press
~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in
+*)
let _ =
- (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in
+(* (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in *)
+ (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_in
~callback:
(fun _ ->
mmlwidget#freeze ;
mmlwidget#thaw ;
true) in
let _ =
- (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out
+(* (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out *)
+ (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_out
~callback:
(fun _ ->
mmlwidget#freeze ;
true) in
let _ = Mathml_editor.push tex_editor '$' in
let dom_tree = Mathml_editor.get_mml tex_editor in
- let _ = mmlwidget#load_doc dom_tree in
+ let _ = mmlwidget#load_root dom_tree#get_documentElement in
let _ =
- drawing_area#event#connect#key_press
+(* drawing_area#event#connect#key_press *)
+ (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#key_press
(function e ->
let key = GdkEvent.Key.keyval e in
mmlwidget#freeze ;
mmlwidget#thaw
end
else if key = GdkKeysyms._BackSpace then
- Mathml_editor.drop tex_editor false ;
- let adj = mmlwidget#get_hadjustment in
+ Mathml_editor.drop tex_editor
+ (List.mem `CONTROL (GdkEvent.Key.state e))
+ else if key = GdkKeysyms._v then
+ ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
+ let hadj, _ = mmlwidget#get_adjustments in
mmlwidget#thaw ;
- adj#set_value adj#upper ;
+ hadj#set_value hadj#upper ;
false) in
- let id_to_uris =
- match share_id_to_uris_with with
- None -> ref empty_id_to_uris
- | Some obj -> obj#id_to_uris
+ let environment =
+ match share_environment_with with
+ None ->
+ ref
+ (DisambiguatingParser.EnvironmentP3.of_string
+ DisambiguatingParser.EnvironmentP3.empty)
+ | Some obj -> obj#environment
in
let _ =
match isnotempty_callback with
~useCapture:false
in
object(self)
+
+ initializer
+ ignore (mmlwidget#misc#connect#selection_received
+ ~callback: (fun selection_data ~time ->
+ let input = try selection_data#data with Gpointer.Null -> "" in
+ mmlwidget#freeze ;
+ ignore (Mathml_editor.freeze tex_editor) ;
+ for i = 0 to String.length input - 1 do
+ Mathml_editor.push tex_editor input.[i]
+ done;
+ ignore (Mathml_editor.thaw tex_editor) ;
+ mmlwidget#thaw))
+
method coerce = mmlwidget#coerce
method reset =
mmlwidget#freeze ;
| None -> None
) context
in
-prerr_endline ("###CSC: " ^ (Mathml_editor.get_tex tex_editor)) ;
- let lexbuf = Lexing.from_string (Mathml_editor.get_tex tex_editor) in
- let dom,mk_metasenv_and_expr =
- TexCicTextualParserContext.main
- ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf
- in
- let id_to_uris',metasenv,expr =
- Disambiguate'.disambiguate_input mqi_handle
- context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris
- in
- id_to_uris := id_to_uris' ;
- metasenv,expr
- method id_to_uris = id_to_uris
+ debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
+ let environment',metasenv,expr,ugraph =
+ match
+ Disambiguate'.disambiguate_term ~dbd
+ ~context ~metasenv (Mathml_editor.get_tex tex_editor)
+ ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment
+ with
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
+ | _ -> assert false
+ in
+ environment := environment' ;
+ metasenv,expr,ugraph
+
+ method environment = environment
end
let term_editor = new term_editor_impl
projects / helm.git / blobdiff