From: Claudio Sacerdoti Coen Date: Fri, 15 Oct 2010 12:17:16 +0000 (+0000) Subject: - grafiteSync no longer used X-Git-Tag: make_still_working~2782 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99a43adccee356e3d6057f67114c5cf08518b3f3;p=helm.git - grafiteSync no longer used - grafiteTypes.status simplified --- diff --git a/matita/components/grafite_engine/.depend b/matita/components/grafite_engine/.depend index 10236823a..d04ec9d2c 100644 --- a/matita/components/grafite_engine/.depend +++ b/matita/components/grafite_engine/.depend @@ -1,14 +1,11 @@ grafiteTypes.cmi: -grafiteSync.cmi: grafiteTypes.cmi nCicCoercDeclaration.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi grafiteTypes.cmx: grafiteTypes.cmi -grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi -grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi -grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi grafiteSync.cmi \ +grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \ grafiteEngine.cmi -grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx grafiteSync.cmx \ +grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \ grafiteEngine.cmi diff --git a/matita/components/grafite_engine/Makefile b/matita/components/grafite_engine/Makefile index b6eb8fc63..c8d3866c0 100644 --- a/matita/components/grafite_engine/Makefile +++ b/matita/components/grafite_engine/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteTypes.mli \ - grafiteSync.mli \ nCicCoercDeclaration.mli \ grafiteEngine.mli \ $(NULL) diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml deleted file mode 100644 index 16f731aab..000000000 --- a/matita/components/grafite_engine/grafiteSync.ml +++ /dev/null @@ -1,54 +0,0 @@ -(* 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/ - *) - -(* $Id$ *) - -open Printf - - (** @return l2 \ l1 *) -let uri_list_diff l2 l1 = - let module S = UriManager.UriSet in - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - -let initial_status lexicon_status baseuri = - (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus -;; - -let time_travel ~present ?(past=initial_status present present#baseuri) () = - NCicLibrary.time_travel past -;; - -let init lexicon_status = - initial_status lexicon_status - ;; -let pop () = () -;; - -let push () = () -;; - diff --git a/matita/components/grafite_engine/grafiteSync.mli b/matita/components/grafite_engine/grafiteSync.mli deleted file mode 100644 index 9f562ad86..000000000 --- a/matita/components/grafite_engine/grafiteSync.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* 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 time_travel: - present:GrafiteTypes.status -> ?past:GrafiteTypes.status -> unit -> unit - - (* also resets the imperative part of the status - * init: the baseuri of the current script *) -val init: LexiconEngine.status -> string -> GrafiteTypes.status - -(* - (* just an empty status, does not reset imperative - * part, use push/pop for that *) -val initial_status: string -> GrafiteTypes.status -*) - - (* preserve _only_ imperative parts of the status *) -val push: unit -> unit -val pop: unit -> unit diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index d68331fec..f26be5194 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -38,13 +38,10 @@ class status = fun (b : string) -> in object val moo_content_rev = ([] : GrafiteMarshal.moo) - val objects = ([] : UriManager.uri list) 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 objects = objects - method set_objects v = {< objects = v >} method baseuri = baseuri method set_baseuri v = {< baseuri = v >} method ng_mode = ng_mode; @@ -59,12 +56,3 @@ let add_moo_content cmds status = (* prerr_endline ("new moo content: " ^ String.concat " " (List.map GrafiteAstPp.pp_command content')); *) status#set_moo_content_rev content' - -let dump_status status = - HLog.message "status.aliases:\n"; - HLog.message "status.proof_status:"; - HLog.message "status.options\n"; - HLog.message "status.coercions\n"; - HLog.message "status.objects:\n"; - List.iter - (fun u -> HLog.message (UriManager.string_of_uri u)) status#objects diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index bfa5f9cdb..c65c3afb6 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -36,8 +36,6 @@ class status : object ('self) method moo_content_rev: GrafiteMarshal.moo method set_moo_content_rev: GrafiteMarshal.moo -> 'self - method objects: UriManager.uri list - method set_objects: UriManager.uri list -> 'self method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] @@ -46,7 +44,5 @@ class status : inherit NTacStatus.tac_status end -val dump_status : status -> unit - (** 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/matitaScript.ml b/matita/matita/matitaScript.ml index 65fc0fcec..f3656081f 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -284,7 +284,8 @@ let initial_statuses current baseuri = (match current with Some current -> LexiconSync.time_travel ~present:current ~past:empty_lstatus; - GrafiteSync.time_travel ~present:current (); + NCicLibrary.time_travel + ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus); (* CSC: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); @@ -292,7 +293,7 @@ let initial_statuses current baseuri = CicNotation2.load_notation ~include_paths:[] empty_lstatus BuildTimeConf.core_notation_script in - let grafite_status = GrafiteSync.init lexicon_status baseuri in + let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in grafite_status in let read_include_paths file = @@ -428,7 +429,8 @@ object (self) match history with s::_ -> s | [] -> assert false in LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; - GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status (); + NCicLibrary.time_travel + ((new GrafiteTypes.status cur_grafite_status#baseuri)#set_lstatus cur_grafite_status#lstatus); statements <- new_statements; history <- new_history; self#moveMark (- offset) diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 11806a8a3..f7450ade0 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -164,7 +164,8 @@ let compile atstart options fname = BuildTimeConf.core_notation_script in atstart (); (* FG: do not invoke before loading the core notation script *) - let grafite_status = GrafiteSync.init lexicon_status baseuri in + let grafite_status = + (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = Unix.times () @@ -333,16 +334,13 @@ module F = let matita_debug = Helm_registry.get_bool "matita.debug" in let compile atstart opts fname = try - GrafiteSync.push (); GrafiteParser.push (); let rc = compile atstart opts fname in GrafiteParser.pop (); - GrafiteSync.pop (); rc with | Sys.Break -> GrafiteParser.pop (); - GrafiteSync.pop (); false | exn when not matita_debug -> HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));