mQueryLevels2.cmx: mQueryLevels2.cmi
mQueryGenerator.cmo: mQueryGenerator.cmi
mQueryGenerator.cmx: mQueryGenerator.cmi
-disambiguate.cmo: mQueryGenerator.cmi disambiguate.cmi
-disambiguate.cmx: mQueryGenerator.cmx disambiguate.cmi
-gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi disambiguate.cmi \
- logicalOperations.cmi mQueryGenerator.cmi mQueryLevels.cmi \
- mQueryLevels2.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi
-gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx disambiguate.cmx \
- logicalOperations.cmx mQueryGenerator.cmx mQueryLevels.cmx \
- mQueryLevels2.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx
+misc.cmo: misc.cmi
+misc.cmx: misc.cmi
+disambiguate.cmo: mQueryGenerator.cmi misc.cmi disambiguate.cmi
+disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi
+termEditor.cmo: disambiguate.cmi termEditor.cmi
+termEditor.cmx: disambiguate.cmx termEditor.cmi
+termEditor.cmi: disambiguate.cmi
+gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \
+ mQueryGenerator.cmi mQueryLevels.cmi mQueryLevels2.cmi misc.cmi \
+ proofEngine.cmi sequentPp.cmi termEditor.cmi xml2Gdome.cmi
+gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \
+ mQueryGenerator.cmx mQueryLevels.cmx mQueryLevels2.cmx misc.cmx \
+ proofEngine.cmx sequentPp.cmx termEditor.cmx xml2Gdome.cmx
all: gTopLevel
opt: gTopLevel.opt
-DEPOBJS = \
- 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 mQueryGenerator.mli mQueryLevels.ml \
- mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml disambiguate.ml \
- disambiguate.mli gTopLevel.ml
-
-TOPLEVELOBJS = \
- xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
- cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
- mQueryLevels2.cmo mQueryGenerator.cmo disambiguate.cmo gTopLevel.cmo
+DEPOBJS = \
+ 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 mQueryGenerator.mli mQueryLevels.ml \
+ mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \
+ disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
+ gTopLevel.ml
+
+TOPLEVELOBJS = \
+ xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
+ cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
+ mQueryLevels2.cmo mQueryGenerator.cmo misc.cmo disambiguate.cmo \
+ termEditor.cmo gTopLevel.cmo
depend:
$(OCAMLDEP) $(DEPOBJS) > .depend
(* *)
(******************************************************************************)
-(** Functions that should be moved in another module **)
-
-exception IllFormedUri of string;;
-
-let string_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
- let uri' =
- match uri with
- CTP.ConUri uri -> UriManager.string_of_uri uri
- | CTP.VarUri uri -> UriManager.string_of_uri uri
- | CTP.IndTyUri (uri,tyno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
- | CTP.IndConUri (uri,tyno,consno) ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
- string_of_int consno
- in
- (* 4 = String.length "cic:" *)
- String.sub uri' 4 (String.length uri' - 4)
-;;
-
-let cic_textual_parser_uri_of_string uri' =
- prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
- try
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
- CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
- if String.sub uri' (String.length uri' - 4) 4 = ".var" then
- CicTextualParser0.VarUri (UriManager.uri_of_string uri')
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
- CicTextualParser0.IndTyUri (uri'',typeno)
- with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
- )
- with
- _ -> raise (IllFormedUri uri')
-;;
-let cic_textual_parser_uri_of_string uri' =
- let res = cic_textual_parser_uri_of_string uri' in
- prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
- res
-
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
- let index_sharp = String.index uri '#' in
- let index_rest = index_sharp + 10 in
- let baseuri = String.sub uri 0 index_sharp in
- let rest =
- String.sub uri index_rest (String.length uri - index_rest - 1)
- in
- baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
let get_last_query =
let query = ref "" in
let uris =
List.map
(function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
+ Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
let html=
" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
~id
uris
in
- List.map cic_textual_parser_uri_of_string uris'
+ List.map Misc.cic_textual_parser_uri_of_string uris'
exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
(* *)
(******************************************************************************)
-(** Functions that should be moved in another module **)
-exception IllFormedUri of string
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-
(** This module provides a functor to disambiguate the input **)
(** given a set of user-interface call-backs **)
type domain_and_interpretation =
string list * (string -> CicTextualParser0.uri option)
-module Make :
- functor (C : Callbacks) ->
+module Make (C : Callbacks) :
sig
exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
val disambiguate_input :
Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
;;
-let empty_id_to_uris = ([],function _ -> None);;
-
-
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
let current_goal_infos = ref None;;
let current_scratch_infos = ref None;;
-let id_to_uris = ref empty_id_to_uris;;
-
let check_term = ref (fun _ _ _ -> assert false);;
let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
let expr =
let term =
term_of_cic_textual_parser_uri
- (Disambiguate.cic_textual_parser_uri_of_string uri)
+ (Misc.cic_textual_parser_uri_of_string uri)
in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
;;
let edit_aliases () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ let id_to_uris = inputt#id_to_uris in
let chosen = ref false in
let window =
GWindow.window
let n' = Str.search_forward regexpr inputtext n in
let id = Str.matched_group 2 inputtext in
let uri =
- Disambiguate.cic_textual_parser_uri_of_string
+ Misc.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
in
let dom,resolve_id = aux (n' + 1) in
id::dom,
(function id' -> if id = id' then Some uri else resolve_id id')
with
- Not_found -> empty_id_to_uris
+ Not_found -> TermEditor.empty_id_to_uris
in
aux 0
in
- id_to_uris := dom,resolve_id
+ id_to_uris := (dom,resolve_id)
;;
let proveit () =
let uris =
List.map
(function uri,_ ->
- Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
let html =
(" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
end
;;
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-class term_editor ?packing ?width ?height ?isnotempty_callback () =
- let input = GEdit.text ~editable:true ?width ?height ?packing () in
- let _ =
- match isnotempty_callback with
- None -> ()
- | Some callback ->
- ignore(input#connect#changed (function () -> callback (input#length > 0)))
- in
-object(self)
- method coerce = input#coerce
- method reset =
- input#delete_text 0 input#length
- (* CSC: txt is now a string, but should be of type Cic.term *)
- method set_term txt =
- self#reset ;
- ignore ((input#insert_text txt) ~pos:0)
- (* CSC: this method should disappear *)
- method get_as_string =
- input#get_chars 0 input#length
- 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 (input#get_chars 0 input#length) in
- let dom,mk_metasenv_and_expr =
- CicTextualParserContext.main
- ~context:name_context ~metasenv CicTextualLexer.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
-end
-;;
+module TermEditor' = TermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
let locate () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
match
exception NotAUriToAConstant;;
let new_inductive () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:20 ~packing:scrolled_window#add
+ ~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:20 ~packing:scrolled_window#add
+ ~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
;;
let new_proof () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ ~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
;;
let check scratch_window () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
match !ProofEngine.proof with
let module U = UriManager in
List.map
(function uri ->
- match Disambiguate.cic_textual_parser_uri_of_string uri with
+ match Misc.cic_textual_parser_uri_of_string uri with
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let uri,metasenv,bo,ty =
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
match notebook#proofw#get_selections with
(fun ~row ~column ~event ->
let (uristr,_) = List.nth results row in
match
- Disambiguate.cic_textual_parser_uri_of_string
- (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
+ Misc.cic_textual_parser_uri_of_string
+ (Misc.wrong_xpointer_format_from_wrong_xpointer_format'
uristr)
with
CicTextualParser0.ConUri uri
;;
let completeSearchPattern () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
;;
let searchPattern () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv =
let uris =
List.map
(function uri,_ ->
- Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
+ Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
let html =
" <h1>Backward Query: </h1>" ^
if
ProofEngine.can_apply
(term_of_cic_textual_parser_uri
- (Disambiguate.cic_textual_parser_uri_of_string uri))
+ (Misc.cic_textual_parser_uri_of_string uri))
then
uri::tl',exc
else
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
check_menu_item#misc#set_sensitive b ;
--- /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 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+exception IllFormedUri of string;;
+
+let string_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ let uri' =
+ match uri with
+ CTP.ConUri uri -> UriManager.string_of_uri uri
+ | CTP.VarUri uri -> UriManager.string_of_uri uri
+ | CTP.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
+ | CTP.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
+ string_of_int consno
+ in
+ (* 4 = String.length "cic:" *)
+ String.sub uri' 4 (String.length uri' - 4)
+;;
+
+let cic_textual_parser_uri_of_string uri' =
+ prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
+ try
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+ CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+ else
+ if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+ CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+ CicTextualParser0.IndTyUri (uri'',typeno)
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
+ )
+ with
+ _ -> raise (IllFormedUri uri')
+;;
+let cic_textual_parser_uri_of_string uri' =
+ let res = cic_textual_parser_uri_of_string uri' in
+ prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
+ res
+
+(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
+let wrong_xpointer_format_from_wrong_xpointer_format' uri =
+ try
+ let index_sharp = String.index uri '#' in
+ let index_rest = index_sharp + 10 in
+ let baseuri = String.sub uri 0 index_sharp in
+ let rest =
+ String.sub uri index_rest (String.length uri - index_rest - 1)
+ in
+ baseuri ^ "#" ^ rest
+ with Not_found -> uri
+;;
--- /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> *)
+(* 15/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** Functions that should be moved in another module **)
+exception IllFormedUri of string
+val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
+val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
+
+val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
--- /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 id_to_uris =
+ match share_id_to_uris_with with
+ None -> ref empty_id_to_uris
+ | Some obj -> obj#id_to_uris
+ in
+ let input = GEdit.text ~editable:true ?width ?height ?packing () in
+ let _ =
+ match isnotempty_callback with
+ None -> ()
+ | Some callback ->
+ ignore(input#connect#changed
+ (function () -> callback (input#length > 0)))
+ in
+ object(self)
+ method coerce = input#coerce
+ method reset =
+ input#delete_text 0 input#length
+ (* CSC: txt is now a string, but should be of type Cic.term *)
+ method set_term txt =
+ self#reset ;
+ ignore ((input#insert_text txt) ~pos:0)
+ (* CSC: this method should disappear *)
+ method get_as_string =
+ input#get_chars 0 input#length
+ 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 (input#get_chars 0 input#length) in
+ let dom,mk_metasenv_and_expr =
+ CicTextualParserContext.main
+ ~context:name_context ~metasenv CicTextualLexer.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 : string list * (string -> CicTextualParser0.uri option)
+
+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