removed all old matita files (kept in attic)

[helm.git] / helm / matita / matitac.ml

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
deleted file mode 100644 (file)
index 533bbc6..0000000
--- a/helm/matita/matitac.ml
+++ /dev/null
@@ -1,113 +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/
- *)
-
-open Printf
-
-open MatitaTypes
-
-let message s = printf  "** MatitaC: %s\n" s; flush stdout
-let warn s =    eprintf "** MatitaC WARNING: %s\n" s; flush stdout
-let error s =   eprintf "** MatitaC ERROR: %s\n" s; flush stderr
-
-  (** console which prints on stdout/stderr *)
-class tty_console =
-  object (self)
-    method clear () = ()
-    method echo_message s = message s
-    method echo_error s =  error s
-      (* TODO Zack: this method is similar to omonymous method in console,
-      * factorize it in a common super class *)
-    method wrap_exn: 'a. (unit -> 'a) -> 'a option =
-      fun f ->
-      try
-        Some (f ())
-      with exn ->
-        self#echo_error (explain exn);
-        None
-    method show ?(msg = "") () = assert false; ()
-    method choose_uri (uris: string list): string = assert false
-  end
-
-(** {2 Initialization} *)
-
-let arg_spec = [
-(*   "-opt", Arg...., "set bla bla bla"; *)
-]
-let usage =
-  sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:"
-    BuildTimeConf.version
-
-let _ =
-  Helm_registry.load_from "matita.conf.xml";
-  Http_getter.init ();
-  MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-  MatitaDb.clean_owner_environment ();
-  MatitaDb.create_owner_environment ()
-
-let scripts =
-  let acc = ref [] in
-  let add_script fname = acc := fname :: !acc in
-  Arg.parse arg_spec add_script usage;
-  List.rev !acc
-
-let console = new tty_console
-let interpreter = MatitaInterpreter.interpreter ~console ()
-
-let run_script fname =
-  message (sprintf "execution of %s started:" fname);
-  let script =
-    let ic = open_in fname in
-    let ast = 
-      try 
-        snd (CicTextualParser2.parse_script (Stream.of_channel ic)) 
-      with
-        exn -> 
-          error (explain exn); 
-          assert false (* should be something like (Unix.exit 1) *)
-    in
-    close_in ic;
-    ast
-  in
-  let rec aux = function
-    | [] -> ()  (* script is over *)
-    | DisambiguateTypes.Comment _ :: tl -> aux tl
-    | DisambiguateTypes.Command ast :: tl ->
-        let loc =
-          match ast with
-          | TacticAst.LocatedTactical (loc, _) -> loc
-          | _ -> assert false
-        in
-        let (success, _) = interpreter#evalAst ast in
-        if not success then
-          error (sprintf "%s: error at %s, aborting." fname
-            (CicAst.pp_location loc))
-        else
-          aux tl
-  in
-  aux script;
-  message (sprintf "execution of %s completed." fname)
-
-let _ = List.iter run_script scripts
-