- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / matita / matitaWiki.ml

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 883cf3284fb835cbbcab30afe1764375f3cc7d41..0fa8554ba9856c2dd9644e0132d91a58029334e6 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -66,13 +66,9 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+       let baseuri = GrafiteTypes.get_baseuri grafite_status in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       exit n
 
 let terminate n =
  let terminator = String.make 1 (Char.chr 249) in
@@ -124,6 +120,10 @@ let outer_syntax_parser () =
              with
               Failure _ -> assert false
 ;;
+
+let include_paths =
+ lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
+;;
   
 let rec interactive_loop () = 
   (* every loop is terminated by a terminator both on stdout and stderr *)
@@ -155,7 +155,7 @@ let rec interactive_loop () =
         let watch_statuses lexicon_status grafite_status =
          match grafite_status.GrafiteTypes.proof_status with
             GrafiteTypes.Incomplete_proof
-             {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
+             {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
               GrafiteTypes.stack = stack } ->
               let open_goals = Continuationals.Stack.open_goals stack in
               print_endline
@@ -163,16 +163,15 @@ let rec interactive_loop () =
                  (List.map
                    (fun i ->
                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
+                      ~map_unicode_to_tex:(Helm_registry.get_bool
+                        "matita.paste_unicode_as_tex")
                       (List.find (fun (j,_,_) -> j=i) metasenv)
                    ) open_goals))
           | _ -> ()
-        in
-        let include_paths =
-         Helm_registry.get_list Helm_registry.string "matita.includes"
         in
          run_script str 
-           (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
-           ~include_paths ~watch_statuses) ;
+           (MatitaEngine.eval_from_stream ~first_statement_only:true 
+           ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
          interactive_loop (Some (List.length !lexicon_status))
   with 
    | GrafiteEngine.Macro (floc,_) ->
@@ -201,18 +200,17 @@ let main () =
        | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
        | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
      in
-      output_string stdout s;
-      flush stdout
+      output_string stderr s;
+      flush stderr
    );
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
-  Helm_registry.set_int "matita.verbosity" 0;
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
-  grafite_status := [GrafiteSync.init ()];
   lexicon_status :=
    [CicNotation2.load_notation ~include_paths
      BuildTimeConf.core_notation_script] ;
+  grafite_status := [GrafiteSync.init (List.hd !lexicon_status) "cic:/matita/tests/"];
   Sys.catch_break true;
   let origcb = HLog.get_log_callback () in
   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
@@ -230,10 +228,10 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,metadata,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev = 
       match !lexicon_status,!grafite_status with
       | ss::_, s::_ ->
-         s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+         s.proof_status, s.moo_content_rev,
           ss.LexiconEngine.lexicon_content_rev
       | _,_ -> assert false
     in
@@ -246,10 +244,11 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_string_option
-         (match !grafite_status with
+        GrafiteTypes.get_baseuri 
+           (match !grafite_status with
              [] -> assert false
-           | s::_ -> s) "baseuri" in
+           | s::_ -> s)
+       in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
            ~must_exist:false ~baseuri ~writable:true 
@@ -258,12 +257,7 @@ let main () =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true
-       in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname metadata;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
        exit 0
      end