From 3f9cb46b5e167955e85b3d2544f1bed90f1a25b7 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 27 Oct 2010 15:16:20 +0000 Subject: [PATCH] Dead code for .moo files removed. --- matita/components/grafite/Makefile | 1 - matita/components/grafite/grafiteMarshal.ml | 55 ------------------- matita/components/grafite/grafiteMarshal.mli | 33 ----------- .../grafite_engine/grafiteEngine.ml | 41 +------------- .../grafite_engine/grafiteEngine.mli | 1 - .../components/grafite_engine/grafiteTypes.ml | 10 ---- .../grafite_engine/grafiteTypes.mli | 5 -- matita/matita/matitaGui.ml | 4 -- matita/matita/matitacLib.ml | 6 +- 9 files changed, 3 insertions(+), 153 deletions(-) delete mode 100644 matita/components/grafite/grafiteMarshal.ml delete mode 100644 matita/components/grafite/grafiteMarshal.mli diff --git a/matita/components/grafite/Makefile b/matita/components/grafite/Makefile index 6eb3e7a78..158bc992d 100644 --- a/matita/components/grafite/Makefile +++ b/matita/components/grafite/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteAstPp.mli \ - grafiteMarshal.mli \ $(NULL) IMPLEMENTATION_FILES = \ grafiteAst.ml \ diff --git a/matita/components/grafite/grafiteMarshal.ml b/matita/components/grafite/grafiteMarshal.ml deleted file mode 100644 index d18ee2f0c..000000000 --- a/matita/components/grafite/grafiteMarshal.ml +++ /dev/null @@ -1,55 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - -(* $Id$ *) - -type ast_command = GrafiteAst.command -type moo = ast_command list - -let format_name = "grafite" - -let save_moo_to_file ~fname moo = - HMarshal.save ~fmt:format_name ~version:GrafiteAst.magic ~fname moo - -let load_moo_from_file ~fname = - let raw = HMarshal.load ~fmt:format_name ~version:GrafiteAst.magic ~fname in - (raw: moo) - -let rehash_cmd_uris = - function - | GrafiteAst.Include _ as cmd -> cmd - | cmd -> - prerr_endline "Found a command not expected in a .moo:"; - let term_pp _ = assert false in - let obj_pp _ = assert false in - prerr_endline (GrafiteAstPp.pp_command cmd); - assert false - -let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo) - -let load_moo ~fname = - let moo = load_moo_from_file ~fname in - List.map rehash_cmd_uris moo - diff --git a/matita/components/grafite/grafiteMarshal.mli b/matita/components/grafite/grafiteMarshal.mli deleted file mode 100644 index aebaf1a7f..000000000 --- a/matita/components/grafite/grafiteMarshal.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - -type ast_command = GrafiteAst.command -type moo = ast_command list - -val save_moo: fname:string -> moo -> unit - - (** @raise Corrupt_moo *) -val load_moo: fname:string -> moo - diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 1a87934a5..22a8dd224 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -27,7 +27,6 @@ exception Drop (* mo file name, ma file name *) -(*exception IncludedFileNotCompiled of string * string *) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -569,28 +568,8 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) = let status,uris = match cmd with | GrafiteAst.Include (loc, baseuri) -> - (* - let status = - let moopath_rw, moopath_r = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false in - let moopath = - if Sys.file_exists moopath_r then moopath_r else - if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled (moopath_rw,baseuri)) - in - eval_from_moo status moopath - in - let status = *) NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status (*in - let status = - GrafiteTypes.add_moo_content - [GrafiteAst.Include (loc,baseuri)] status - in - status,[] *), [] + status, [] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Set (loc, name, value) -> status, [] in @@ -617,24 +596,6 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) = | GrafiteAst.NMacro (loc, macro) -> raise (NMacro (loc,macro)) -and eval_from_moo status fname = - let ast_of_cmd cmd = - ("",0,GrafiteAst.Executable (HExtlib.dummy_floc, - GrafiteAst.Command (HExtlib.dummy_floc, - cmd))) - in - let moo = GrafiteMarshal.load_moo fname in - List.fold_left - (fun status ast -> - let ast = ast_of_cmd ast in - let status,lemmas = - eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) - status ast - in - assert (lemmas=[]); - status) - status moo - and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status (text,prefix_len,st) = diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index 4c7371e09..ad88d5dfd 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -24,7 +24,6 @@ *) exception Drop -(*exception IncludedFileNotCompiled of string * string*) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index f26be5194..b99b15eaa 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -37,11 +37,8 @@ class status = fun (b : string) -> NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular)) in object - val moo_content_rev = ([] : GrafiteMarshal.moo) val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) - method moo_content_rev = moo_content_rev - method set_moo_content_rev v = {< moo_content_rev = v >} method baseuri = baseuri method set_baseuri v = {< baseuri = v >} method ng_mode = ng_mode; @@ -49,10 +46,3 @@ class status = fun (b : string) -> (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty)) end - -let add_moo_content cmds status = - let content = status#moo_content_rev in - let content' = cmds@content in -(* prerr_endline ("new moo content: " ^ String.concat " " (List.map - GrafiteAstPp.pp_command content')); *) - status#set_moo_content_rev content' diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index c65c3afb6..e59e5375a 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -34,8 +34,6 @@ val command_error: string -> 'a (** @raise Command_error *) class status : string -> object ('self) - method moo_content_rev: GrafiteMarshal.moo - method set_moo_content_rev: GrafiteMarshal.moo -> 'self method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] @@ -43,6 +41,3 @@ class status : (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) inherit NTacStatus.tac_status end - - (** list is not reversed, head command will be the first emitted *) -val add_moo_content: GrafiteMarshal.ast_command list -> status -> status diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 6f4e09bbc..6d4c8c0f5 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -75,14 +75,10 @@ let save_moo grafite_status = match script#bos, script#eos with | true, _ -> () | _, true -> - let moo_fname = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri - ~writable:true in let lexicon_fname = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in - GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname grafite_status#lstatus.LexiconEngine.lexicon_content_rev; NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index f7450ade0..8ab5d407f 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -225,13 +225,11 @@ let compile atstart options fname = aux_for_dump print_cb grafite_status in let elapsed = Unix.time () -. time in - let moo_content_rev,lexicon_content_rev = - grafite_status#moo_content_rev, - grafite_status#lstatus.LexiconEngine.lexicon_content_rev + let lexicon_content_rev = + grafite_status#lstatus.LexiconEngine.lexicon_content_rev in (if Helm_registry.get_bool "matita.moo" then begin (* FG: we do not generate .moo when dumping .mma files *) - GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump -- 2.39.2