From 238b544db1786fbc68354fd62aa6b05983906997 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 25 Apr 2009 21:12:49 +0000 Subject: [PATCH] - matitacLib: lexicon status and grafite status where lost after handling a macro. Fixed. --- helm/software/matita/matita.ml | 14 +++++++++++--- helm/software/matita/matitaEngine.ml | 4 ++-- helm/software/matita/matitaEngine.mli | 2 +- helm/software/matita/matitaExcPp.ml | 4 ++-- helm/software/matita/matitacLib.ml | 24 ++++++++++++------------ 5 files changed, 28 insertions(+), 20 deletions(-) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index aecf026aa..fb7ad27bf 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -134,10 +134,18 @@ let _ = in addDebugItem "dump aliases" (fun _ -> let status = script#lexicon_status in + LexiconEngine.dump_aliases HLog.debug "" status); +(* FG: DEBUGGING + addDebugItem "dump interpretations" (fun _ -> + let status = script#lexicon_status in + let filter = + List.filter (function LexiconAst.Interpretation _ -> true | _ -> false) + in HLog.debug (String.concat "\n" - (DisambiguateTypes.Environment.fold - (fun _ x l -> (LexiconAstPp.pp_alias x)::l) - status.LexiconEngine.aliases []))); + (List.fold_right + (fun x l -> (LexiconAstPp.pp_command x)::l) + (filter status.LexiconEngine.lexicon_content_rev) []))); +*) addDebugItem "dump environment to \"env.dump\"" (fun _ -> let oc = open_out "env.dump" in CicEnvironment.dump_to_channel oc; diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 5468c863a..cf8d6860b 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -119,7 +119,7 @@ let eval_ast ?do_heavy_checks lexicon_status ((new_grafite_status,new_lexicon_status),None)::intermediate_states exception TryingToAdd of string -exception EnrichedWithLexiconStatus of exn * LexiconEngine.status +exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status let out = ref ignore @@ -173,7 +173,7 @@ let eval_from_stream ~first_statement_only ~include_paths watch_statuses lexicon_status grafite_status ; false, lexicon_status, grafite_status, (new_statuses @ statuses)) with exn when not matita_debug -> - raise (EnrichedWithLexiconStatus (exn, lexicon_status)) + raise (EnrichedWithStatus (exn, lexicon_status, grafite_status)) in if stop then s else loop l g s in diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index 032ee2c1e..9429b00e6 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -38,7 +38,7 @@ val eval_ast : (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) -exception EnrichedWithLexiconStatus of exn * LexiconEngine.status +exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status (* should be used only by the compiler since it looses the * disambiguation_context (text,prefix_len,_) *) diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 7579c3a56..d728fb0b3 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -165,8 +165,8 @@ let rec to_string = None, "Already defined: " ^ UriManager.string_of_uri s | DisambiguateChoices.Choice_not_found msg -> None, ("Disambiguation choice not found: " ^ Lazy.force msg) - | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> - None, "EnrichedWithLexiconStatus "^snd(to_string exn) + | MatitaEngine.EnrichedWithStatus (exn,_,_) -> + None, "EnrichedWithStatus "^snd(to_string exn) | NTacStatus.Error msg -> None, "NTactic error: " ^ Lazy.force msg | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index b33b103c1..7a6d48663 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -185,7 +185,7 @@ let compile atstart options fname = CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script in - atstart (); + atstart (); (* FG: do not invoke before loading the core notation script *) let grafite_status = GrafiteSync.init lexicon_status baseuri in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = @@ -233,20 +233,20 @@ let compile atstart options fname = if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) else pp_ast_statement in - let grafite_status, lexicon_status = - let rec aux_for_dump x = + let lexicon_status, grafite_status = + let rec aux_for_dump x lexicon_status grafite_status = try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths lexicon_status grafite_status buf x with - | [] -> grafite_status, lexicon_status - | ((grafite,lexicon),None)::_ -> grafite, lexicon + | [] -> lexicon_status, grafite_status + | ((grafite,lexicon),None)::_ -> lexicon, grafite | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) - with MatitaEngine.EnrichedWithLexiconStatus - (GrafiteEngine.Macro (floc, f), lex_status) as exn -> - match f (get_macro_context (Some grafite_status)) with + with MatitaEngine.EnrichedWithStatus + (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn -> + match f (get_macro_context (Some grafite)) with | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) -> let str = ApplyTransformation.txt_of_inline_macro style prefix suri @@ -255,10 +255,10 @@ let compile atstart options fname = "matita.paste_unicode_as_tex") in !out str; - aux_for_dump x + aux_for_dump x lexicon grafite |_-> raise exn in - aux_for_dump print_cb + aux_for_dump print_cb lexicon_status grafite_status in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = @@ -306,7 +306,7 @@ let compile atstart options fname = ~present:lexicon_status ~past:initial_lexicon_status; *) clean_exit baseuri false - | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' -> + | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' -> (match exn with | Sys.Break -> HLog.error "user break!" | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> @@ -315,7 +315,7 @@ let compile atstart options fname = | exn when matita_debug -> raise exn' | exn -> HLog.error (snd (MatitaExcPp.to_string exn)) ); -(* LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; +(* LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; * *) pp_times fname false big_bang big_bang_u big_bang_s; clean_exit baseuri false -- 2.39.2