Dead code for .moo files removed.

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 1a87934a595cb4c1406d49b39ba81a844f4909f6..22a8dd2248b7b28315a3b7b8d254f7157ae7f7fd 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -27,7 +27,6 @@
 
 exception Drop
 (* mo file name, ma file name *)
-(*exception IncludedFileNotCompiled of string * string *)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a
@@ -569,28 +568,8 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  let status,uris =
   match cmd with
   | GrafiteAst.Include (loc, baseuri) ->
-      (*
-     let status =
-      let moopath_rw, moopath_r = 
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true,
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:false in
-      let moopath = 
-       if Sys.file_exists moopath_r then moopath_r else
-         if Sys.file_exists moopath_rw then moopath_rw else
-           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
-      in
-       eval_from_moo status moopath
-     in
-      let status = *)
        NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status (*in
-      let status =
-       GrafiteTypes.add_moo_content
-        [GrafiteAst.Include (loc,baseuri)] status
-      in
-      status,[] *), []
+        status, []
   | GrafiteAst.Print (_,_) -> status,[]
   | GrafiteAst.Set (loc, name, value) -> status, []
  in
@@ -617,24 +596,6 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
   | GrafiteAst.NMacro (loc, macro) ->
      raise (NMacro (loc,macro))
 
-and eval_from_moo status fname =
-  let ast_of_cmd cmd =
-    ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
-      GrafiteAst.Command (HExtlib.dummy_floc,
-        cmd)))
-  in
-  let moo = GrafiteMarshal.load_moo fname in
-  List.fold_left 
-    (fun status ast -> 
-      let ast = ast_of_cmd ast in
-      let status,lemmas =
-       eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
-         status ast
-      in
-       assert (lemmas=[]);
-       status)
-    status moo
-
 and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
 (text,prefix_len,st)
 =