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

diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml
deleted file mode 100644
index 0d959ac65..000000000
--- a/helm/gTopLevel/batchParser.ml
+++ /dev/null
@@ -1,89 +0,0 @@
-(* Copyright (C) 2004, 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://helm.cs.unibo.it/
- *)
-
-let verbose = false
-
-exception Failure of string
-let fail msg = raise (Failure msg)
-
-let constants_only ~prefix =
- let test_prefix =
-  if prefix = "" then
-   (fun _ -> true)
-  else
-   (fun uri -> Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ prefix)) uri)
- in
- fun uri ->
-  test_prefix uri && (not (String.sub uri (String.length uri - 4) 4 = ".var"))
-
-let uri_predicate = ref (constants_only ~prefix:"")
-
-let uri_pred_of_conf tryvars ~prefix ~varsprefix =
-  if not tryvars then
-    constants_only ~prefix
-  else
-    let test_prefix = Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ prefix)) in
-    let test_varsprefix = Pcre.pmatch ~rex:(Pcre.regexp ("^" ^ varsprefix)) in
-     fun uri ->
-      if String.sub uri (String.length uri - 4) 4 = ".var" then
-       test_varsprefix uri
-      else
-       test_prefix uri
-
-module DisambiguateCallbacks =
- struct
-  let interactive_user_uri_choice
-   ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices =
-     List.filter !uri_predicate choices
-
-  let interactive_interpretation_choice =
-   let rec aux n =
-    function
-       [] -> []
-     | _::tl -> n::(aux (n+1) tl)
-   in
-    aux 0
-
-  let input_or_locate_uri ~title = fail "Unknown identifier"
- end
-
-module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks)
-
-let parse mqi_handle ?(uri_pred = constants_only ~prefix:"") =
-  uri_predicate := uri_pred;
-  let empty_environment =
-    DisambiguatingParser.EnvironmentP3.of_string
-      DisambiguatingParser.EnvironmentP3.empty
-  in
-  let empty_context = [] in
-  let empty_metasenv = [] in
-  fun input ->
-   (Disambiguate'.disambiguate_term
-     mqi_handle empty_context empty_metasenv input empty_environment)
-
-let parse_pp mqi_handle ?uri_pred input = 
- List.map (fun (_,_,t) -> CicPp.ppterm t)
-  (parse mqi_handle ?uri_pred input)
-