termEditor.cmo: disambiguate.cmi termEditor.cmi
termEditor.cmx: disambiguate.cmx termEditor.cmi
termEditor.cmi: disambiguate.cmi
+texTermEditor.cmo: disambiguate.cmi misc.cmi texTermEditor.cmi
+texTermEditor.cmx: disambiguate.cmx misc.cmx texTermEditor.cmi
+texTermEditor.cmi: disambiguate.cmi
applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \
applyStylesheets.cmi
applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \
hbugs.cmo: invokeTactics.cmi misc.cmi proofEngine.cmi hbugs.cmi
hbugs.cmx: invokeTactics.cmx misc.cmx proofEngine.cmx hbugs.cmi
hbugs.cmi: invokeTactics.cmi
-gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi disambiguate.cmi \
- hbugs.cmi invokeTactics.cmi logicalOperations.cmi misc.cmi \
- proofEngine.cmi sequentPp.cmi termEditor.cmi termViewer.cmi
-gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx disambiguate.cmx \
- hbugs.cmx invokeTactics.cmx logicalOperations.cmx misc.cmx \
- proofEngine.cmx sequentPp.cmx termEditor.cmx termViewer.cmx
+gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi hbugs.cmi \
+ invokeTactics.cmi logicalOperations.cmi misc.cmi proofEngine.cmi \
+ sequentPp.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi
+gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx hbugs.cmx \
+ invokeTactics.cmx logicalOperations.cmx misc.cmx proofEngine.cmx \
+ sequentPp.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx
BIN_DIR = /usr/local/bin
-REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
- helm-xml gdome2-xslt helm-cic_unification helm-tactics helm-mathql \
- helm-mathql_interpreter helm-mquery_generator threads hbugs-client
+REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
+ helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \
+ helm-tactics helm-mathql helm-mathql_interpreter \
+ helm-mquery_generator threads hbugs-client
PREDICATES = "gnome,init,glade"
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o \
+ -I /home/claudio/miohelm/helm/DEVEL/mathml_editor/ocaml
OCAMLFIND = ocamlfind
OCAMLC = $(OCAMLFIND) ocamlc -thread $(OCAMLOPTIONS)
OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(OCAMLOPTIONS)
xml2Gdome.ml xml2Gdome.mli proofEngine.ml proofEngine.mli \
doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml cic2acic.mli\
cic2Xml.ml cic2Xml.mli logicalOperations.ml logicalOperations.mli \
- sequentPp.ml sequentPp.mli misc.ml misc.mli \
- disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
- applyStylesheets.ml applyStylesheets.mli termViewer.ml \
- termViewer.mli invokeTactics.ml invokeTactics.mli \
- hbugs.ml hbugs.mli gTopLevel.ml
+ sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \
+ mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \
+ disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
+ texTermEditor.ml texTermEditor.mli applyStylesheets.ml \
+ applyStylesheets.mli termViewer.ml termViewer.mli invokeTactics.ml \
+ invokeTactics.mli hbugs.ml hbugs.mli gTopLevel.ml
TOPLEVELOBJS = \
xml2Gdome.cmo doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
- proofEngine.cmo logicalOperations.cmo sequentPp.cmo misc.cmo \
- disambiguate.cmo termEditor.cmo applyStylesheets.cmo termViewer.cmo \
+ proofEngine.cmo logicalOperations.cmo sequentPp.cmo \
+ mQueryLevels2.cmo misc.cmo disambiguate.cmo \
+ termEditor.cmo texTermEditor.cmo applyStylesheets.cmo termViewer.cmo \
invokeTactics.cmo hbugs.cmo gTopLevel.cmo
depend:
$(OCAMLDEP) $(DEPOBJS) > .depend
gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES)
- $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS)
+ $(OCAMLC) -linkpkg -o gTopLevel /home/claudio/miohelm/helm/DEVEL/mathml_editor/src/.libs/libeditex.a mlmathml-editor.cma $(TOPLEVELOBJS)
gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
- $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx)
+ $(OCAMLOPT) -linkpkg -o gTopLevel.opt /home/claudio/miohelm/helm/DEVEL/mathml_editor/src/.libs/libeditex.a mlmathml-editor.cmxa $(TOPLEVELOBJS:.cmo=.cmx)
.SUFFIXES: .ml .mli .cmo .cmi .cmx
.ml.cmo:
module type Callbacks =
sig
+ (* The following two functions are used to save/restore the metasenv *)
+ (* before/after the parsing. *)
+ (*CSC: This should be made functional sooner or later! *)
+ val get_metasenv : unit -> Cic.metasenv
+ val set_metasenv : Cic.metasenv -> unit
+
val output_html : string -> unit
val interactive_user_uri_choice :
selection_mode:[`SINGLE | `EXTENDED] ->
;;
type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+ CicTextualParser0.interpretation
;;
module Make(C:Callbacks) =
| Ko
| Uncertain
+ type ambiguous_choices =
+ Uris of CicTextualParser0.uri list
+ | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
+
let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
let known_ids,resolve_id = id_to_uris in
let dom' =
filter dom
in
(* for each id in dom' we get the list of uris associated to it *)
- let list_of_uris = List.map locate_one_id dom' in
+ let list_of_uris =
+ List.map
+ (function
+ CicTextualParser0.Id id -> Uris (locate_one_id id)
+ | CicTextualParser0.Symbol (descr,choices) ->
+ (* CSC: Implementare la funzione di filtraggio manuale *)
+ (* CSC: corrispondente alla locate_one_id *)
+ Symbols (List.map snd choices)
+ ) dom' in
let tests_no =
- List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+ List.fold_left
+ (fun i uris ->
+ let len =
+ match uris with
+ Uris l -> List.length l
+ | Symbols l -> List.length l
+ in
+ i * len
+ ) 1 list_of_uris
in
if tests_no > 1 then
C.output_html
- ("<h1>Disambiguation phase started: " ^
+ ("<h1>Disambiguation phase started: up to " ^
string_of_int tests_no ^ " cases will be tried.") ;
(* and now we compute the list of all possible assignments from *)
(* id to uris that generate well-typed terms *)
let test resolve_id residual_dom =
(* We put implicits in place of every identifier that is not *)
(* resolved by resolve_id *)
- let resolve_id'' =
- let resolve_id' =
- function id ->
- match resolve_id id with
- None -> None
- | Some uri -> Some (CicTextualParser0.Uri uri)
- in
- List.fold_left
- (fun f id ->
- function id' ->
- if id = id' then Some (CicTextualParser0.Implicit) else f id'
- ) resolve_id' residual_dom
+ let resolve_id' =
+ List.fold_left
+ (fun f id ->
+ function id' ->
+ if id = id' then Some (CicTextualParser0.Implicit) else f id'
+ ) resolve_id residual_dom
in
(* and we try to refine the term *)
- let saved_status = !CicTextualParser0.metasenv in
- let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
+ let saved_status = C.get_metasenv () in
+ let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
(* The parser is imperative ==> we must restore the old status ;-(( *)
- CicTextualParser0.metasenv := saved_status ;
+ C.set_metasenv saved_status ;
try
let term,_,_,metasenv'' =
CicRefine.type_of_aux' metasenv' context expr
let rec filter =
function
[] -> []
- | uri::uritl ->
+ | (uri : CicTextualParser0.interpretation_codomain_item)::uritl ->
let resolve_id' =
function id' -> if id = id' then Some uri else resolve_id id'
in
filter uritl
)
in
- filter uris
+ (match uris with
+ Uris uris ->
+ filter
+ (List.map (function uri -> CicTextualParser0.Uri uri) uris)
+ | Symbols symbols ->
+ filter
+ (List.map
+ (function sym -> CicTextualParser0.Term sym) symbols))
| _,_ -> assert false
in
aux resolve_id dom' list_of_uris
(function (resolve,_,_) ->
List.map
(function id ->
- id,
+ (match id with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) -> descr
+ ),
match resolve id with
None -> assert false
- | Some uri ->
- match uri with
- CicTextualParser0.ConUri uri
- | CicTextualParser0.VarUri uri ->
- UriManager.string_of_uri uri
- | CicTextualParser0.IndTyUri (uri,tyno) ->
- UriManager.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (tyno+1) ^ ")"
- | CicTextualParser0.IndConUri (uri,tyno,consno) ->
- UriManager.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
+ | Some (CicTextualParser0.Uri uri) ->
+ (match uri with
+ CicTextualParser0.ConUri uri
+ | CicTextualParser0.VarUri uri ->
+ UriManager.string_of_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ ")"
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")")
+ | Some (CicTextualParser0.Term term) ->
+ (* CSC: Implementare resa delle scelte *)
+ "To be implemented XXX01"
+ | Some CicTextualParser0.Implicit -> assert false
) dom
) resolve_ids
in
module type Callbacks =
sig
+ (* The following two functions are used to save/restore the metasenv *)
+ (* before/after the parsing. *)
+ (*CSC: This should be made functional sooner or later! *)
+ val get_metasenv : unit -> Cic.metasenv
+ val set_metasenv : Cic.metasenv -> unit
+
val output_html : string -> unit
val interactive_user_uri_choice :
selection_mode:[`SINGLE | `EXTENDED] ->
end
type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+ CicTextualParser0.interpretation
module Make (C : Callbacks) :
sig
val disambiguate_input :
Cic.context ->
Cic.metasenv ->
- string list ->
- ((string -> CicTextualParser0.interp_codomain option) ->
- Cic.metasenv * Cic.term) ->
+ CicTextualParser0.interpretation_domain_item list ->
+ (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) ->
id_to_uris:domain_and_interpretation ->
domain_and_interpretation * Cic.metasenv * Cic.term
end
let uri =
match resolve_id v with
None -> assert false
- | Some uri -> uri
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
in
- "alias " ^ v ^ " " ^
- (string_of_cic_textual_parser_uri uri)
+ "alias " ^
+ (match v with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) ->
+ (* CSC: To be implemented *)
+ assert false
+ )^ " " ^ (string_of_cic_textual_parser_uri uri)
) dom))) ;
window#show () ;
GtkThread.main ();
let rec aux n =
try
let n' = Str.search_forward regexpr inputtext n in
- let id = Str.matched_group 2 inputtext in
+ let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
let uri =
MQueryMisc.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
dom,resolve_id
else
id::dom,
- (function id' -> if id = id' then Some uri else resolve_id id')
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
with
Not_found -> TermEditor.empty_id_to_uris
in
let obj = CicEnvironment.get_obj uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
- if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
- let uri =
- (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
- in
- show_in_show_window_uri (UriManager.uri_of_string uri)
- else
- ignore (mmlwidget#action_toggle n)
+ let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+ match n with
+ None -> ()
+ | Some n' ->
+ if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+ let uri =
+ (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+ in
+ show_in_show_window_uri (UriManager.uri_of_string uri)
+ else
+ ignore (mmlwidget#action_toggle n')
in
let _ =
mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
(* A WIDGET TO ENTER CIC TERMS *)
+module ChosenTermEditor = TexTermEditor;;
+module ChosenTextualParser0 = TexCicTextualParser0;;
+(*
+module ChosenTermEditor = TermEditor;;
+module ChosenTextualParser0 = CicTextualParser0;;
+*)
+
module Callbacks =
struct
+ let get_metasenv () = !ChosenTextualParser0.metasenv
+ let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
+
let output_html msg = output_html (outputhtml ()) msg;;
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
end
;;
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-module TermEditor' = TermEditor.Make(Callbacks);;
+module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
in
let insert_query_item =
- factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+ factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y
~callback:insertQuery in
(* hbugs menu *)
let hbugs_menu = factory0#add_submenu "HBugs" in
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
method id_to_uris : Disambiguate.domain_and_interpretation ref
end
-val empty_id_to_uris : string list * (string -> CicTextualParser0.uri option)
+val empty_id_to_uris : Disambiguate.domain_and_interpretation
module Make (C : Disambiguate.Callbacks) :
sig
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(* A WIDGET TO ENTER CIC TERMS *)
+
+class type term_editor =
+ object
+ method coerce : GObj.widget
+ method get_as_string : string
+ method get_metasenv_and_term :
+ context:Cic.context ->
+ metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ method reset : unit
+ method set_term : string -> unit
+ method id_to_uris : Disambiguate.domain_and_interpretation ref
+ end
+;;
+
+let empty_id_to_uris = ([],function _ -> None);;
+
+module Make(C:Disambiguate.Callbacks) =
+ struct
+
+ module Disambiguate' = Disambiguate.Make(C);;
+
+ class term_editor_impl
+ ?packing ?width ?height
+ ?isnotempty_callback ?share_id_to_uris_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 dictionary =
+ Misc.domImpl#createDocumentFromURI
+ "/home/claudio/miohelm/helm/DEVEL/mathml_editor/dictionary-tex.xml" () in
+ let mml_style =
+ Misc.domImpl#createDocumentFromURI
+ "/home/claudio/miohelm/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl" () in
+ let tex_style =
+ Misc.domImpl#createDocumentFromURI
+ "/home/claudio/miohelm/helm/DEVEL/mathml_editor/xsl/tml-tex.xsl" () in
+ let logger =
+ fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in
+ let tex_editor =
+ Mathml_editor.create dictionary mml_style tex_style 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
+ ~callback:
+ (fun _ ->
+ mmlwidget#freeze ;
+ Mathml_editor.cursor_show ~editor:tex_editor ;
+ mmlwidget#thaw ;
+ true) in
+ let _ =
+ (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out
+ ~callback:
+ (fun _ ->
+ mmlwidget#freeze ;
+ Mathml_editor.cursor_hide ~editor:tex_editor ;
+ mmlwidget#thaw ;
+ 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 _ =
+ drawing_area#event#connect#key_press
+ (function e ->
+ let key = GdkEvent.Key.keyval e in
+ mmlwidget#freeze ;
+(*CSC: pre-lexer *)
+ if key = GdkKeysyms._space && GdkEvent.Key.state e = [] then
+ begin
+ ignore (Mathml_editor.freeze tex_editor) ;
+ Mathml_editor.push tex_editor '\\' ;
+ Mathml_editor.push tex_editor ';' ;
+ ignore (Mathml_editor.thaw tex_editor)
+ end
+(*CSC: end of pre-lexer *)
+ else if
+ key >= 32 && key < 256 &&
+ (GdkEvent.Key.state e = [] || GdkEvent.Key.state e = [`SHIFT])
+ then
+ Mathml_editor.push tex_editor (Char.chr key)
+ else if key = GdkKeysyms._u then
+ begin
+ mmlwidget#freeze ;
+ Mathml_editor.reset tex_editor ;
+ Mathml_editor.push tex_editor '$' ;
+ mmlwidget#thaw
+ end
+ else if key = GdkKeysyms._BackSpace then
+ Mathml_editor.drop tex_editor false ;
+ mmlwidget#thaw ;
+ 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
+ in
+ let _ =
+ match isnotempty_callback with
+ None -> ()
+ | Some callback ->
+ (* This approximation of the test that checks if the tree is empty *)
+ (* is utterly unprecise. We assume a tree to look as an empty tree *)
+ (* iff it is made of just one node m:mtext (which should be the *)
+ (* cursor). *)
+ let is_empty_tree () =
+ let root = dom_tree#get_documentElement in
+ match root#get_firstChild with
+ None -> true
+ | Some n -> n#get_nodeName#to_string = "m:mtext"
+ in
+ dom_tree#addEventListener
+ ~typ:(Gdome.domString "DOMSubtreeModified")
+ ~listener:
+ (Gdome.eventListener
+ (function _ -> callback (not (is_empty_tree ()))))
+ ~useCapture:false
+ in
+ object(self)
+ method coerce = mmlwidget#coerce
+ method reset =
+ mmlwidget#freeze ;
+ Mathml_editor.reset tex_editor ;
+ Mathml_editor.push tex_editor '$' ;
+ mmlwidget#thaw
+
+ method set_term txt =
+ mmlwidget#freeze ;
+ ignore (Mathml_editor.freeze tex_editor) ;
+ self#reset ;
+ (* we need to remove the initial and final '$' *)
+ let txt' = String.sub txt 1 (String.length txt - 2) in
+ String.iter (fun ch -> Mathml_editor.push tex_editor ch) txt' ;
+ ignore (Mathml_editor.thaw tex_editor) ;
+ mmlwidget#thaw
+
+ method get_as_string =
+ Mathml_editor.get_tex tex_editor
+
+ method get_metasenv_and_term ~context ~metasenv =
+ let name_context =
+ List.map
+ (function
+ Some (n,_) -> Some n
+ | None -> None
+ ) context
+ in
+ let lexbuf = Lexing.from_string self#get_as_string 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
+ 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
+ end
+
+ let term_editor = new term_editor_impl
+
+end
+;;
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+class type term_editor =
+ object
+ method coerce : GObj.widget
+ method get_as_string : string
+ method get_metasenv_and_term :
+ context:Cic.context ->
+ metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ method reset : unit
+ method set_term : string -> unit
+ method id_to_uris : Disambiguate.domain_and_interpretation ref
+ end
+
+val empty_id_to_uris : Disambiguate.domain_and_interpretation
+
+module Make (C : Disambiguate.Callbacks) :
+ sig
+ val term_editor :
+ ?packing:(GObj.widget -> unit) ->
+ ?width:int ->
+ ?height:int ->
+ ?isnotempty_callback:(bool -> unit) ->
+ ?share_id_to_uris_with:term_editor ->
+ unit -> term_editor
+ end
projects / helm.git / commitdiff