From: Claudio Sacerdoti Coen Date: Thu, 30 Jan 2003 09:43:03 +0000 (+0000) Subject: Minor code reorganization: X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=279178e6812c3fc9d376b5e3c919d59c486d6da3;p=helm.git Minor code reorganization: 1. several functions unrelated do disambiguation moved from Disambiguate do Misc. 2. TermEditor module added. It implements a widget for entering terms. The widget is also responsible for the disambiguation. 3. TermEditor is now the only widget that uses the Disambiguate module. --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index b27f702c0..3e72e3670 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -20,11 +20,16 @@ mQueryLevels2.cmo: mQueryLevels2.cmi 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 diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index cf12d3121..d0210e087 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -15,18 +15,20 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA 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 diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index 11de21b18..ff794fd5b 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -33,70 +33,6 @@ (* *) (******************************************************************************) -(** 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 @@ -135,7 +71,7 @@ module Make(C:Callbacks) = 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= "

Locate Query: 

" ^ get_last_query result ^ "
" @@ -160,7 +96,7 @@ module Make(C:Callbacks) = ~id uris in - List.map cic_textual_parser_uri_of_string uris' + List.map Misc.cic_textual_parser_uri_of_string uris' exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli index 63206cb15..2a03f58d9 100644 --- a/helm/gTopLevel/disambiguate.mli +++ b/helm/gTopLevel/disambiguate.mli @@ -33,13 +33,6 @@ (* *) (******************************************************************************) -(** 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 **) @@ -59,8 +52,7 @@ module type Callbacks = 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 : diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 06f72d550..52f9e407f 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -86,9 +86,6 @@ let postgresqlconnectionstring = 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;; @@ -97,8 +94,6 @@ let current_cic_infos = ref None;; 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);; @@ -221,7 +216,7 @@ let check_window outputhtml uris = 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 @@ -868,6 +863,8 @@ let load () = ;; 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 @@ -926,7 +923,7 @@ let edit_aliases () = 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 @@ -936,11 +933,11 @@ let edit_aliases () = 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 () = @@ -1127,7 +1124,7 @@ let locate_callback id = 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 = ("

Locate Query: 

" ^ get_last_query result ^ "
") @@ -1261,53 +1258,12 @@ module Callbacks = 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 @@ -1328,6 +1284,7 @@ exception UriAlreadyInUse;; 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 @@ -1447,7 +1404,9 @@ let new_inductive () = 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 ;*) @@ -1556,7 +1515,9 @@ let new_inductive () = 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 ;*) @@ -1669,7 +1630,7 @@ let mk_fresh_name_callback context name ~typ = ;; 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 @@ -1714,7 +1675,8 @@ let new_proof () = ~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 ; @@ -1799,7 +1761,7 @@ let check_term_in_scratch scratch_window metasenv context expr = ;; 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 @@ -1829,7 +1791,7 @@ let decompose_uris_choice_callback uris = 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 @@ -1885,7 +1847,7 @@ let call_tactic_with_input tactic () = 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 = @@ -2055,7 +2017,7 @@ let call_tactic_with_input_and_goal_input tactic () = 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 @@ -2396,8 +2358,8 @@ let show_query_results results = (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 @@ -2615,7 +2577,7 @@ let refine_constraints (must_obj,must_rel,must_sort) = ;; 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 @@ -2823,7 +2785,7 @@ let choose_must list_of_must only = ;; 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 = @@ -2854,7 +2816,7 @@ let searchPattern () = 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 = "

Backward Query:

" ^ @@ -2871,7 +2833,7 @@ let searchPattern () = 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 @@ -3501,7 +3463,8 @@ class rendering_window output (notebook : notebook) = 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 ; diff --git a/helm/gTopLevel/misc.ml b/helm/gTopLevel/misc.ml new file mode 100644 index 000000000..139db60c8 --- /dev/null +++ b/helm/gTopLevel/misc.ml @@ -0,0 +1,96 @@ +(* 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 *) +(* 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 +;; diff --git a/helm/gTopLevel/misc.mli b/helm/gTopLevel/misc.mli new file mode 100644 index 000000000..866976004 --- /dev/null +++ b/helm/gTopLevel/misc.mli @@ -0,0 +1,41 @@ +(* 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 *) +(* 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 diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml new file mode 100644 index 000000000..90ce49ae4 --- /dev/null +++ b/helm/gTopLevel/termEditor.ml @@ -0,0 +1,110 @@ +(* 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 *) +(* 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 +;; diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli new file mode 100644 index 000000000..23f657c64 --- /dev/null +++ b/helm/gTopLevel/termEditor.mli @@ -0,0 +1,49 @@ +(* 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