From cb408b9ea336cd8efb990f7a1c88b566ccf0bd2e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 5 Jul 2005 13:57:07 +0000 Subject: [PATCH] * new interface matitaTypes.mli * when exiting with an error message matitac cleans what it produced during the interrupted compilation --- helm/matita/.depend | 76 +++++++++++++------------ helm/matita/Makefile.in | 3 +- helm/matita/matitaSync.ml | 6 +- helm/matita/matitaSync.mli | 3 +- helm/matita/matitaTypes.mli | 100 +++++++++++++++++++++++++++++++++ helm/matita/matitacLib.ml | 22 ++++++-- helm/matita/matitacLib.mli | 25 +++++++++ helm/matita/matitacleanLib.ml | 4 +- helm/matita/matitacleanLib.mli | 2 +- 9 files changed, 190 insertions(+), 51 deletions(-) create mode 100644 helm/matita/matitaTypes.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index d6272980d..8a4e05d8a 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,32 +1,24 @@ -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi -matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx -matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \ - matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi -matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi -matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx -matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi +matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi -matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ +matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi -matitaExcPp.cmo: matitaTypes.cmo matitaExcPp.cmi +matitaExcPp.cmo: matitaTypes.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaTypes.cmx matitaExcPp.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi -matitaGtkMisc.cmo: matitaTypes.cmo matitaGeneratedGui.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi -matitaGui.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi matitaLog.cmi \ +matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaLog.cmi \ matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ @@ -34,37 +26,47 @@ matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ buildTimeConf.cmx matitaGui.cmi matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi -matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ +matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaGui.cmx matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ matitaMathView.cmi -matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx -matitaScript.cmo: matitacleanLib.cmi matitaTypes.cmo matitaSync.cmi \ +matitaScript.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ matitaMisc.cmi matitaLog.cmi matitaEngine.cmi matitaDisambiguator.cmi \ matitaDb.cmi matitaScript.cmi matitaScript.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ matitaMisc.cmx matitaLog.cmx matitaEngine.cmx matitaDisambiguator.cmx \ matitaDb.cmx matitaScript.cmi -matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ +matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ matitaSync.cmi matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi -matitaTypes.cmo: matitaLog.cmi -matitaTypes.cmx: matitaLog.cmx -matitaDisambiguator.cmi: matitaTypes.cmo -matitaEngine.cmi: matitaTypes.cmo +matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi +matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx +matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \ + matitacLib.cmi +matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + matitacLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi +matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi +matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx +matitaDisambiguator.cmi: matitaTypes.cmi +matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi -matitaMathView.cmi: matitaTypes.cmo -matitaMisc.cmi: matitaTypes.cmo -matitaScript.cmi: matitaTypes.cmo -matitaSync.cmi: matitaTypes.cmo +matitaMathView.cmi: matitaTypes.cmi +matitaMisc.cmi: matitaTypes.cmi +matitaScript.cmi: matitaTypes.cmi +matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 4d03f8dfc..ac2ec13d3 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -48,8 +48,9 @@ CCMOS = \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitaEngine.cmo \ + matitacleanLib.cmo \ matitacLib.cmo -CLEANCMOS = $(CCMOS) matitacleanLib.cmo +CLEANCMOS = $(CCMOS) all: matita matitac matitatop cicbrowser matitadep matitaclean diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 23e3b048f..29e19c690 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -222,7 +222,7 @@ let time_travel ~present ~past = MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 -let remove uri = +let remove ~verbose uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: (match UriManager.bodyuri_of_uri uri with @@ -237,10 +237,10 @@ let remove uri = List.iter (fun uri -> (try - MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); + if verbose then + MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); MatitaMisc.safe_remove (Http_getter.resolve' uri) with Http_getter_types.Key_not_found _ -> ()); remove_coercion uri; ignore (MatitaDb.remove_uri uri)) to_remove - diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index bb573fcb1..66787ad46 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -43,5 +43,4 @@ val set_proof_aliases : (* removes the object from DB, Disk, CoercionsDB, getter * asserts the uri is resolved to file:// so it is only for * user's objects *) -val remove: UriManager.uri -> unit - +val remove: verbose:bool -> UriManager.uri -> unit diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli new file mode 100644 index 000000000..662dad6ab --- /dev/null +++ b/helm/matita/matitaTypes.mli @@ -0,0 +1,100 @@ +(* Copyright (C) 2004-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/ + *) + +exception Cancel +exception Statement_error of string +val statement_error : string -> 'a + +exception Command_error of string +val command_error : string -> 'a + +exception Option_error of string * string +exception Unbound_identifier of string + +type proof_status = + No_proof + | Incomplete_proof of ProofEngineTypes.status + | Proof of ProofEngineTypes.proof + | Intermediate of Cic.metasenv + +module StringMap : Map.S with type key = String.t + +type option_value = + | String of string + | Int of int +type options = option_value StringMap.t +val no_options : 'a StringMap.t + +type status = { + aliases : DisambiguateTypes.environment; + moo_content_rev : string list; + proof_status : proof_status; + options : options; + objects : (UriManager.uri * string) list; +} + +val dump_status : status -> unit +val get_option : status -> StringMap.key -> option_value +val get_string_option : status -> StringMap.key -> string +val set_option : status -> StringMap.key -> string -> status + +class type console = + object + method choose_uri : string list -> string + method clear : unit -> unit + method echo_error : string -> unit + method echo_message : string -> unit + method show : ?msg:string -> unit -> unit + method wrap_exn : (unit -> 'a) -> 'a option + end + +type abouts = [ `Blank | `Current_proof | `Us ] + +type mathViewer_entry = + [ `About of abouts + | `Check of string + | `Cic of Cic.term * Cic.metasenv + | `Dir of string + | `Uri of UriManager.uri + | `Whelp of string * UriManager.uri list ] + +val string_of_entry : + [< `About of [< `Blank | `Current_proof | `Us ] + | `Check of 'a + | `Cic of 'b * 'c + | `Dir of string + | `Uri of UriManager.uri + | `Whelp of string * 'd ] -> + string + +val entry_of_string : + string -> [> `About of [> `Blank | `Current_proof | `Us ] ] + +class type mathViewer = + object + method show_entry : ?reuse:bool -> mathViewer_entry -> unit + method show_uri_list : + ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit + end diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index fbc393cfb..ec722490a 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -98,6 +98,14 @@ let rec go () = MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); go () | exn -> MatitaLog.error (Printexc.to_string exn); go () + +let clean_exit n = + match !status with + None -> exit n + | Some status -> + let baseuri = MatitaTypes.get_string_option !status "baseuri" in + MatitacleanLib.clean_baseuris ~verbose:false [baseuri]; + exit n let main ~mode = Helm_registry.load_from "matita.conf.xml"; @@ -140,7 +148,7 @@ let main ~mode = begin MatitaLog.error "there are still incomplete proofs at the end of the script"; - exit 2 + clean_exit 2 end else begin @@ -157,19 +165,23 @@ let main ~mode = | Sys.Break -> MatitaLog.error "user break!"; if mode = `COMPILER then - exit ~-1 + clean_exit ~-1 else pp_ocaml_mode () | MatitaEngine.Drop -> if mode = `COMPILER then - exit 1 + clean_exit 1 else pp_ocaml_mode () | CicTextualParser2.Parse_error (floc,err) -> let (x, y) = CicAst.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); if mode = `COMPILER then - exit 1 + clean_exit 1 else pp_ocaml_mode () - + | _ -> + if mode = `COMPILER then + clean_exit 3 + else + pp_ocaml_mode () diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli index aad2b29ac..b778b91f3 100644 --- a/helm/matita/matitacLib.mli +++ b/helm/matita/matitacLib.mli @@ -1,2 +1,27 @@ +(* Copyright (C) 2004-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/ + *) + val go : unit -> unit val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 37c87d770..a616519c1 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -115,14 +115,14 @@ let rec fix uris next = | [] -> uris | l -> let uris, next = close_uri_list l in fix uris next @ uris -let clean_baseuris buris = +let clean_baseuris ?(verbose=true) buris = let buris = List.map HGM.strip_trailing_slash buris in (* List.iter prerr_endline buris; *) let l = fix [] buris in let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in let l = List.map UriManager.uri_of_string l in (* List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) l; *) - List.iter MatitaSync.remove l + List.iter (MatitaSync.remove ~verbose) l let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = [] diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli index 0de7f5867..7077ed41e 100644 --- a/helm/matita/matitacleanLib.mli +++ b/helm/matita/matitacleanLib.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -val clean_baseuris : string list -> unit +val clean_baseuris : ?verbose:bool -> string list -> unit val baseuri_of_file : string -> string val baseuri_of_baseuri_decl : ('a, 'b, 'c) TacticAst.statement -> string option -- 2.39.2