From 939dfce0cb12f7e7760a24d89f6812890b9df431 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 11:27:09 +0000 Subject: [PATCH] dead code removal: the parser used to be able to return LNone when it parsed and immediately executed a lexicon command --- .../grafite_parser/grafiteParser.ml | 14 ++----- .../grafite_parser/grafiteParser.mli | 9 +---- matita/matita/matitaEngine.ml | 37 +++++++++---------- matita/matita/matitaScript.ml | 20 ++++------ 4 files changed, 30 insertions(+), 50 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index fb042585a..6da952c7d 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -28,10 +28,6 @@ module N = NotationPt module G = GrafiteAst -type 'a localized_option = - LSome of 'a - | LNone of G.loc - type ast_statement = G.statement let exc_located_wrapper f = @@ -611,12 +607,10 @@ EXTEND ] ]; statement: [ - [ ex = executable -> - LSome (G.Executable (loc, ex)) - | com = comment -> - LSome (G.Comment (loc, com)) + [ ex = executable -> G.Executable (loc, ex) + | com = comment -> G.Comment (loc, com) | (iloc,fname,mode) = include_command ; SYMBOL "." -> - LSome (G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname)))) + G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname))) | EOI -> raise End_of_file ] ]; @@ -625,7 +619,7 @@ EXTEND statement ;; -type db = ast_statement localized_option Grammar.Entry.e ;; +type db = ast_statement Grammar.Entry.e ;; class type g_status = object diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index 3e3f40e13..888b73942 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -23,10 +23,6 @@ * http://helm.cs.unibo.it/ *) -type 'a localized_option = - LSome of 'a - | LNone of GrafiteAst.loc - type ast_statement = GrafiteAst.statement type db @@ -53,7 +49,4 @@ val extend : #status as 'status -> (* never_include: do not call LexiconEngine to do includes, * always raise NoInclusionPerformed *) (** @raise End_of_file *) -val parse_statement: - #status -> - Ulexing.lexbuf -> - ast_statement localized_option +val parse_statement: #status -> Ulexing.lexbuf -> ast_statement diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index bacc4aa26..43a09d2a6 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -99,26 +99,23 @@ let eval_from_stream ~include_paths ?do_heavy_checks match cont with | None -> true, status, statuses | Some ast -> - (match ast with - GrafiteParser.LNone _ -> false, status, ((status,None)::statuses) - | GrafiteParser.LSome ast -> - cb status ast; - let new_statuses = - eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in - if enforce_no_new_aliases then - List.iter - (fun (_,alias) -> - match alias with - None -> () - | Some (k,value) -> - let newtxt = GrafiteAstPp.pp_alias value in - raise (TryingToAdd newtxt)) new_statuses; - let status = - match new_statuses with - [] -> assert false - | (s,_)::_ -> s - in - false, status, (new_statuses @ statuses)) + cb status ast; + let new_statuses = + eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in + if enforce_no_new_aliases then + List.iter + (fun (_,alias) -> + match alias with + None -> () + | Some (k,value) -> + let newtxt = GrafiteAstPp.pp_alias value in + raise (TryingToAdd newtxt)) new_statuses; + let status = + match new_statuses with + [] -> assert false + | (s,_)::_ -> s + in + false, status, (new_statuses @ statuses) with exn when not matita_debug -> raise (EnrichedWithStatus (exn, status)) in diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index c1bf944c7..04cbb9a8f 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -105,8 +105,9 @@ let eval_with_engine include_paths guistuff grafite_status user_goal * in the good order, here files may be compiled on demand. *) let wrap_with_make include_paths f x = match f x with - GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand - (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> + (GrafiteAst.Executable + (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd + -> let root, buri, _, tgt = try Librarian.baseuri_of_script ~include_paths mafilename with Librarian.NoRootFor _ -> @@ -227,20 +228,16 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff txt,nonskipped_txt,skipped_txt,len in match st with - | GrafiteParser.LNone loc -> - let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [grafite_status,parsed_text],"", - parsed_text_length - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> + | GrafiteAst.Executable (loc, ex) -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> + | GrafiteAst.Comment (loc, _) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in @@ -689,15 +686,14 @@ object (self) match GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s) with - | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> + | GrafiteAst.Comment (loc,_) -> let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) let parsed_text_length = parsed_text_length + 1 in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_only_comments lexicon_status next - | GrafiteParser.LNone _ - | GrafiteParser.LSome (GrafiteAst.Executable _) -> false + | GrafiteAst.Executable _ -> false in try is_there_only_comments self#grafite_status self#getFuture with -- 2.39.2