X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FtermEditor.ml;fp=helm%2FgTopLevel%2FtermEditor.ml;h=0000000000000000000000000000000000000000;hp=3a74ef05111ce88f2948052896e5ce47a9fc598e;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
deleted file mode 100644
index 3a74ef051..000000000
--- a/helm/gTopLevel/termEditor.ml
+++ /dev/null
@@ -1,118 +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                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-open Printf
-
-(* 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 environment : DisambiguatingParser.EnvironmentP3.t ref
- end
-
-module Make(C:DisambiguateTypes.Callbacks) =
-  struct
-
-   module Disambiguate' = DisambiguatingParser.Make(C);;
-
-   class term_editor_impl mqi_handle ?packing ?width ?height
-    ?isnotempty_callback ?share_environment_with () : term_editor
-   =
-    let environment =
-     match share_environment_with with
-        None -> ref
-          (DisambiguatingParser.EnvironmentP3.of_string
-            DisambiguatingParser.EnvironmentP3.empty)
-      | Some obj -> obj#environment
-    in
-    let input = GText.view ~editable:true ?width ?height ?packing () in
-    let _ =
-     match isnotempty_callback with
-        None -> ()
-      | Some callback ->
-         ignore(input#buffer#connect#changed
-          (function () -> callback (input#buffer#char_count > 0)))
-    in
-     object(self)
-
-      method coerce = input#coerce
-
-      method reset =
-       input#buffer#delete input#buffer#start_iter input#buffer#end_iter
-      (* CSC: txt is now a string, but should be of type Cic.term *)
-
-      method set_term txt =
-       self#reset ;
-       ignore (input#buffer#insert txt)
-
-      (* CSC: this method should disappear *)
-      (* get_as_string returns the unquoted string *)
-      method get_as_string = input#buffer#get_text ()
-
-      method get_metasenv_and_term ~context ~metasenv =
-       let name_context =
-        List.map
-         (function
-             Some (n,_) -> Some n
-           | None -> None
-         ) context
-       in
-        let environment',metasenv,expr =
-         match
-          Disambiguate'.disambiguate_term mqi_handle context metasenv
-           (input#buffer#get_text ()) !environment
-         with
-            [environment',metasenv,expr] -> environment',metasenv,expr
-          | _ -> assert false
-        in
-        environment := environment';
-        (metasenv, expr)
-
-      method environment = environment
-   end
-
-   let term_editor = new term_editor_impl
-
-end
-