This commit was manufactured by cvs2svn to create branch

[helm.git] / helm / gTopLevel / termEditor.ml

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
deleted file mode 100644 (file)
index 310efd1..0000000
--- a/helm/gTopLevel/termEditor.ml
+++ /dev/null
@@ -1,113 +0,0 @@
-(* 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
-   (* get_as_string returns the unquoted string *)
-   method get_as_string : string
-   method get_metasenv_and_term :
-     context:Cic.context ->
-     metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
-   method reset : unit
-   (* The input of set_term is unquoted *)
-   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 mqi_handle ?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 *)
-      (* get_as_string returns the unquoted string *)
-      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 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
-   end
-
-   let term_editor = new term_editor_impl
-
-end
-;;