dead code removal: the parser used to be able to return LNone when it

parsed and immediately executed a lexicon command

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index fb042585aedec3e8703970d2741bc88c9886d406..6da952c7d2ada70e80cc973925c747d7d07a25fd 100644 (file)
--- 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 3e3f40e13183d3fbd10e8bcef2b2e3f8365adf9a..888b7394249b148313929ba702f09726f0a609b3 100644 (file)
--- 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 bacc4aa26b3a8452a9cdde7baf425c82c2238d95..43a09d2a6e50cd329592086ea0eefe28a6976a12 100644 (file)
--- 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 c1bf944c78df83e46fe0c659996ea99346c21090..04cbb9a8fde4fa493015812b84701ef30390d256 100644 (file)
--- 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