]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitacLib.ml
notation kind of works
[helm.git] / matita / matita / matitacLib.ml
index eb4ed69915f1e17cbc4b36639ed7500f1ef5d164..cf037531fa73fb5d401ce08e83c023cc02b48cc2 100644 (file)
@@ -29,16 +29,13 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of LexiconEngine.status
+exception AttemptToInsertAnAlias of LexiconTypes.status
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
 let pp_ast_statement grafite_status stm =
-  let stm = GrafiteAstPp.pp_statement
+  let stm = GrafiteAstPp.pp_statement stm
     ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
-    ~term_pp:NotationPp.pp_term
-    ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj
-    NotationPp.pp_term) stm
   in
   let stm = Pcre.replace ~rex:slash_n_RE stm in
   let stm =
@@ -52,45 +49,6 @@ let clean_exit baseuri rc =
   LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
 ;;
 
-let dump f =
-   let module G = GrafiteAst in
-   let module L = LexiconAst in
-   let module H = HExtlib in
-   let floc = H.dummy_floc in
-   let nl_ast = G.Comment (floc, G.Note (floc, "")) in
-   let pp_statement stm =
-     GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
-       ~map_unicode_to_tex:(Helm_registry.get_bool
-         "matita.paste_unicode_as_tex")
-       ~lazy_term_pp:NotationPp.pp_term 
-       ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
-   in
-   let pp_lexicon = LexiconAstPp.pp_command in
-   let och = open_out f in
-   let nl () =  output_string och (pp_statement nl_ast) in
-   MatitaMisc.out_preamble och;
-   let grafite_parser_cb = function
-      | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
-      | stm ->
-         output_string och (pp_statement stm); nl (); nl ()
-   in
-   let lexicon_parser_cb cmd =
-         output_string och (pp_lexicon cmd); nl (); nl ()
-   in
-   begin fun () ->
-      Helm_registry.set_bool "matita.moo" false;
-      GrafiteParser.set_grafite_callback grafite_parser_cb;
-      GrafiteParser.set_lexicon_callback lexicon_parser_cb
-   end, 
-   begin fun x ->
-      close_out och;
-      GrafiteParser.set_grafite_callback (fun _ -> ());
-      GrafiteParser.set_lexicon_callback (fun _ -> ());
-      Helm_registry.set_bool "matita.moo" true;
-      x
-   end
-;;
-
 let get_macro_context = function _ -> []
 ;;
    
@@ -164,26 +122,16 @@ let compile atstart options fname =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
-  let lexicon_status = 
-    CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
-      BuildTimeConf.core_notation_script 
-  in
+  let lexicon_status = new LexiconTypes.status 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 () 
   in
   let time = Unix.time () in
   try
-    (* sanity checks *)
-    let moo_fname = 
-     LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
-    in
-    let lexicon_fname= 
-     LibraryMisc.lexicon_file_of_baseuri 
-       ~must_exist:false ~baseuri ~writable:true
-    in
     (* cleanup of previously compiled objects *)
     if (not (Http_getter_storage.is_empty ~local:true baseuri))
       then begin
@@ -224,21 +172,14 @@ let compile atstart options fname =
       | [] -> grafite_status
       | (g,None)::_ -> g
       | (g,Some _)::_ ->
-         raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
+         raise (AttemptToInsertAnAlias (g :> LexiconTypes.status))
      in
        aux_for_dump print_cb grafite_status
     in
     let elapsed = Unix.time () -. time in
-    let moo_content_rev,lexicon_content_rev = 
-      grafite_status#moo_content_rev, 
-       grafite_status#lstatus.LexiconEngine.lexicon_content_rev
-    in
      (if Helm_registry.get_bool "matita.moo" then begin
-        (* FG: we do not generate .moo when dumping .mma files *)
-        GrafiteMarshal.save_moo moo_fname moo_content_rev;
-        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-        NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-         grafite_status#dump
+       GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in
@@ -338,32 +279,16 @@ 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
+        (* MATITA 1.0: c'erano le push/pop per il parser; ma per
+         * l'environment nuovo? *)
+         compile atstart opts fname
         with 
-        | Sys.Break ->
-            GrafiteParser.pop ();
-            GrafiteSync.pop ();
-            false
+        | Sys.Break -> false
         | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
-      if Filename.check_suffix fname ".mma" then 
-         let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
-         let atstart, atexit = dump generated in
-         let res = compile atstart options fname in
-         let r = compact (atexit res) in
-         if r then r else begin
-(*            Sys.remove generated; *)
-            Printf.printf "rm %s\n" generated; flush stdout; r
-         end
-      else
-         compact (compile ignore options fname)
+       compact (compile ignore options fname)
     ;;
 
     let load_deps_file = Librarian.load_deps_file;;